IOpen

theorem LO.Arith.open_induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {P : V → Prop} (hP : ∃ (p : FirstOrder.Semiformula ℒₒᵣ V 1), p.Open ∧ ∀ (x : V), P x ↔ (FirstOrder.Semiformula.Evalm V ![x] id) p) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) : P x

theorem LO.Arith.open_leastNumber {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {P : V → Prop} (hP : ∃ (p : FirstOrder.Semiformula ℒₒᵣ V 1), p.Open ∧ ∀ (x : V), P x ↔ (FirstOrder.Semiformula.Evalm V ![x] id) p) (zero : P 0) {a : V} (counterex : ¬P a) : ∃ (x : V), P x ∧ ¬P (x + 1)

theorem LO.Arith.div_exists_unique_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) : ∃! u : V, b * u ≤ a ∧ a < b * (u + 1)

theorem LO.Arith.div_exists_unique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : ∃! u : V, (0 < b → b * u ≤ a ∧ a < b * (u + 1)) ∧ (b = 0 → u = 0)

@[implicit_reducible]

noncomputable def LO.Arith.instDivV {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : Div V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.instDivV = { div := fun (a b : V) => Classical.choose! ⋯ }

theorem LO.Arith.mul_div_le_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {b : V} (a : V) (h : 0 < b) : b * (a / b) ≤ a

theorem LO.Arith.lt_mul_div_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {b : V} (a : V) (h : 0 < b) : a < b * (a / b + 1)

theorem LO.Arith.eq_mul_div_add_of_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (hb : 0 < b) : ∃ r < b, a = b * (a / b) + r

@[simp]

theorem LO.Arith.div_spec_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a / 0 = 0

theorem LO.Arith.div_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b c : V} : c = a / b ↔ (0 < b → b * c ≤ a ∧ a < b * (c + 1)) ∧ (b = 0 → c = 0)

def LO.FirstOrder.Arith.divDef : 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.div_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₂ fun (x1 x2 : V) => x1 / x2 via FirstOrder.Arith.divDef

@[simp]

theorem LO.Arith.div_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.divDef) ↔ v 0 = v 1 / v 2

theorem LO.Arith.div_spec_of_pos' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {b : V} (a : V) (h : 0 < b) : ∃ v < b, a = a / b * b + v

theorem LO.Arith.div_eq_of {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {c a b : V} (hb : b * c ≤ a) (ha : a < b * (c + 1)) : a / b = c

theorem LO.Arith.div_mul_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) {r : V} (hr : r < b) : (a * b + r) / b = a

theorem LO.Arith.div_mul_add' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) {r : V} (hr : r < b) : (b * a + r) / b = a

@[simp]

theorem LO.Arith.zero_div {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : 0 / a = 0

theorem LO.Arith.div_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b c : V) : a / (b * c) = a / b / c

@[simp]

theorem LO.Arith.mul_div_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : b * (a / b) ≤ a

@[simp]

theorem LO.Arith.div_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : a / b ≤ a

instance LO.Arith.div_polybounded {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Bounded₂ fun (x1 x2 : V) => x1 / x2

instance LO.Arith.div_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₂ fun (x1 x2 : V) => x1 / x2

@[simp]

theorem LO.Arith.div_mul_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : a / b * b ≤ a

theorem LO.Arith.lt_mul_div {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) : a < b * (a / b + 1)

@[simp]

theorem LO.Arith.div_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a / 1 = a

theorem LO.Arith.div_add_mul_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a c : V) {b : V} (pos : 0 < b) : (a + c * b) / b = a / b + c

theorem LO.Arith.div_add_mul_self' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a c : V) {b : V} (pos : 0 < b) : (a + b * c) / b = a / b + c

theorem LO.Arith.div_mul_add_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a c : V) {b : V} (pos : 0 < b) : (a * b + c) / b = a + c / b

theorem LO.Arith.div_mul_add_self' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a c : V) {b : V} (pos : 0 < b) : (b * a + c) / b = a + c / b

@[simp]

theorem LO.Arith.div_mul_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) : a * b / b = a

theorem LO.Arith.div_mul_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) : b * a / b = a

@[simp]

theorem LO.Arith.div_eq_zero_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (b : V) {a : V} (h : a < b) : a / b = 0

@[simp]

theorem LO.Arith.div_sq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a ^ 2 / a = a

@[simp]

theorem LO.Arith.div_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} (hx : 0 < a) : a / a = 1

@[simp]

theorem LO.Arith.div_mul' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) : b * a / b = a

@[simp]

theorem LO.Arith.div_add_self_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} (pos : 0 < a) (b : V) : (a + b) / a = 1 + b / a

@[simp]

theorem LO.Arith.div_add_self_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) : (a + b) / b = a / b + 1

theorem LO.Arith.mul_div_self_of_dvd {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} : a * (b / a) = b ↔ a ∣ b

theorem LO.Arith.div_lt_of_pos_of_one_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} (ha : 0 < a) (hb : 1 < b) : a / b < a

theorem LO.Arith.le_two_mul_div_two_add_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a ≤ 2 * (a / 2) + 1

theorem LO.Arith.div_monotone {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} (h : a ≤ b) (c : V) : a / c ≤ b / c

theorem LO.Arith.div_lt_of_lt_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b c : V} (h : a < b * c) : a / c < b

theorem LO.Arith.div_cancel_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {c : V} (pos : 0 < c) (a b : V) : c * a / (c * b) = a / b

theorem LO.Arith.div_cancel_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {c : V} (pos : 0 < c) (a b : V) : a * c / (b * c) = a / b

@[simp]

theorem LO.Arith.two_mul_add_one_div_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : (2 * a + 1) / 2 = a

noncomputable def LO.Arith.rem {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.rem a b = a - b * (a / b)

@[implicit_reducible]

noncomputable def LO.Arith.instModV {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : Mod V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.instModV = { mod := LO.Arith.rem }

theorem LO.Arith.mod_def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : a % b = a - b * (a / b)

def LO.FirstOrder.Arith.remDef : 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.rem_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b c : V) : a = b % c ↔ ∃ x ≤ b, x = b / c ∧ a = b - c * x

theorem LO.Arith.rem_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₂ fun (x1 x2 : V) => x1 % x2 via FirstOrder.Arith.remDef

@[simp]

theorem LO.Arith.rem_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.remDef) ↔ v 0 = v 1 % v 2

instance LO.Arith.rem_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₂ fun (x1 x2 : V) => x1 % x2

theorem LO.Arith.div_add_mod {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : b * (a / b) + a % b = a

@[simp]

theorem LO.Arith.mod_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a % 0 = a

@[simp]

theorem LO.Arith.zero_mod {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : 0 % a = 0

@[simp]

theorem LO.Arith.mod_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a % a = 0

theorem LO.Arith.mod_mul_add_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) {r : V} (hr : r < b) : (a * b + r) % b = r

@[simp]

theorem LO.Arith.mod_mul_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {b : V} (a c : V) (pos : 0 < b) : (a * b + c) % b = c % b

@[simp]

theorem LO.Arith.mod_add_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {c : V} (a b : V) (pos : 0 < c) : (a + b * c) % c = a % c

@[simp]

theorem LO.Arith.mod_add_mul' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {c : V} (a b : V) (pos : 0 < c) : (a + c * b) % c = a % c

@[simp]

theorem LO.Arith.mod_mul_add' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {b : V} (a c : V) (pos : 0 < b) : (b * a + c) % b = c % b

@[simp]

theorem LO.Arith.mod_mul_self_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : a * b % b = 0

@[simp]

theorem LO.Arith.mod_mul_self_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : b * a % b = 0

@[simp]

theorem LO.Arith.mod_eq_self_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} (h : a < b) : a % b = a

@[simp]

theorem LO.Arith.mod_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b : V} (pos : 0 < b) : a % b < b

@[simp]

theorem LO.Arith.mod_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : a % b ≤ a

instance LO.Arith.mod_polybounded {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Bounded₂ fun (x1 x2 : V) => x1 % x2

theorem LO.Arith.mod_eq_zero_iff_dvd {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} : b % a = 0 ↔ a ∣ b

@[simp]

theorem LO.Arith.mod_add_remove_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} (pos : 0 < b) : (a + b) % b = a % b

theorem LO.Arith.mod_add_remove_right_of_dvd {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b m : V} (h : m ∣ b) (pos : 0 < m) : (a + b) % m = a % m

@[simp]

theorem LO.Arith.mod_add_remove_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} (pos : 0 < a) : (a + b) % a = b % a

theorem LO.Arith.mod_add_remove_left_of_dvd {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b m : V} (h : m ∣ a) (pos : 0 < m) : (a + b) % m = b % m

theorem LO.Arith.mod_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b m : V} (pos : 0 < m) : (a + b) % m = (a % m + b % m) % m

theorem LO.Arith.mod_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b m : V} (pos : 0 < m) : a * b % m = a % m * (b % m) % m

@[simp]

theorem LO.Arith.mod_div {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : a % b / b = 0

@[simp]

theorem LO.Arith.mod_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a % 1 = 0

theorem LO.Arith.mod_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a % 2 = 0 ∨ a % 2 = 1

@[simp]

theorem LO.Arith.mod_two_not_zero_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} : ¬a % 2 = 0 ↔ a % 2 = 1

@[simp]

theorem LO.Arith.mod_two_not_one_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} : ¬a % 2 = 1 ↔ a % 2 = 0

theorem LO.Arith.two_dvd_mul {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} : 2 ∣ a * b → 2 ∣ a ∨ 2 ∣ b

theorem LO.Arith.even_or_odd {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : ∃ (x : V), a = 2 * x ∨ a = 2 * x + 1

theorem LO.Arith.even_or_odd' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1

theorem LO.Arith.two_prime {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : Prime 2

theorem LO.Arith.sqrt_exists_unique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : ∃! x : V, x * x ≤ a ∧ a < (x + 1) * (x + 1)

noncomputable def LO.Arith.sqrt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• √a = Classical.choose! ⋯

def LO.Arith.«term√_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.«term√_» = Lean.ParserDescr.node `LO.Arith.«term√_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "√") (Lean.ParserDescr.cat `term 75))

@[simp]

theorem LO.Arith.sqrt_spec_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : √a * √a ≤ a

@[simp]

theorem LO.Arith.sqrt_spec_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a < (√a + 1) * (√a + 1)

theorem LO.Arith.sqrt_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} : b = √a ↔ b * b ≤ a ∧ a < (b + 1) * (b + 1)

def LO.FirstOrder.Arith.sqrtDef : 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.sqrt_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₁ fun (a : V) => √a via FirstOrder.Arith.sqrtDef

@[simp]

theorem LO.Arith.sqrt_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.sqrtDef) ↔ v 0 = √v 1

instance LO.Arith.sqrt_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₁ fun (x : V) => √x

theorem LO.Arith.eq_sqrt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (x a : V) : x * x ≤ a ∧ a < (x + 1) * (x + 1) → x = √a

theorem LO.Arith.sqrt_eq_of_le_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {x a : V} (le : x * x ≤ a) (lt : a < (x + 1) * (x + 1)) : √a = x

theorem LO.Arith.sqrt_eq_of_le_of_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {x a : V} (le : x * x ≤ a) (h : a ≤ x * x + 2 * x) : √a = x

@[simp]

theorem LO.Arith.sq_sqrt_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : (√a) ^ 2 ≤ a

@[simp]

theorem LO.Arith.sqrt_lt_sq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a < (√a + 1) ^ 2

@[simp]

theorem LO.Arith.sqrt_mul_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : √(a * a) = a

@[simp]

theorem LO.Arith.sqrt_sq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : √a ^ 2 = a

@[simp]

theorem LO.Arith.sqrt_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : √0 = 0

@[simp]

theorem LO.Arith.sqrt_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : √1 = 1

theorem LO.Arith.sqrt_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : √2 = 1

theorem LO.Arith.sqrt_three {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : √3 = 1

@[simp]

theorem LO.Arith.sqrt_four {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : √4 = 2

@[simp]

theorem LO.Arith.two_ne_square {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : 2 ≠ a ^ 2

@[simp]

theorem LO.Arith.sqrt_le_add {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : a ≤ √a * √a + 2 * √a

@[simp]

theorem LO.Arith.sqrt_le_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : √a ≤ a

instance LO.Arith.instBounded₁Sqrt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Bounded₁ fun (x : V) => √x

theorem LO.Arith.sqrt_lt_self_of_one_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} (h : 1 < a) : √a < a

theorem LO.Arith.sqrt_le_of_le_sq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} : a ≤ b ^ 2 → √a ≤ b

theorem LO.Arith.sq_lt_of_lt_sqrt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b : V} : a < √b → a ^ 2 < b

noncomputable def LO.Arith.pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• ⟪a, b⟫ = if a < b then b * b + a else a * a + a + b

def LO.Arith.«term⟪_⟫» : Lean.ParserDescr

!⟪x, y, z, ...⟫ notation for Seq

Equations

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

def LO.Arith.pairUnexpander : Lean.PrettyPrinter.Unexpander

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.pair_graph {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a b c : V} : c = ⟪a, b⟫ ↔ a < b ∧ c = b * b + a ∨ b ≤ a ∧ c = a * a + a + b

def LO.FirstOrder.Arith.pairDef : 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.pair_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₂ fun (a b : V) => ⟪a, b⟫ via FirstOrder.Arith.pairDef

@[simp]

theorem LO.Arith.pair_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.pairDef) ↔ v 0 = ⟪v 1, v 2⟫

instance LO.Arith.pair_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₂ pair

instance LO.Arith.instBounded₂Pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Bounded₂ pair

noncomputable def LO.Arith.unpair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : V × V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.unpair a = if a - √a * √a < √a then (a - √a * √a, √a) else (√a, a - √a * √a - √a)

@[reducible, inline]

noncomputable abbrev LO.Arith.pi₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• π₁ a = (LO.Arith.unpair a).1

@[reducible, inline]

noncomputable abbrev LO.Arith.pi₂ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• π₂ a = (LO.Arith.unpair a).2

def LO.Arith.termπ₁_ : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.termπ₁_ = Lean.ParserDescr.node `LO.Arith.termπ₁_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "π₁") (Lean.ParserDescr.cat `term 80))

def LO.Arith.termπ₂_ : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.termπ₂_ = Lean.ParserDescr.node `LO.Arith.termπ₂_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "π₂") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem LO.Arith.pair_unpair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : ⟪π₁ a, π₂ a⟫ = a

@[simp]

theorem LO.Arith.unpair_pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : unpair ⟪a, b⟫ = (a, b)

@[simp]

theorem LO.Arith.pi₁_pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : π₁⟪a, b⟫ = a

@[simp]

theorem LO.Arith.pi₂_pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : π₂⟪a, b⟫ = b

noncomputable def LO.Arith.pairEquiv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : V × V ≃ V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.pairEquiv = { toFun := Function.uncurry LO.Arith.pair, invFun := LO.Arith.unpair, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LO.Arith.pi₁_le_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : π₁ a ≤ a

@[simp]

theorem LO.Arith.pi₂_le_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) : π₂ a ≤ a

@[simp]

theorem LO.Arith.le_pair_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : a ≤ ⟪a, b⟫

@[simp]

theorem LO.Arith.le_pair_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : b ≤ ⟪a, b⟫

@[simp]

theorem LO.Arith.lt_pair_left_of_pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a : V} (pos : 0 < a) (b : V) : a < ⟪a, b⟫

instance LO.Arith.instBounded₁Pi₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Bounded₁ pi₁

instance LO.Arith.instBounded₁Pi₂ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Bounded₁ pi₂

def LO.FirstOrder.Arith.pi₁Def : Sg0.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.pi₂Def : 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.pi₁_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₁ pi₁ via FirstOrder.Arith.pi₁Def

@[simp]

theorem LO.Arith.pi₁_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.pi₁Def) ↔ v 0 = π₁ v 1

instance LO.Arith.pi₁_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₁ pi₁

theorem LO.Arith.pi₂_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₁ pi₂ via FirstOrder.Arith.pi₂Def

@[simp]

theorem LO.Arith.pi₂_defined_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.pi₂Def) ↔ v 0 = π₂ v 1

instance LO.Arith.pi₂_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₁ pi₂

theorem LO.Arith.pair_lt_pair_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a₁ a₂ : V} (h : a₁ < a₂) (b : V) : ⟪a₁, b⟫ < ⟪a₂, b⟫

theorem LO.Arith.pair_le_pair_left {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a₁ a₂ : V} (h : a₁ ≤ a₂) (b : V) : ⟪a₁, b⟫ ≤ ⟪a₂, b⟫

theorem LO.Arith.pair_lt_pair_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b₁ b₂ : V} (h : b₁ < b₂) : ⟪a, b₁⟫ < ⟪a, b₂⟫

theorem LO.Arith.pair_le_pair_right {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a : V) {b₁ b₂ : V} (h : b₁ ≤ b₂) : ⟪a, b₁⟫ ≤ ⟪a, b₂⟫

theorem LO.Arith.pair_le_pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a₁ a₂ b₁ b₂ : V} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : ⟪a₁, b₁⟫ ≤ ⟪a₂, b₂⟫

theorem LO.Arith.pair_lt_pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a₁ a₂ b₁ b₂ : V} (ha : a₁ < a₂) (hb : b₁ < b₂) : ⟪a₁, b₁⟫ < ⟪a₂, b₂⟫

@[simp]

theorem LO.Arith.pair_polybound {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (a b : V) : ⟪a, b⟫ ≤ (a + b + 1) ^ 2

@[simp]

theorem LO.Arith.pair_ext_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {a₁ a₂ b₁ b₂ : V} : ⟪a₁, b₁⟫ = ⟪a₂, b₂⟫ ↔ a₁ = a₂ ∧ b₁ = b₂

def LO.FirstOrder.Arith.pair₃Def : Sg0.Semisentence 4

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.pair₄Def : Sg0.Semisentence 5

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.pair₅Def : Sg0.Semisentence 6

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.pair₆Def : Sg0.Semisentence 7

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.fegergreg (v : Fin 4 → ℕ) : v (Fin.succ 0).succ = v 2

theorem LO.Arith.fin4 {n : ℕ} : Fin.succ 2 = 3

@[simp]

theorem LO.Arith.Fin.succ_zero_eq_one'' {n : ℕ} : Fin.succ 0 = 1

@[simp]

theorem LO.Arith.Fin.succ_two_eq_three {n : ℕ} : Fin.succ 2 = 3

theorem LO.Arith.ss (v : Fin 4 → ℕ) : v (Fin.succ 0).succ = v 2

theorem LO.Arith.pair₃_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₃ fun (x1 x2 x3 : V) => ⟪x1, ⟪x2, x3⟫⟫ via FirstOrder.Arith.pair₃Def

@[simp]

theorem LO.Arith.eval_pair₃Def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 4 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.pair₃Def) ↔ v 0 = ⟪v 1, ⟪v 2, v 3⟫⟫

theorem LO.Arith.pair₄_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.Sg0-Function₄ fun (x1 x2 x3 x4 : V) => ⟪x1, ⟪x2, ⟪x3, x4⟫⟫⟫ via FirstOrder.Arith.pair₄Def

@[simp]

theorem LO.Arith.eval_pair₄Def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 5 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.pair₄Def) ↔ v 0 = ⟪v 1, ⟪v 2, ⟪v 3, v 4⟫⟫⟫

theorem LO.Arith.pair₅_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 5 → V) => ⟪v 0, ⟪v 1, ⟪v 2, ⟪v 3, v 4⟫⟫⟫⟫) FirstOrder.Arith.pair₅Def

@[simp]

theorem LO.Arith.eval_pair₅Def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 6 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.pair₅Def) ↔ v 0 = ⟪v 1, ⟪v 2, ⟪v 3, ⟪v 4, v 5⟫⟫⟫⟫

theorem LO.Arith.pair₆_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] : FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 6 → V) => ⟪v 0, ⟪v 1, ⟪v 2, ⟪v 3, ⟪v 4, v 5⟫⟫⟫⟫⟫) FirstOrder.Arith.pair₆Def

@[simp]

theorem LO.Arith.eval_pair₆Def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 7 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.pair₆Def) ↔ v 0 = ⟪v 1, ⟪v 2, ⟪v 3, ⟪v 4, ⟪v 5, v 6⟫⟫⟫⟫⟫

def LO.Arith.npair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {n : ℕ} (v : Fin n → V) : V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.npair x_2 = 0
• LO.Arith.npair v = ⟪v 0, LO.Arith.npair fun (x : Fin n) => v x.succ⟫

@[simp]

theorem LO.Arith.npair_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (v : Fin 0 → V) : npair v = 0

theorem LO.Arith.npair_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {n : ℕ} (x : V) (v : Fin n → V) : npair (x :> v) = ⟪x, npair v⟫

def LO.Arith.unNpair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {n : ℕ} : Fin n → V → V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.unNpair i x✝ = i.elim0
• LO.Arith.unNpair i x✝ = Fin.cases (π₁ x✝) (fun (i : Fin n) => LO.Arith.unNpair i (π₂ x✝)) i

@[simp]

theorem LO.Arith.unNpair_npair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {n : ℕ} (i : Fin n) (v : Fin n → V) : unNpair i (npair v) = v i

def LO.FirstOrder.Arith.unNpairDef {n : ℕ} (i : Fin n) : Sg0.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Arith.unNpairDef i = i.elim0

theorem LO.Arith.unNpair_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {n : ℕ} (i : Fin n) : FirstOrder.Arith.Sg0-Function₁ unNpair i via FirstOrder.Arith.unNpairDef i

@[simp]

theorem LO.Arith.eval_unNpairDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {n : ℕ} (i : Fin n) (v : Fin 2 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val (FirstOrder.Arith.unNpairDef i)) ↔ v 0 = unNpair i (v 1)

instance LO.Arith.unNpair_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] {n : ℕ} (i : Fin n) (Γ : FirstOrder.Arith.HierarchySymbol) : Γ-Function₁ unNpair i

theorem LO.Arith.hierarchy_polynomial_induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (Γ : Polarity) (m : ℕ) [V ⊧ₘ* FirstOrder.Theory.indScheme ℒₒᵣ (FirstOrder.Arith.Hierarchy Γ m)] {P : V → Prop} (hP : { Γ := Γ.coe, rank := m }-Predicate P) (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ (x : V), P x → P (2 * x + 1)) (x : V) : P x

theorem LO.Arith.hierarchy_polynomial_induction_oRing_sigma₀ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg0] {P : V → Prop} (hP : FirstOrder.Arith.Sg0-Predicate P) (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ (x : V), P x → P (2 * x + 1)) (x : V) : P x

theorem LO.Arith.hierarchy_polynomial_induction_oRing_sigma₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {P : V → Prop} (hP : FirstOrder.Arith.Sg1-Predicate P) (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ (x : V), P x → P (2 * x + 1)) (x : V) : P x

theorem LO.Arith.hierarchy_polynomial_induction_oRing_pi₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Pg1] {P : V → Prop} (hP : FirstOrder.Arith.Pg1-Predicate P) (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ (x : V), P x → P (2 * x + 1)) (x : V) : P x

theorem LO.Arith.nat_cast_pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (n m : ℕ) : ↑⟪n, m⟫ = ⟪↑n, ↑m⟫

theorem LO.Arith.nat_pair_eq (m n : ℕ) : ⟪n, m⟫ = Nat.pair n m

theorem LO.Arith.pair_coe_eq_coe_pair {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈open] (m n : ℕ) : ↑⟪n, m⟫ = ↑(Nat.pair n m)