Documentation

Logic.FirstOrder.Arith.PeanoMinus

def LO.Arith.instLE_logic {M : Type u_1} [LO.ORingStruc M] :

LE M

Equations

LO.Arith.instLE_logic = { le := fun (x y : M) => x = y ∨ x < y }

theorem LO.Arith.le_def {M : Type u_1} [LO.ORingStruc M] {x : M} {y : M} :

x ≤ y ↔ x = y ∨ x < y

theorem LO.Arith.add_zero {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

x + 0 = x

theorem LO.Arith.add_assoc {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :

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

theorem LO.Arith.add_comm {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) :

x + y = y + x

theorem LO.Arith.add_eq_of_lt {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) :

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

@[simp]

theorem LO.Arith.zero_le {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

0 ≤ x

theorem LO.Arith.zero_lt_one {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

0 < 1

theorem LO.Arith.one_le_of_zero_lt {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

0 < x → 1 ≤ x

theorem LO.Arith.add_lt_add {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :

x < y → x + z < y + z

theorem LO.Arith.mul_zero {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

x * 0 = 0

theorem LO.Arith.mul_one {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

x * 1 = x

theorem LO.Arith.mul_assoc {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :

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

theorem LO.Arith.mul_comm {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) :

x * y = y * x

theorem LO.Arith.mul_lt_mul {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :

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

theorem LO.Arith.distr {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :

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

theorem LO.Arith.lt_irrefl {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

¬x < x

theorem LO.Arith.lt_trans {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) (z : M) :

x < y → y < z → x < z

theorem LO.Arith.lt_tri {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) (y : M) :

x < y ∨ x = y ∨ y < x

def LO.Arith.instAddCommMonoid_logic {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

AddCommMonoid M

Equations

LO.Arith.instAddCommMonoid_logic = AddCommMonoid.mk ⋯

def LO.Arith.instCommMonoid_logic {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

Equations

LO.Arith.instCommMonoid_logic = CommMonoid.mk ⋯

def LO.Arith.instLinearOrder_logic {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

Equations

LO.Arith.instLinearOrder_logic = LinearOrder.mk ⋯ (fun (x x_1 : M) => Classical.dec ((fun (x x_2 : M) => x ≤ x_2) x x_1)) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

theorem LO.Arith.zero_mul {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

0 * x = 0

def LO.Arith.instLinearOrderedCommSemiring_logic {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

LinearOrderedCommSemiring M

Equations

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

def LO.Arith.instCanonicallyOrderedAddCommMonoid_logic {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :

CanonicallyOrderedAddCommMonoid M

Equations

LO.Arith.instCanonicallyOrderedAddCommMonoid_logic = CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

theorem LO.Arith.numeral_eq_natCast {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (n : ℕ) :

LO.ORingStruc.numeral n = ↑n

theorem LO.Arith.not_neg {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x : M) :

¬x < 0

theorem LO.Arith.eq_succ_of_pos {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x : M} (h : 0 < x) :

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

theorem LO.Arith.le_iff_lt_succ {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {x : M} {y : M} :

x ≤ y ↔ x < y + 1

theorem LO.Arith.eq_nat_of_lt_nat {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {n : ℕ} {x : M} :

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

instance LO.FirstOrder.Arith.CobhamR0.subTheoryPAMinus :

𝐑₀ ≼ 𝐏𝐀⁻

Equations

LO.FirstOrder.Arith.CobhamR0.subTheoryPAMinus = LO.System.Subtheory.ofAxm! @LO.FirstOrder.Arith.CobhamR0.subTheoryPAMinus.proof_1