Basic properties of theory $\mathsf{IOpen}$

instance LO.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrPeanoMinus {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻

instance LO.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrInductionSchemeOpenNat {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : V↓[ℒₒᵣ] ⊧* InductionScheme ℒₒᵣ Semiformula.Open

theorem LO.FirstOrder.Arithmetic.succ_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {P : V → Prop} (hP : ∃ (φ : ArithmeticSemiformula V 1), Semiformula.Open φ ∧ ∀ (x : V), P x ↔ (Semiformula.Eval ![x] id) φ) (zero : P 0) (succ : ∀ (x : V), P x → P (x + 1)) (x : V) : P x

theorem LO.FirstOrder.Arithmetic.least_number {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {P : V → Prop} (hP : ∃ (φ : ArithmeticSemiformula V 1), Semiformula.Open φ ∧ ∀ (x : V), P x ↔ (Semiformula.Eval ![x] id) φ) (zero : P 0) {a : V} (counterex : ¬P a) : ∃ (x : V), P x ∧ ¬P (x + 1)

Division

theorem LO.FirstOrder.Arithmetic.div_exists_unique_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b : V} (pos : 0 < b) : ∃! u : V, b * u ≤ a ∧ a < b * (u + 1)

theorem LO.FirstOrder.Arithmetic.div_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : ∃! u : V, (0 < b → b * u ≤ a ∧ a < b * (u + 1)) ∧ (b = 0 → u = 0)

@[implicit_reducible]

noncomputable def LO.FirstOrder.Arithmetic.instDiv_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : Div V

Equations

• LO.FirstOrder.Arithmetic.instDiv_foundation = { div := fun (a b : V) => Classical.choose! ⋯ }

theorem LO.FirstOrder.Arithmetic.mul_div_le_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {b : V} (a : V) (h : 0 < b) : b * (a / b) ≤ a

theorem LO.FirstOrder.Arithmetic.lt_mul_div_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {b : V} (a : V) (h : 0 < b) : a < b * (a / b + 1)

theorem LO.FirstOrder.Arithmetic.eq_mul_div_add_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b : V} (hb : 0 < b) : ∃ r < b, a = b * (a / b) + r

@[simp]

theorem LO.FirstOrder.Arithmetic.div_spec_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a / 0 = 0

theorem LO.FirstOrder.Arithmetic.div_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b c : V} : c = a / b ↔ (0 < b → b * c ≤ a ∧ a < b * (c + 1)) ∧ (b = 0 → c = 0)

def LO.FirstOrder.Arithmetic.divDef : 𝚺₀.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.div_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₂ HDiv.hDiv via divDef

theorem LO.FirstOrder.Arithmetic.div_spec_of_pos' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {b : V} (a : V) (h : 0 < b) : ∃ v < b, a = a / b * b + v

theorem LO.FirstOrder.Arithmetic.div_eq_of {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {c a b : V} (hb : b * c ≤ a) (ha : a < b * (c + 1)) : a / b = c

theorem LO.FirstOrder.Arithmetic.div_mul_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) {r : V} (hr : r < b) : (a * b + r) / b = a

theorem LO.FirstOrder.Arithmetic.div_mul_add' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) {r : V} (hr : r < b) : (b * a + r) / b = a

@[simp]

theorem LO.FirstOrder.Arithmetic.zero_div {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : 0 / a = 0

theorem LO.FirstOrder.Arithmetic.div_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b c : V) : a / (b * c) = a / b / c

@[simp]

theorem LO.FirstOrder.Arithmetic.mul_div_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : b * (a / b) ≤ a

@[simp]

theorem LO.FirstOrder.Arithmetic.div_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : a / b ≤ a

instance LO.FirstOrder.Arithmetic.div_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : Bounded₂ fun (x1 x2 : V) => x1 / x2

instance LO.FirstOrder.Arithmetic.div_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₂ fun (x1 x2 : V) => x1 / x2

@[simp]

theorem LO.FirstOrder.Arithmetic.div_mul_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : a / b * b ≤ a

theorem LO.FirstOrder.Arithmetic.lt_mul_div {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b : V} (pos : 0 < b) : a < b * (a / b + 1)

@[simp]

theorem LO.FirstOrder.Arithmetic.div_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a / 1 = a

theorem LO.FirstOrder.Arithmetic.div_add_mul_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a c : V) {b : V} (pos : 0 < b) : (a + c * b) / b = a / b + c

theorem LO.FirstOrder.Arithmetic.div_add_mul_self' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a c : V) {b : V} (pos : 0 < b) : (a + b * c) / b = a / b + c

theorem LO.FirstOrder.Arithmetic.div_mul_add_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a c : V) {b : V} (pos : 0 < b) : (a * b + c) / b = a + c / b

theorem LO.FirstOrder.Arithmetic.div_mul_add_self' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a c : V) {b : V} (pos : 0 < b) : (b * a + c) / b = a + c / b

@[simp]

theorem LO.FirstOrder.Arithmetic.div_mul_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b : V} (pos : 0 < b) : a * b / b = a

@[simp]

theorem LO.FirstOrder.Arithmetic.div_mul_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b : V} (pos : 0 < b) : b * a / b = a

@[simp]

theorem LO.FirstOrder.Arithmetic.div_eq_zero_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (b : V) {a : V} (h : a < b) : a / b = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.div_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a ^ 2 / a = a

@[simp]

theorem LO.FirstOrder.Arithmetic.div_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} (hx : 0 < a) : a / a = 1

@[simp]

theorem LO.FirstOrder.Arithmetic.div_mul' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b : V} (pos : 0 < b) : b * a / b = a

@[simp]

theorem LO.FirstOrder.Arithmetic.div_add_self_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} (pos : 0 < a) (b : V) : (a + b) / a = 1 + b / a

@[simp]

theorem LO.FirstOrder.Arithmetic.div_add_self_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b : V} (pos : 0 < b) : (a + b) / b = a / b + 1

theorem LO.FirstOrder.Arithmetic.mul_div_self_of_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} : a * (b / a) = b ↔ a ∣ b

theorem LO.FirstOrder.Arithmetic.div_lt_of_pos_of_one_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} (ha : 0 < a) (hb : 1 < b) : a / b < a

theorem LO.FirstOrder.Arithmetic.le_two_mul_div_two_add_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a ≤ 2 * (a / 2) + 1

theorem LO.FirstOrder.Arithmetic.div_monotone {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} (h : a ≤ b) (c : V) : a / c ≤ b / c

theorem LO.FirstOrder.Arithmetic.div_lt_of_lt_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b c : V} (h : a < b * c) : a / c < b

theorem LO.FirstOrder.Arithmetic.div_cancel_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {c : V} (pos : 0 < c) (a b : V) : c * a / (c * b) = a / b

theorem LO.FirstOrder.Arithmetic.div_cancel_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {c : V} (pos : 0 < c) (a b : V) : a * c / (b * c) = a / b

@[simp]

theorem LO.FirstOrder.Arithmetic.two_mul_add_one_div_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : (2 * a + 1) / 2 = a

Remainder

noncomputable def LO.FirstOrder.Arithmetic.rem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : V

Equations

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

@[implicit_reducible]

noncomputable def LO.FirstOrder.Arithmetic.instMod_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : Mod V

Equations

• LO.FirstOrder.Arithmetic.instMod_foundation = { mod := LO.FirstOrder.Arithmetic.rem }

theorem LO.FirstOrder.Arithmetic.mod_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : a % b = a - b * (a / b)

def LO.FirstOrder.Arithmetic.remDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.FirstOrder.Arithmetic.rem_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b c : V) : a = b % c ↔ ∃ x ≤ b, x = b / c ∧ a = b - c * x

instance LO.FirstOrder.Arithmetic.rem_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₂ HMod.hMod via remDef

instance LO.FirstOrder.Arithmetic.rem_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₂ HMod.hMod

theorem LO.FirstOrder.Arithmetic.div_add_mod {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : b * (a / b) + a % b = a

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a % 0 = a

@[simp]

theorem LO.FirstOrder.Arithmetic.zero_mod {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : 0 % a = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a % a = 0

theorem LO.FirstOrder.Arithmetic.mod_mul_add_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) {r : V} (hr : r < b) : (a * b + r) % b = r

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_mul_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {b : V} (a c : V) (pos : 0 < b) : (a * b + c) % b = c % b

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_add_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {c : V} (a b : V) (pos : 0 < c) : (a + b * c) % c = a % c

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_add_mul' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {c : V} (a b : V) (pos : 0 < c) : (a + c * b) % c = a % c

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_mul_add' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {b : V} (a c : V) (pos : 0 < b) : (b * a + c) % b = c % b

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_mul_self_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : a * b % b = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_mul_self_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : b * a % b = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_eq_self_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} (h : a < b) : a % b = a

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b : V} (pos : 0 < b) : a % b < b

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : a % b ≤ a

instance LO.FirstOrder.Arithmetic.mod_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : Bounded₂ fun (x1 x2 : V) => x1 % x2

theorem LO.FirstOrder.Arithmetic.mod_eq_zero_iff_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} : b % a = 0 ↔ a ∣ b

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_add_remove_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} (pos : 0 < b) : (a + b) % b = a % b

theorem LO.FirstOrder.Arithmetic.mod_add_remove_right_of_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b m : V} (h : m ∣ b) (pos : 0 < m) : (a + b) % m = a % m

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_add_remove_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} (pos : 0 < a) : (a + b) % a = b % a

theorem LO.FirstOrder.Arithmetic.mod_add_remove_left_of_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b m : V} (h : m ∣ a) (pos : 0 < m) : (a + b) % m = b % m

theorem LO.FirstOrder.Arithmetic.mod_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b m : V} (pos : 0 < m) : (a + b) % m = (a % m + b % m) % m

theorem LO.FirstOrder.Arithmetic.mod_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b m : V} (pos : 0 < m) : a * b % m = a % m * (b % m) % m

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_div {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : a % b / b = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a % 1 = 0

theorem LO.FirstOrder.Arithmetic.mod_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a % 2 = 0 ∨ a % 2 = 1

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_two_not_zero_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} : ¬a % 2 = 0 ↔ a % 2 = 1

@[simp]

theorem LO.FirstOrder.Arithmetic.mod_two_not_one_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} : ¬a % 2 = 1 ↔ a % 2 = 0

theorem LO.FirstOrder.Arithmetic.two_dvd_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} : 2 ∣ a * b → 2 ∣ a ∨ 2 ∣ b

theorem LO.FirstOrder.Arithmetic.even_or_odd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : ∃ (x : V), a = 2 * x ∨ a = 2 * x + 1

theorem LO.FirstOrder.Arithmetic.even_or_odd' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1

theorem LO.FirstOrder.Arithmetic.two_prime {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : Prime 2

Square root

theorem LO.FirstOrder.Arithmetic.sqrt_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : ∃! x : V, x * x ≤ a ∧ a < (x + 1) * (x + 1)

noncomputable def LO.FirstOrder.Arithmetic.sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : V

Equations

• √a = Classical.choose! ⋯

def LO.FirstOrder.Arithmetic.«term√_» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_spec_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : √a * √a ≤ a

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_spec_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a < (√a + 1) * (√a + 1)

theorem LO.FirstOrder.Arithmetic.sqrt_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} : b = √a ↔ b * b ≤ a ∧ a < (b + 1) * (b + 1)

def LO.FirstOrder.Arithmetic.sqrtDef : 𝚺₀.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.sqrt_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₁ sqrt via sqrtDef

instance LO.FirstOrder.Arithmetic.sqrt_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₁ sqrt

theorem LO.FirstOrder.Arithmetic.eq_sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (x a : V) : x * x ≤ a ∧ a < (x + 1) * (x + 1) → x = √a

theorem LO.FirstOrder.Arithmetic.sqrt_eq_of_le_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {x a : V} (le : x * x ≤ a) (lt : a < (x + 1) * (x + 1)) : √a = x

theorem LO.FirstOrder.Arithmetic.sqrt_eq_of_le_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {x a : V} (le : x * x ≤ a) (h : a ≤ x * x + 2 * x) : √a = x

@[simp]

theorem LO.FirstOrder.Arithmetic.sq_sqrt_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : (√a) ^ 2 ≤ a

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_lt_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a < (√a + 1) ^ 2

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_mul_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : √(a * a) = a

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : √a ^ 2 = a

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : √0 = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : √1 = 1

theorem LO.FirstOrder.Arithmetic.sqrt_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : √2 = 1

theorem LO.FirstOrder.Arithmetic.sqrt_three {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : √3 = 1

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_four {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : √4 = 2

@[simp]

theorem LO.FirstOrder.Arithmetic.two_ne_square {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : 2 ≠ a ^ 2

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_le_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : a ≤ √a * √a + 2 * √a

@[simp]

theorem LO.FirstOrder.Arithmetic.sqrt_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : √a ≤ a

instance LO.FirstOrder.Arithmetic.instBounded₁Sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : Bounded₁ fun (x : V) => √x

theorem LO.FirstOrder.Arithmetic.sqrt_lt_self_of_one_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} (h : 1 < a) : √a < a

theorem LO.FirstOrder.Arithmetic.sqrt_le_of_le_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} : a ≤ b ^ 2 → √a ≤ b

theorem LO.FirstOrder.Arithmetic.sq_lt_of_lt_sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} : a < √b → a ^ 2 < b

Pairing

noncomputable def LO.FirstOrder.Arithmetic.pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : V

Equations

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

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

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

Equations

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

def LO.FirstOrder.Arithmetic.pairUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

theorem LO.FirstOrder.Arithmetic.pair_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b c : V} : c = ⟪a, b⟫ ↔ a < b ∧ c = b * b + a ∨ b ≤ a ∧ c = a * a + a + b

def LO.FirstOrder.Arithmetic.pairDef : 𝚺₀.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.pair_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₂ pair via pairDef

instance LO.FirstOrder.Arithmetic.pair_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₂ pair

instance LO.FirstOrder.Arithmetic.instBounded₂Pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : Bounded₂ pair

noncomputable def LO.FirstOrder.Arithmetic.unpair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : V × V

Equations

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

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Arithmetic.pi₁ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : V

Equations

• π₁ a = (LO.FirstOrder.Arithmetic.unpair a).1

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Arithmetic.pi₂ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : V

Equations

• π₂ a = (LO.FirstOrder.Arithmetic.unpair a).2

def LO.FirstOrder.Arithmetic.termπ₁_ : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.termπ₂_ : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.pair_unpair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : ⟪π₁ a, π₂ a⟫ = a

@[simp]

theorem LO.FirstOrder.Arithmetic.unpair_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : unpair ⟪a, b⟫ = (a, b)

@[simp]

theorem LO.FirstOrder.Arithmetic.pi₁_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : π₁⟪a, b⟫ = a

@[simp]

theorem LO.FirstOrder.Arithmetic.pi₂_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : π₂⟪a, b⟫ = b

noncomputable def LO.FirstOrder.Arithmetic.pairEquiv {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : V × V ≃ V

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.pi₁_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : π₁ a ≤ a

@[simp]

theorem LO.FirstOrder.Arithmetic.pi₂_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) : π₂ a ≤ a

@[simp]

theorem LO.FirstOrder.Arithmetic.le_pair_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : a ≤ ⟪a, b⟫

@[simp]

theorem LO.FirstOrder.Arithmetic.le_pair_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : b ≤ ⟪a, b⟫

@[simp]

theorem LO.FirstOrder.Arithmetic.lt_pair_left_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} (pos : 0 < a) (b : V) : a < ⟪a, b⟫

instance LO.FirstOrder.Arithmetic.instBounded₁Pi₁ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : Bounded₁ pi₁

instance LO.FirstOrder.Arithmetic.instBounded₁Pi₂ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : Bounded₁ pi₂

def LO.FirstOrder.Arithmetic.pi₁Def : 𝚺₀.Semisentence 2

Equations

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

def LO.FirstOrder.Arithmetic.pi₂Def : 𝚺₀.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.pi₁_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₁ pi₁ via pi₁Def

instance LO.FirstOrder.Arithmetic.pi₁_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₁ pi₁

instance LO.FirstOrder.Arithmetic.pi₂_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₁ pi₂ via pi₂Def

instance LO.FirstOrder.Arithmetic.pi₂_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₁ pi₂

theorem LO.FirstOrder.Arithmetic.pair_lt_pair_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a₁ a₂ : V} (h : a₁ < a₂) (b : V) : ⟪a₁, b⟫ < ⟪a₂, b⟫

theorem LO.FirstOrder.Arithmetic.pair_le_pair_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a₁ a₂ : V} (h : a₁ ≤ a₂) (b : V) : ⟪a₁, b⟫ ≤ ⟪a₂, b⟫

theorem LO.FirstOrder.Arithmetic.pair_lt_pair_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b₁ b₂ : V} (h : b₁ < b₂) : ⟪a, b₁⟫ < ⟪a, b₂⟫

theorem LO.FirstOrder.Arithmetic.pair_le_pair_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) {b₁ b₂ : V} (h : b₁ ≤ b₂) : ⟪a, b₁⟫ ≤ ⟪a, b₂⟫

theorem LO.FirstOrder.Arithmetic.pair_le_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a₁ a₂ b₁ b₂ : V} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : ⟪a₁, b₁⟫ ≤ ⟪a₂, b₂⟫

theorem LO.FirstOrder.Arithmetic.pair_lt_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a₁ a₂ b₁ b₂ : V} (ha : a₁ < a₂) (hb : b₁ < b₂) : ⟪a₁, b₁⟫ < ⟪a₂, b₂⟫

@[simp]

theorem LO.FirstOrder.Arithmetic.pair_polybound {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a b : V) : ⟪a, b⟫ ≤ (a + b + 1) ^ 2

@[simp]

theorem LO.FirstOrder.Arithmetic.pair_ext_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a₁ a₂ b₁ b₂ : V} : ⟪a₁, b₁⟫ = ⟪a₂, b₂⟫ ↔ a₁ = a₂ ∧ b₁ = b₂

def LO.FirstOrder.Arithmetic.pair₃Def : 𝚺₀.Semisentence 4

Equations

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

def LO.FirstOrder.Arithmetic.pair₄Def : 𝚺₀.Semisentence 5

Equations

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

def LO.FirstOrder.Arithmetic.pair₅Def : 𝚺₀.Semisentence 6

Equations

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

def LO.FirstOrder.Arithmetic.pair₆Def : 𝚺₀.Semisentence 7

Equations

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

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

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

@[simp]

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

@[simp]

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

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

instance LO.FirstOrder.Arithmetic.pair₃_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₃ fun (x1 x2 x3 : V) => ⟪x1, ⟪x2, x3⟫⟫ via pair₃Def

instance LO.FirstOrder.Arithmetic.pair₄_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : 𝚺₀-Function₄ fun (x1 x2 x3 x4 : V) => ⟪x1, ⟪x2, ⟪x3, x4⟫⟫⟫ via pair₄Def

instance LO.FirstOrder.Arithmetic.pair₅_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : HierarchySymbol.DefinedFunction (fun (v : Fin 5 → V) => ⟪v 0, ⟪v 1, ⟪v 2, ⟪v 3, v 4⟫⟫⟫⟫) pair₅Def

instance LO.FirstOrder.Arithmetic.pair₆_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] : HierarchySymbol.DefinedFunction (fun (v : Fin 6 → V) => ⟪v 0, ⟪v 1, ⟪v 2, ⟪v 3, ⟪v 4, v 5⟫⟫⟫⟫⟫) pair₆Def

noncomputable def LO.FirstOrder.Arithmetic.npair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {n : ℕ} (v : Fin n → V) : V

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.npair_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (v : Fin 0 → V) : npair v = 0

theorem LO.FirstOrder.Arithmetic.npair_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {n : ℕ} (x : V) (v : Fin n → V) : npair (x :> v) = ⟪x, npair v⟫

noncomputable def LO.FirstOrder.Arithmetic.unNpair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {n : ℕ} : Fin n → V → V

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.unNpair_npair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {n : ℕ} (i : Fin n) (v : Fin n → V) : unNpair i (npair v) = v i

def LO.FirstOrder.Arithmetic.unNpairDef {n : ℕ} (i : Fin n) : 𝚺₀.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.unNpair_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {n : ℕ} (i : Fin n) : 𝚺₀-Function₁ unNpair i via unNpairDef i

@[simp]

instance LO.FirstOrder.Arithmetic.unNpair_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {n : ℕ} (i : Fin n) (Γ : HierarchySymbol) : Γ-Function₁ unNpair i

theorem LO.FirstOrder.Arithmetic.nat_cast_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (n m : ℕ) : ↑⟪n, m⟫ = ⟪↑n, ↑m⟫

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

theorem LO.FirstOrder.Arithmetic.coe_pair_eq_pair_coe {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (n m : ℕ) : ↑(Nat.pair n m) = ⟪↑n, ↑m⟫

Polynomial induction

theorem LO.FirstOrder.Arithmetic.polynomial_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (Γ : Polarity) (m : ℕ) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ 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.FirstOrder.Arithmetic.sigma0_polynomial_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {P : V → Prop} (hP : 𝚺₀-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.FirstOrder.Arithmetic.sigma1_polynomial_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {P : V → Prop} (hP : 𝚺₁-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.FirstOrder.Arithmetic.pi1_polynomial_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {P : V → Prop} (hP : 𝚷₁-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