Theory $\mathsf{PA^-}$ #

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.addZero :

ArithmeticSentence

Equations

LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.addZero = (“∀¹ (!!(LO.FirstOrder.Semiterm.bvar 0) + 0 ) = !!(LO.FirstOrder.Semiterm.bvar 0)”)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.addAssoc :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.addComm :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.addEqOfLt :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.zeroLe :

ArithmeticSentence

Equations

LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.zeroLe = (“∀¹ 0 ≤ !!(LO.FirstOrder.Semiterm.bvar 0)”)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.zeroLtOne :

ArithmeticSentence

Equations

LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.zeroLtOne = (“0 < 1 ”)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.oneLeOfZeroLt :

ArithmeticSentence

Equations

LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.oneLeOfZeroLt = (“∀¹ (0 < !!(LO.FirstOrder.Semiterm.bvar 0) → 1 ≤ !!(LO.FirstOrder.Semiterm.bvar 0))”)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.addLtAdd :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulZero :

ArithmeticSentence

Equations

LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulZero = (“∀¹ (!!(LO.FirstOrder.Semiterm.bvar 0) * 0 ) = 0 ”)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulOne :

ArithmeticSentence

Equations

LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulOne = (“∀¹ (!!(LO.FirstOrder.Semiterm.bvar 0) * 1 ) = !!(LO.FirstOrder.Semiterm.bvar 0)”)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulAssoc :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulComm :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulLtMul :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.distr :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.ltIrrefl :

ArithmeticSentence

Equations

LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.ltIrrefl = (“∀¹ ¬!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.bvar 0)”)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.ltTrans :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.PeanoMinus.Axiom.ltTri :

ArithmeticSentence

Equations

One or more equations did not get rendered due to their size.

Instances For

source

inductive LO.FirstOrder.Arithmetic.PeanoMinus :

ArithmeticTheory

equal (φ : Sentence ℒₒᵣ) : φ ∈ 𝗘𝗤 ℒₒᵣ → 𝗣𝗔⁻ φ
addZero : 𝗣𝗔⁻ Axiom.addZero
addAssoc : 𝗣𝗔⁻ Axiom.addAssoc
addComm : 𝗣𝗔⁻ Axiom.addComm
addEqOfLt : 𝗣𝗔⁻ Axiom.addEqOfLt
zeroLe : 𝗣𝗔⁻ Axiom.zeroLe
zeroLtOne : 𝗣𝗔⁻ Axiom.zeroLtOne
oneLeOfZeroLt : 𝗣𝗔⁻ Axiom.oneLeOfZeroLt
addLtAdd : 𝗣𝗔⁻ Axiom.addLtAdd
mulZero : 𝗣𝗔⁻ Axiom.mulZero
mulOne : 𝗣𝗔⁻ Axiom.mulOne
mulAssoc : 𝗣𝗔⁻ Axiom.mulAssoc
mulComm : 𝗣𝗔⁻ Axiom.mulComm
mulLtMul : 𝗣𝗔⁻ Axiom.mulLtMul
distr : 𝗣𝗔⁻ Axiom.distr
ltIrrefl : 𝗣𝗔⁻ Axiom.ltIrrefl
ltTrans : 𝗣𝗔⁻ Axiom.ltTrans
ltTri : 𝗣𝗔⁻ Axiom.ltTri

Instances For

source

def LO.FirstOrder.Arithmetic.«term𝗣𝗔⁻» :

Lean.ParserDescr

Equations

LO.FirstOrder.Arithmetic.«term𝗣𝗔⁻» = Lean.ParserDescr.node `LO.FirstOrder.Arithmetic.«term𝗣𝗔⁻» 1024 (Lean.ParserDescr.symbol "𝗣𝗔⁻")

Instances For

source

@[simp]

theorem LO.FirstOrder.Arithmetic.PeanoMinus.finite :

Set.Finite 𝗣𝗔⁻

source

theorem LO.FirstOrder.Arithmetic.PeanoMinus.equiv_singleton_finiteConj :

𝗣𝗔⁻ ≊ {finite.toFinset.conj}

source

@[simp]

instance LO.FirstOrder.Arithmetic.PeanoMinus.instModelsSetStrucORingSentenceStrNat :

ℕ ↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻

source

instance LO.FirstOrder.Arithmetic.PeanoMinus.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiom :

𝗘𝗤 ℒₒᵣ ⪯ 𝗣𝗔⁻

source

@[implicit_reducible]

def LO.FirstOrder.Arithmetic.instLE_foundation {M : Type u_1} [ORingStructure M] :

LE M

Equations

LO.FirstOrder.Arithmetic.instLE_foundation = { le := fun (x y : M) => x = y ∨ x < y }

Instances For

source

theorem LO.FirstOrder.Arithmetic.le_def {M : Type u_1} [ORingStructure M] {x y : M} :

x ≤ y ↔ x = y ∨ x < y

source

theorem LO.FirstOrder.Arithmetic.add_zero' {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

x + 0 = x

source

theorem LO.FirstOrder.Arithmetic.add_assoc {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y z : M) :

x + y + z = x + (y + z)

source

theorem LO.FirstOrder.Arithmetic.add_comm {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y : M) :

x + y = y + x

source

theorem LO.FirstOrder.Arithmetic.add_eq_of_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y : M) :

x < y → ∃ (z : M), x + z = y

source

@[simp]

theorem LO.FirstOrder.Arithmetic.zero_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

0 ≤ x

source

theorem LO.FirstOrder.Arithmetic.zero_lt_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

0 < 1

source

theorem LO.FirstOrder.Arithmetic.one_le_of_zero_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

0 < x → 1 ≤ x

source

theorem LO.FirstOrder.Arithmetic.add_lt_add {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y z : M) :

x < y → x + z < y + z

source

theorem LO.FirstOrder.Arithmetic.mul_zero' {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

x * 0 = 0

source

theorem LO.FirstOrder.Arithmetic.mul_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

x * 1 = x

source

theorem LO.FirstOrder.Arithmetic.mul_assoc {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y z : M) :

x * y * z = x * (y * z)

source

theorem LO.FirstOrder.Arithmetic.mul_comm {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y : M) :

x * y = y * x

source

theorem LO.FirstOrder.Arithmetic.mul_lt_mul {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y z : M) :

x < y → 0 < z → x * z < y * z

source

theorem LO.FirstOrder.Arithmetic.mul_add_distr {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y z : M) :

x * (y + z) = x * y + x * z

source

theorem LO.FirstOrder.Arithmetic.lt_irrefl {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

¬x < x

source

theorem LO.FirstOrder.Arithmetic.lt_trans {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y z : M) :

x < y → y < z → x < z

source

theorem LO.FirstOrder.Arithmetic.lt_tri {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x y : M) :

x < y ∨ x = y ∨ y < x

source

@[implicit_reducible]

def LO.FirstOrder.Arithmetic.instAddCommMonoid_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

AddCommMonoid M

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implicit_reducible]

def LO.FirstOrder.Arithmetic.instCommMonoid_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

CommMonoid M

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implicit_reducible]

noncomputable def LO.FirstOrder.Arithmetic.instLinearOrder_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

LinearOrder M

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem LO.FirstOrder.Arithmetic.zero_mul {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

0 * x = 0

source

@[implicit_reducible]

def LO.FirstOrder.Arithmetic.instCommSemiring_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

CommSemiring M

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem LO.FirstOrder.Arithmetic.instIsStrictOrderedRing_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

IsStrictOrderedRing M

source

theorem LO.FirstOrder.Arithmetic.instCanonicallyOrderedAdd_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

CanonicallyOrderedAdd M

source

theorem LO.FirstOrder.Arithmetic.instIsOrderedAddMonoid_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

IsOrderedAddMonoid M

source

theorem LO.FirstOrder.Arithmetic.numeral_eq_natCast_app {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (n : ℕ) :

ORingStructure.numeral n = ↑n

source

theorem LO.FirstOrder.Arithmetic.numeral_eq_natCast {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

ORingStructure.numeral = Nat.cast

source

theorem LO.FirstOrder.Arithmetic.not_neg {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

¬x < 0

source

theorem LO.FirstOrder.Arithmetic.eq_succ_of_pos {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {x : M} (h : 0 < x) :

∃ (y : M), x = y + 1

source

theorem LO.FirstOrder.Arithmetic.le_iff_lt_succ {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {x y : M} :

x ≤ y ↔ x < y + 1

source

theorem LO.FirstOrder.Arithmetic.eq_nat_of_lt_nat {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {n : ℕ} {x : M} :

x < ↑n → ∃ (m : ℕ), x = ↑m

source

theorem LO.FirstOrder.Arithmetic.eq_nat_of_le_nat {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {n : ℕ} {x : M} :

x ≤ ↑n → ∃ (m : ℕ), x = ↑m

source

instance LO.FirstOrder.Arithmetic.models_R0_of_models_PeanoMinus {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

M↓[ℒₒᵣ ] ⊧* 𝗥₀

source

instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryR0PeanoMinus :

𝗥₀ ⪯ 𝗣𝗔⁻

source

instance LO.FirstOrder.Arithmetic.models_RobinsonQ_of_models_PeanoMinus {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

M↓[ℒₒᵣ ] ⊧* 𝗤

source

instance LO.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryRobinsonQPeanoMinus :

𝗤 ⪯ 𝗣𝗔⁻

source

@[simp]

theorem LO.FirstOrder.Arithmetic.numeral_two_eq_two {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

ORingStructure.numeral 2 = 2

source

@[simp]

theorem LO.FirstOrder.Arithmetic.numeral_three_eq_three {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

ORingStructure.numeral 3 = 3

source

@[simp]

theorem LO.FirstOrder.Arithmetic.numeral_four_eq_four {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

ORingStructure.numeral 4 = 4

source

theorem LO.FirstOrder.Arithmetic.lt_succ_iff_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {x y : M} :

x < y + 1 ↔ x ≤ y

source

theorem LO.FirstOrder.Arithmetic.lt_iff_succ_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : M} :

a < b ↔ a + 1 ≤ b

source

theorem LO.FirstOrder.Arithmetic.succ_le_iff_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : M} :

a + 1 ≤ b ↔ a < b

source

theorem LO.FirstOrder.Arithmetic.pos_iff_one_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

0 < a ↔ 1 ≤ a

source

theorem LO.FirstOrder.Arithmetic.one_lt_iff_two_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

1 < a ↔ 2 ≤ a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.not_nonpos {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a : M) :

¬a < 0

source

theorem LO.FirstOrder.Arithmetic.lt_two_iff_le_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

a < 2 ↔ a ≤ 1

source

@[simp]

theorem LO.FirstOrder.Arithmetic.lt_one_iff_eq_zero {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

a < 1 ↔ a = 0

source

theorem LO.FirstOrder.Arithmetic.le_one_iff_eq_zero_or_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

a ≤ 1 ↔ a = 0 ∨ a = 1

source

theorem LO.FirstOrder.Arithmetic.le_two_iff_eq_zero_or_one_or_two {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

a ≤ 2 ↔ a = 0 ∨ a = 1 ∨ a = 2

source

theorem LO.FirstOrder.Arithmetic.le_three_iff_eq_zero_or_one_or_two_or_three {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

a ≤ 3 ↔ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3

source

theorem LO.FirstOrder.Arithmetic.two_mul_two_eq_four {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

2 * 2 = 4

source

theorem LO.FirstOrder.Arithmetic.two_pow_two_eq_four {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

2 ^ 2 = 4

source

theorem LO.FirstOrder.Arithmetic.two_pos {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

0 < 2

source

@[simp]

theorem LO.FirstOrder.Arithmetic.le_mul_self {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a : M) :

a ≤ a * a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.le_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a : M) :

a ≤ a ^ 2

source

@[simp]

theorem LO.FirstOrder.Arithmetic.sq_le_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : M} :

a ^ 2 ≤ b ^ 2 ↔ a ≤ b

source

@[simp]

theorem LO.FirstOrder.Arithmetic.sq_lt_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : M} :

a ^ 2 < b ^ 2 ↔ a < b

source

theorem LO.FirstOrder.Arithmetic.le_mul_of_pos_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : M} (h : 0 < b) :

a ≤ a * b

source

theorem LO.FirstOrder.Arithmetic.le_mul_of_pos_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : M} (h : 0 < b) :

a ≤ b * a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.le_two_mul_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

a ≤ 2 * a

source

theorem LO.FirstOrder.Arithmetic.lt_mul_of_pos_of_one_lt_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : M} (pos : 0 < a) (h : 1 < b) :

a < a * b

source

theorem LO.FirstOrder.Arithmetic.lt_mul_of_pos_of_one_lt_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : M} (pos : 0 < a) (h : 1 < b) :

a < b * a

source

theorem LO.FirstOrder.Arithmetic.mul_le_mul_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : M} (h : b ≤ c) :

a * b ≤ a * c

source

theorem LO.FirstOrder.Arithmetic.mul_le_mul_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : M} (h : b ≤ c) :

b * a ≤ c * a

source

theorem LO.FirstOrder.Arithmetic.lt_of_mul_lt_mul_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : M} (h : a * b < a * c) :

b < c

source

theorem LO.FirstOrder.Arithmetic.lt_of_mul_lt_mul_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : M} (h : b * a < c * a) :

b < c

source

theorem LO.FirstOrder.Arithmetic.pow_three {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

x ^ 3 = x * x * x

source

theorem LO.FirstOrder.Arithmetic.pow_four {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

x ^ 4 = x * x * x * x

source

theorem LO.FirstOrder.Arithmetic.pow_four_eq_sq_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

x ^ 4 = (x ^ 2) ^ 2

source

theorem LO.FirstOrder.Arithmetic.instCovariantClassHMulLe_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

source

theorem LO.FirstOrder.Arithmetic.instCovariantClassHAddLe_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2

source

theorem LO.FirstOrder.Arithmetic.instCovariantClassSwapHMulLe_foundation {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

source

@[simp]

theorem LO.FirstOrder.Arithmetic.one_lt_mul_self_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

1 < a * a ↔ 1 < a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.opos_lt_sq_pos_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

0 < a ^ 2 ↔ 0 < a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.one_lt_sq_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

1 < a ^ 2 ↔ 1 < a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.mul_self_eq_one_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

a * a = 1 ↔ a = 1

source

@[simp]

theorem LO.FirstOrder.Arithmetic.sq_eq_one_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} :

a ^ 2 = 1 ↔ a = 1

source

theorem LO.FirstOrder.Arithmetic.lt_square_of_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} (pos : 1 < a) :

a < a ^ 2

source

theorem LO.FirstOrder.Arithmetic.two_mul_le_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {i : M} (h : 2 ≤ i) :

2 * i ≤ i ^ 2

source

theorem LO.FirstOrder.Arithmetic.two_mul_le_sq_add_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (i : M) :

2 * i ≤ i ^ 2 + 1

source

theorem LO.FirstOrder.Arithmetic.two_mul_lt_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {i : M} (h : 2 < i) :

2 * i < i ^ 2

source

theorem LO.FirstOrder.Arithmetic.succ_le_double_of_pos {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : M} (h : 0 < a) :

a + 1 ≤ 2 * a

source

theorem LO.FirstOrder.Arithmetic.two_mul_add_one_lt_two_mul_of_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : M} (h : a < b) :

2 * a + 1 < 2 * b

source

@[simp]

theorem LO.FirstOrder.Arithmetic.le_add_add_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a b c : M) :

a ≤ a + b + c

source

@[simp]

theorem LO.FirstOrder.Arithmetic.le_add_add_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a b c : M) :

b ≤ a + b + c

source

theorem LO.FirstOrder.Arithmetic.add_le_cancel {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a : M) :

AddLECancellable a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.val_npow {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (k : ℕ) (a : M) :

Semiterm.Operator.val ![a] (Semiterm.Operator.npow ℒₒᵣ k) = a ^ k

source

instance LO.FirstOrder.Arithmetic.instMonotoneORing {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

Structure.Monotone ℒₒᵣ M

source

@[simp]

theorem LO.FirstOrder.Arithmetic.zero_ne_add_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : M) :

0 ≠ x + 1

source

@[simp]

theorem LO.FirstOrder.Arithmetic.nat_cast_inj {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {n m : ℕ} :

↑n = ↑m ↔ n = m

source

@[simp]

theorem LO.FirstOrder.Arithmetic.coe_coe_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {n m : ℕ} :

↑n < ↑m ↔ n < m

source

theorem LO.FirstOrder.Arithmetic.coe_add_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (x : ℕ) :

↑(x + 1) = ↑x + 1

source

theorem LO.FirstOrder.Arithmetic.eq_fin_of_lt_nat {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {n : ℕ} {x : M} (hx : x < ↑n) :

∃ (i : Fin n), x = ↑↑i

source

@[simp]

theorem LO.FirstOrder.Arithmetic.eval_ballLTSucc' {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {ξ : Type u_2} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {t : ArithmeticSemiterm ξ n} {φ : ArithmeticSemiformula ξ (n + 1)} :

(Semiformula.Eval e ε) (Semiformula.ballLTSucc t φ) ↔ ∀ x ≤ Semiterm.val e ε t, (Semiformula.Eval (x :> e) ε) φ

source

@[simp]

theorem LO.FirstOrder.Arithmetic.eval_bexsLTSucc' {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {ξ : Type u_2} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {t : ArithmeticSemiterm ξ n} {φ : ArithmeticSemiformula ξ (n + 1)} :

(Semiformula.Eval e ε) (Semiformula.bexsLTSucc t φ) ↔ ∃ x ≤ Semiterm.val e ε t, (Semiformula.Eval (x :> e) ε) φ

source

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.natCast (M : Type u_1) [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

NatCast M

Equations

LO.FirstOrder.Arithmetic.natCast M = inferInstance

Instances For

source

@[simp]

theorem LO.FirstOrder.Arithmetic.natCast_nat (n : ℕ) :

↑n = n

source

instance LO.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryR0PeanoMinus :

𝗥₀ ⪱ 𝗣𝗔⁻

source

instance LO.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrR0 (M : Type u_2) [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

M↓[ℒₒᵣ ] ⊧* 𝗥₀

Documentation

Foundation.FirstOrder.Arithmetic.PeanoMinus.Basic

Theory $\mathsf{PA^-}$ #