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

Equations

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

theorem LO.Arith.le_def {M : Type u_1} [ORingStruc M] {x y : M} : x ≤ y ↔ x = y ∨ x < y

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

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

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

theorem LO.Arith.add_eq_of_lt {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] (x y : M) : x < y → ∃ (z : M), x + z = y

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

• LO.Arith.instAddCommMonoid_foundation = AddCommMonoid.mk ⋯

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

Equations

• LO.Arith.instCommMonoid_foundation = CommMonoid.mk ⋯

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

Equations

• LO.Arith.instLinearOrder_foundation = LinearOrder.mk ⋯ (fun (x x_1 : M) => Classical.dec ((fun (x1 x2 : M) => x1 ≤ x2) x x_1)) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

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

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

Equations

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

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

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

Equations

• LO.Arith.instOrderedAddCommMonoid_foundation = OrderedAddCommMonoid.mk ⋯

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

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

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

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

theorem LO.Arith.eq_nat_of_lt_nat {M : Type u_1} [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_2