Supporting results for pointwise provable equality.

Basic properties of theory $\mathsf{IOpen}$

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrPeanoMinus {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : V↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrInductionSchemeOpenNat {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : V↓[ℒₒᵣ] ⊧* InductionScheme ℒₒᵣ Semiformula.Open

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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)

@[instance_reducible]

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.instDivModel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Div V

The inst Div lean Pool construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.instDivModel = { div := fun (a b : V) => PointwiseComposition.Classical.chooseUnique ⋯ }

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.div_spec_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a / 0 = 0

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.divDef : Σ₀.Semisentence 3

The div Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.div_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₂ HDiv.hDiv via divDef

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_div {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : 0 / a = 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.div_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b c : V) : a / (b * c) = a / b / c

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_div_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : b * (a / b) ≤ a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.div_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : a / b ≤ a

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.div_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Bounded₂ fun (x1 x2 : V) => x1 / x2

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.div_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₂ fun (x1 x2 : V) => x1 / x2

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.div_mul_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : a / b * b ≤ a

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.div_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a / 1 = a

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.div_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a ^ 2 / a = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.div_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {a : V} (hx : 0 < a) : a / a = 1

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.div_mul' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) {b : V} (pos : 0 < b) : b * a / b = a

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_div_self_of_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {a b : V} : a * (b / a) = b ↔ a ∣ b

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.le_two_mul_div_two_add_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a ≤ 2 * (a / 2) + 1

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.div_monotone {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {a b : V} (h : a ≤ b) (c : V) : a / c ≤ b / c

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.rem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : V

The rem construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[instance_reducible]

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.instModModel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Mod V

The inst Mod lean Pool construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.instModModel = { mod := PointwiseComposition.FFL.FirstOrder.Arithmetic.rem }

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : a % b = a - b * (a / b)

def PointwiseComposition.FFL.FirstOrder.Arithmetic.remDef : Σ₀.Semisentence 3

The rem Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.rem_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₂ HMod.hMod via remDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.rem_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₂ HMod.hMod

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.div_add_mod {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : b * (a / b) + a % b = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a % 0 = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_mod {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : 0 % a = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a % a = 0

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_mul_self_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : a * b % b = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_mul_self_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : b * a % b = 0

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) {b : V} (pos : 0 < b) : a % b < b

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : a % b ≤ a

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Bounded₂ fun (x1 x2 : V) => x1 % x2

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_eq_zero_iff_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {a b : V} : b % a = 0 ↔ a ∣ b

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_div {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : a % b / b = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a % 1 = 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a % 2 = 0 ∨ a % 2 = 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_two_not_zero_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {a : V} : ¬a % 2 = 0 ↔ a % 2 = 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mod_two_not_one_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {a : V} : ¬a % 2 = 1 ↔ a % 2 = 0

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_dvd_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {a b : V} : 2 ∣ a * b → 2 ∣ a ∨ 2 ∣ b

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.even_or_odd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : ∃ (x : V), a = 2 * x ∨ a = 2 * x + 1

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.even_or_odd' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_prime {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Prime 2

Square root

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : V

The sqrt construction in FFL.FirstOrder.Arithmetic.

Equations

• √a = PointwiseComposition.Classical.chooseUnique ⋯

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

The «term√ » construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_spec_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : √a * √a ≤ a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_spec_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a < (√a + 1) * (√a + 1)

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrtDef : Σ₀.Semisentence 2

The sqrt Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₁ sqrt via sqrtDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₁ sqrt

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.sq_sqrt_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : (√a) ^ 2 ≤ a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_lt_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a < (√a + 1) ^ 2

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_mul_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : √(a * a) = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : √a ^ 2 = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : √0 = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : √1 = 1

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : √2 = 1

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_three {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : √3 = 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_four {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : √4 = 2

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_ne_square {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : 2 ≠ a ^ 2

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_le_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : a ≤ √a * √a + 2 * √a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : √a ≤ a

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instBounded₁Sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Bounded₁ fun (x : V) => √x

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_lt_self_of_one_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {a : V} (h : 1 < a) : √a < a

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sqrt_le_of_le_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {a b : V} : a ≤ b ^ 2 → √a ≤ b

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : V

The pair construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.pairUnexpander : Lean.PrettyPrinter.Unexpander

The pair Unexpander construction in FFL.FirstOrder.Arithmetic.

Equations

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.pairDef : Σ₀.Semisentence 3

The pair Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.pair_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₂ pair via pairDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.pair_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₂ pair

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instBounded₂Pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Bounded₂ pair

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.unpair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : V × V

The unpair construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[reducible, inline]

noncomputable abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₁ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : V

The pi₁ construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[reducible, inline]

noncomputable abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₂ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : V

The pi₂ construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.termπ₁_ : Lean.ParserDescr

The termπ₁ construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.termπ₂_ : Lean.ParserDescr

The termπ₂ construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pair_unpair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : ⟪π₁ a, π₂ a⟫ = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.unpair_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : unpair ⟪a, b⟫ = (a, b)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₁_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : π₁⟪a, b⟫ = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₂_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : π₂⟪a, b⟫ = b

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.pairEquiv {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : V × V ≃ V

The pair Equiv construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₁_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : π₁ a ≤ a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₂_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a : V) : π₂ a ≤ a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_pair_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : a ≤ ⟪a, b⟫

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_pair_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : b ≤ ⟪a, b⟫

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.instBounded₁Pi₁ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Bounded₁ pi₁

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instBounded₁Pi₂ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Bounded₁ pi₂

def PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₁Def : Σ₀.Semisentence 2

The pi₁Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₂Def : Σ₀.Semisentence 2

The pi₂Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₁_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₁ pi₁ via pi₁Def

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₁_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₁ pi₁

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₂_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₁ pi₂ via pi₂Def

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.pi₂_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₁ pi₂

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.pair_polybound {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : V) : ⟪a, b⟫ ≤ (a + b + 1) ^ 2

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.pair₃Def : Σ₀.Semisentence 4

The pair₃Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.pair₄Def : Σ₀.Semisentence 5

The pair₄Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.pair₅Def : Σ₀.Semisentence 6

The pair₅Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.pair₆Def : Σ₀.Semisentence 7

The pair₆Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

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

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

@[simp]

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

@[simp]

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

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.pair₃_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] : Σ₀-Function₃ fun (x1 x2 x3 : V) => ⟪x1, ⟪x2, x3⟫⟫ via pair₃Def

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.npair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {n : ℕ} (v : Fin n → V) : V

The npair construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.npair_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (v : Fin 0 → V) : npair v = 0

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.unNpair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {n : ℕ} : Fin n → V → V

The un Npair construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.unNpairDef {n : ℕ} (i : Fin n) : Σ₀.Semisentence 2

The un Npair Def construction in FFL.FirstOrder.Arithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.unNpair_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {n : ℕ} (i : Fin n) : Σ₀-Function₁ unNpair i via unNpairDef i

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.unNpair_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] {n : ℕ} (i : Fin n) (Γ : HierarchySymbol) : Γ-Function₁ unNpair i

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nat_cast_pair {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (n m : ℕ) : ↑⟪n, m⟫ = ⟪↑n, ↑m⟫

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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