PeanoMinus

theorem LO.Arith.sub_existsUnique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a b : V) : ∃! c : V, (a ≥ b → a = b + c) ∧ (a < b → c = 0)

noncomputable def LO.Arith.sub {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a b : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.sub a b = Classical.choose! ⋯

@[implicit_reducible]

noncomputable instance LO.Arith.instSubV {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : Sub V

Equations

• LO.Arith.instSubV = { sub := LO.Arith.sub }

theorem LO.Arith.sub_spec_of_ge {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (h : a ≥ b) : a = b + (a - b)

theorem LO.Arith.sub_spec_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (h : a < b) : a - b = 0

theorem LO.Arith.sub_eq_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b c : V} : c = a - b ↔ (a ≥ b → a = b + c) ∧ (a < b → c = 0)

@[simp]

theorem LO.Arith.sub_le_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a b : V) : a - b ≤ a

def LO.FirstOrder.Arith.subDef : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.sub_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : FirstOrder.Arith.Sg0-Function₂ fun (x1 x2 : V) => x1 - x2 via FirstOrder.Arith.subDef

@[simp]

theorem LO.Arith.sub_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.subDef) ↔ v 0 = v 1 - v 2

instance LO.Arith.sub_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (ℌ : FirstOrder.Arith.HierarchySymbol) : ℌ-Function₂ fun (x1 x2 : V) => x1 - x2

instance LO.Arith.sub_polybounded {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : FirstOrder.Arith.Bounded₂ fun (x1 x2 : V) => x1 - x2

@[simp]

theorem LO.Arith.sub_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) : a - a = 0

theorem LO.Arith.sub_spec_of_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (h : a ≤ b) : a - b = 0

theorem LO.Arith.sub_add_self_of_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (h : b ≤ a) : a - b + b = a

theorem LO.Arith.add_tsub_self_of_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (h : b ≤ a) : b + (a - b) = a

@[simp]

theorem LO.Arith.add_sub_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} : a + b - b = a

@[simp]

theorem LO.Arith.add_sub_self' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} : b + a - b = a

@[simp]

theorem LO.Arith.zero_sub {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) : 0 - a = 0

@[simp]

theorem LO.Arith.sub_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) : a - 0 = a

theorem LO.Arith.sub_remove_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b c : V} (e : a = b + c) : a - c = b

theorem LO.Arith.sub_sub {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b c : V} : a - b - c = a - (b + c)

@[simp]

theorem LO.Arith.pos_sub_iff_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} : 0 < a - b ↔ b < a

@[simp]

theorem LO.Arith.sub_eq_zero_iff_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} : a - b = 0 ↔ a ≤ b

instance LO.Arith.instOrderedSub_leanPool {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : OrderedSub V

theorem LO.Arith.zero_or_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) : a = 0 ∨ ∃ (a' : V), a = a' + 1

theorem LO.Arith.pred_lt_self_of_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} (h : 0 < a) : a - 1 < a

theorem LO.Arith.tsub_lt_iff_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b c : V} (h : b ≤ a) : a - b < c ↔ a < c + b

theorem LO.Arith.sub_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b c : V} (h : b ≤ a) : (a - b) * c = a * c - b * c

theorem LO.Arith.mul_sub {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b c : V} (h : b ≤ a) : c * (a - b) = c * a - c * b

theorem LO.Arith.add_sub_of_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {b c : V} (h : c ≤ b) (a : V) : a + b - c = a + (b - c)

theorem LO.Arith.sub_succ_add_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {x y : V} (h : y < x) (z : V) : x - (y + 1) + (z + 1) = x - y + z

theorem LO.Arith.le_sub_one_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (h : a < b) : a ≤ b - 1

theorem LO.Arith.le_mul_self_of_pos_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (hy : 0 < b) : a ≤ b * a

theorem LO.Arith.le_mul_self_of_pos_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (hy : 0 < b) : a ≤ a * b

theorem LO.Arith.dvd_iff_bounded {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} : a ∣ b ↔ ∃ c ≤ b, b = a * c

def LO.FirstOrder.Arith.dvd : Sg0.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.dvd_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : FirstOrder.Arith.Sg0-Relation fun (a b : V) => a ∣ b via FirstOrder.Arith.dvd

@[simp]

theorem LO.Arith.dvd_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.dvd) ↔ v 0 ∣ v 1

instance LO.Arith.dvd_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (ℌ : FirstOrder.Arith.HierarchySymbol) : ℌ-Relation fun (x1 x2 : V) => x1 ∣ x2

def LO.Arith.«firstOrderFormula_∣_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.le_of_dvd {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (h : 0 < b) : a ∣ b → a ≤ b

theorem LO.Arith.not_dvd_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} (pos : 0 < b) : b < a → ¬a ∣ b

theorem LO.Arith.dvd_antisymm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a b : V} : a ∣ b → b ∣ a → a = b

theorem LO.Arith.dvd_one_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} : a ∣ 1 ↔ a = 1

theorem LO.Arith.units_eq_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (u : Vˣ) : u = 1

@[simp]

theorem LO.Arith.unit_iff_eq_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {a : V} : IsUnit a ↔ a = 1

theorem LO.Arith.eq_one_or_eq_of_dvd_of_prime {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] {p a : V} (pp : Prime p) (hxp : a ∣ p) : a = 1 ∨ a = p

def LO.Arith.IsPrime {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (a : V) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.IsPrime a = (1 < a ∧ ∀ b ≤ a, b ∣ a → b = 1 ∨ b = a)

def LO.FirstOrder.Arith.isPrime : Sg0.Semisentence 1

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.isPrime_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : FirstOrder.Arith.Sg0-Predicate fun (a : V) => IsPrime a via FirstOrder.Arith.isPrime

def LO.FirstOrder.Arith.min : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.min_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : FirstOrder.Arith.Sg0-Function₂ min via FirstOrder.Arith.min

@[simp]

theorem LO.Arith.eval_minDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.min) ↔ v 0 = v 1 ⊓ v 2

instance LO.Arith.min_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (ℌ : FirstOrder.Arith.HierarchySymbol) : ℌ-Function₂ min

instance LO.Arith.min_polybounded {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : FirstOrder.Arith.Bounded₂ min

def LO.FirstOrder.Arith.max : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.max_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : FirstOrder.Arith.Sg0-Function₂ max via FirstOrder.Arith.max

@[simp]

theorem LO.Arith.eval_maxDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.max) ↔ v 0 = v 1 ⊔ v 2

instance LO.Arith.max_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] (Γ : FirstOrder.Arith.HierarchySymbol) : Γ-Function₂ max

instance LO.Arith.max_polybounded {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] : FirstOrder.Arith.Bounded₂ max