def LO.Arith.ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (u : V) (z : V) : V

Equations

• LO.Arith.ext u z = z / u % u

theorem LO.Arith.ext_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (b : V) (c : V) : a = LO.Arith.ext b c ↔ ∃ x ≤ c, x = c / b ∧ a = x % b

def LO.FirstOrder.Arith.extDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.ext_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₂ fun (a b : V) => LO.Arith.ext a b via LO.FirstOrder.Arith.extDef

instance LO.Arith.ext_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₂ LO.Arith.ext

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.ext_le_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (u : V) (z : V) : LO.Arith.ext u z ≤ z

instance LO.Arith.instBounded₂Ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.FirstOrder.Arith.Bounded₂ LO.Arith.ext

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.ext_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {u : V} (z : V) (pos : 0 < u) : LO.Arith.ext u z < u

theorem LO.Arith.ext_add_of_dvd_sq_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {u : V} {z₁ : V} {z₂ : V} (pos : 0 < u) (h : u ^ 2 ∣ z₂) : LO.Arith.ext u (z₁ + z₂) = LO.Arith.ext u z₁

theorem LO.Arith.ext_add_of_dvd_sq_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {u : V} {z₁ : V} {z₂ : V} (pos : 0 < u) (h : u ^ 2 ∣ z₁) : LO.Arith.ext u (z₁ + z₂) = LO.Arith.ext u z₂

theorem LO.Arith.ext_rem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {j : V} {z : V} (ppi : LO.Arith.PPow2 i) (ppj : LO.Arith.PPow2 j) (hij : i < j) : LO.Arith.ext i (z % j) = LO.Arith.ext i z

def LO.Arith.Exponential.Seq₀ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (X : V) (Y : V) : Prop

Equations

• LO.Arith.Exponential.Seq₀ X Y = (LO.Arith.ext 4 X = 1 ∧ LO.Arith.ext 4 Y = 2)

def LO.Arith.Exponential.Seqₛ.Even {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (X : V) (Y : V) (u : V) : Prop

Equations

• LO.Arith.Exponential.Seqₛ.Even X Y u = (LO.Arith.ext (u ^ 2) X = 2 * LO.Arith.ext u X ∧ LO.Arith.ext (u ^ 2) Y = LO.Arith.ext u Y ^ 2)

def LO.Arith.Exponential.Seqₛ.Odd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (X : V) (Y : V) (u : V) : Prop

Equations

• LO.Arith.Exponential.Seqₛ.Odd X Y u = (LO.Arith.ext (u ^ 2) X = 2 * LO.Arith.ext u X + 1 ∧ LO.Arith.ext (u ^ 2) Y = 2 * LO.Arith.ext u Y ^ 2)

def LO.Arith.Exponential.Seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (y : V) (X : V) (Y : V) : Prop

Equations

• LO.Arith.Exponential.Seqₛ y X Y = ∀ u ≤ y, u ≠ 2 → LO.Arith.PPow2 u → LO.Arith.Exponential.Seqₛ.Even X Y u ∨ LO.Arith.Exponential.Seqₛ.Odd X Y u

def LO.Arith.Exponential.Seqₘ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (x : V) (y : V) (X : V) (Y : V) : Prop

Equations

• LO.Arith.Exponential.Seqₘ x y X Y = ∃ u ≤ y ^ 2, u ≠ 2 ∧ LO.Arith.PPow2 u ∧ LO.Arith.ext u X = x ∧ LO.Arith.ext u Y = y

def LO.Arith.Exponential {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (x : V) (y : V) : Prop

Equations

• LO.Arith.Exponential x y = (x = 0 ∧ y = 1 ∨ ∃ X ≤ y ^ 4, ∃ Y ≤ y ^ 4, LO.Arith.Exponential.Seq₀ X Y ∧ LO.Arith.Exponential.Seqₛ y X Y ∧ LO.Arith.Exponential.Seqₘ x y X Y)

theorem LO.Arith.Exponential.Seqₛ.iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (y : V) (X : V) (Y : V) : LO.Arith.Exponential.Seqₛ y X Y ↔ ∀ u ≤ y, u ≠ 2 → LO.Arith.PPow2 u → ((∃ ext_u_X ≤ X, ext_u_X = LO.Arith.ext u X ∧ 2 * ext_u_X = LO.Arith.ext (u ^ 2) X) ∧ ∃ ext_u_Y ≤ Y, ext_u_Y = LO.Arith.ext u Y ∧ ext_u_Y ^ 2 = LO.Arith.ext (u ^ 2) Y) ∨ (∃ ext_u_X ≤ X, ext_u_X = LO.Arith.ext u X ∧ 2 * ext_u_X + 1 = LO.Arith.ext (u ^ 2) X) ∧ ∃ ext_u_Y ≤ Y, ext_u_Y = LO.Arith.ext u Y ∧ 2 * ext_u_Y ^ 2 = LO.Arith.ext (u ^ 2) Y

def LO.Arith.Exponential.Seqₛ.def : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.Exponential.Seqₛ.defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Relation₃ LO.Arith.Exponential.Seqₛ via LO.Arith.Exponential.Seqₛ.def

theorem LO.Arith.Exponential.graph_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (x : V) (y : V) : LO.Arith.Exponential x y ↔ x = 0 ∧ y = 1 ∨ ∃ X ≤ y ^ 4, ∃ Y ≤ y ^ 4, (1 = LO.Arith.ext 4 X ∧ 2 = LO.Arith.ext 4 Y) ∧ LO.Arith.Exponential.Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ LO.Arith.PPow2 u ∧ x = LO.Arith.ext u X ∧ y = LO.Arith.ext u Y

def LO.FirstOrder.Arith.exponentialDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.Exponential.defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Relation LO.Arith.Exponential via LO.FirstOrder.Arith.exponentialDef

@[simp]

theorem LO.Arith.exponential_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.exponentialDef) ↔ LO.Arith.Exponential (v 0) (v 1)

instance LO.Arith.exponential_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Relation LO.Arith.Exponential

Equations

• ⋯ = ⋯

@[simp]

instance LO.Arith.exponential_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (Γ : LO.FirstOrder.Arith.HierarchySymbol) : Γ-Relation LO.Arith.Exponential

Equations

• ⋯ = ⋯

def LO.Arith.Exponential.seqX₀ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : V

Equations

• LO.Arith.Exponential.seqX₀ = 4

def LO.Arith.Exponential.seqY₀ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : V

Equations

• LO.Arith.Exponential.seqY₀ = 2 * 4

theorem LO.Arith.Exponential.one_lt_four {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 1 < 4

theorem LO.Arith.Exponential.two_lt_three {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 2 < 3

theorem LO.Arith.Exponential.three_lt_four {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 3 < 4

theorem LO.Arith.Exponential.two_lt_four {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 2 < 4

theorem LO.Arith.Exponential.seq₀_zero_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.Arith.Exponential.Seq₀ LO.Arith.Exponential.seqX₀ LO.Arith.Exponential.seqY₀

theorem LO.Arith.Exponential.Seq₀.rem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {X : V} {Y : V} {i : V} (h : LO.Arith.Exponential.Seq₀ X Y) (ppi : LO.Arith.PPow2 i) (hi : 4 < i) : LO.Arith.Exponential.Seq₀ (X % i) (Y % i)

theorem LO.Arith.Exponential.Seqₛ.rem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {y' : V} {X : V} {Y : V} {i : V} (h : LO.Arith.Exponential.Seqₛ y X Y) (ppi : LO.Arith.PPow2 i) (hi : y' ^ 2 < i) (hy : y' ≤ y) : LO.Arith.Exponential.Seqₛ y' (X % i) (Y % i)

theorem LO.Arith.Exponential.seqₛ_one_zero_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.Arith.Exponential.Seqₛ 1 LO.Arith.Exponential.seqX₀ LO.Arith.Exponential.seqY₀

def LO.Arith.Exponential.append {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (i : V) (X : V) (z : V) : V

Equations

• LO.Arith.Exponential.append i X z = X % i + z * i

theorem LO.Arith.Exponential.append_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (i : V) (X : V) {z : V} (hz : z < i) : LO.Arith.Exponential.append i X z < i ^ 2

theorem LO.Arith.Exponential.ext_append_last {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (i : V) (X : V) {z : V} (hz : z < i) : LO.Arith.ext i (LO.Arith.Exponential.append i X z) = z

theorem LO.Arith.Exponential.ext_append_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {j : V} (hi : LO.Arith.PPow2 i) (hj : LO.Arith.PPow2 j) (hij : i < j) (X : V) (z : V) : LO.Arith.ext i (LO.Arith.Exponential.append j X z) = LO.Arith.ext i X

theorem LO.Arith.Exponential.Seq₀.append {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {X : V} {Y : V} {i : V} {x : V} {y : V} (H : LO.Arith.Exponential.Seq₀ X Y) (ppi : LO.Arith.PPow2 i) (hi : 4 < i) : LO.Arith.Exponential.Seq₀ (LO.Arith.Exponential.append i X x) (LO.Arith.Exponential.append i Y y)

theorem LO.Arith.Exponential.Seqₛ.append {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {z : V} {x : V} {y : V} {X : V} {Y : V} {i : V} (h : LO.Arith.Exponential.Seqₛ z X Y) (ppi : LO.Arith.PPow2 i) (hz : z < i) : LO.Arith.Exponential.Seqₛ z (LO.Arith.Exponential.append (i ^ 2) X x) (LO.Arith.Exponential.append (i ^ 2) Y y)

@[simp]

theorem LO.Arith.Exponential.exponential_zero_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.Arith.Exponential 0 1

@[simp]

theorem LO.Arith.Exponential.exponential_one_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.Arith.Exponential 1 2

theorem LO.Arith.Exponential.pow2_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i ≠ 2) (hi : i ≤ y ^ 2) (ppi : LO.Arith.PPow2 i) : LO.Arith.Pow2 (LO.Arith.ext i Y)

theorem LO.Arith.Exponential.range_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (h : LO.Arith.Exponential x y) : LO.Arith.Pow2 y

theorem LO.Arith.Exponential.le_sq_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i ≠ 2) (hi : i ≤ y ^ 2) (ppi : LO.Arith.PPow2 i) : i ≤ LO.Arith.ext i Y ^ 2

theorem LO.Arith.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i ≠ 2) (hi : i ≤ y ^ 2) (ppi : LO.Arith.PPow2 i) : 2 * LO.Arith.ext i Y ≤ i

theorem LO.Arith.Exponential.exponential_exists_sq_of_exponential_even {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential (2 * x) y → ∃ (y' : V), y = y' ^ 2 ∧ LO.Arith.Exponential x y'

theorem LO.Arith.Exponential.bit_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential x y → LO.Arith.Exponential (2 * x) (y ^ 2)

theorem LO.Arith.Exponential.exponential_even {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential (2 * x) y ↔ ∃ (y' : V), y = y' ^ 2 ∧ LO.Arith.Exponential x y'

theorem LO.Arith.Exponential.exponential_even_sq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential (2 * x) (y ^ 2) ↔ LO.Arith.Exponential x y

theorem LO.Arith.Exponential.exponential_exists_sq_of_exponential_odd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential (2 * x + 1) y → ∃ (y' : V), y = 2 * y' ^ 2 ∧ LO.Arith.Exponential x y'

theorem LO.Arith.Exponential.bit_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential x y → LO.Arith.Exponential (2 * x + 1) (2 * y ^ 2)

theorem LO.Arith.Exponential.exponential_odd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential (2 * x + 1) y ↔ ∃ (y' : V), y = 2 * y' ^ 2 ∧ LO.Arith.Exponential x y'

theorem LO.Arith.Exponential.exponential_odd_two_mul_sq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential (2 * x + 1) (2 * y ^ 2) ↔ LO.Arith.Exponential x y

theorem LO.Arith.Exponential.two_le_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i ≠ 2) (hi : i ≤ y ^ 2) (ppi : LO.Arith.PPow2 i) : 2 ≤ LO.Arith.ext i Y

theorem LO.Arith.Exponential.ext_le_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i ≠ 2) (hi : i ≤ y ^ 2) (ppi : LO.Arith.PPow2 i) : LO.Arith.ext i X < LO.Arith.ext i Y

theorem LO.Arith.Exponential.range_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (h : LO.Arith.Exponential x y) : 0 < y

theorem LO.Arith.Exponential.lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (h : LO.Arith.Exponential x y) : x < y

theorem LO.Arith.Exponential.not_exponential_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (h : x ≤ y) : ¬LO.Arith.Exponential y x

@[simp]

theorem LO.Arith.Exponential.one_not_even {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) : 1 ≠ 2 * a

@[simp]

theorem LO.Arith.Exponential.exponential_two_four {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.Arith.Exponential 2 4

theorem LO.Arith.Exponential.exponential_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential (x + 1) y ↔ ∃ (z : V), y = 2 * z ∧ LO.Arith.Exponential x z

theorem LO.Arith.Exponential.exponential_succ_mul_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential (x + 1) (2 * y) ↔ LO.Arith.Exponential x y

theorem LO.Arith.Exponential.succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential x y → LO.Arith.Exponential (x + 1) (2 * y)

Alias of the reverse direction of LO.Arith.Exponential.exponential_succ_mul_two.

theorem LO.Arith.Exponential.of_succ_two_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential (x + 1) (2 * y) → LO.Arith.Exponential x y

Alias of the forward direction of LO.Arith.Exponential.exponential_succ_mul_two.

theorem LO.Arith.Exponential.one_le_ext_of_seq₀_of_seqₛ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {X : V} {Y : V} (h₀ : LO.Arith.Exponential.Seq₀ X Y) (hₛ : LO.Arith.Exponential.Seqₛ y X Y) {i : V} (ne2 : i ≠ 2) (hi : i ≤ y ^ 2) (ppi : LO.Arith.PPow2 i) : 1 ≤ LO.Arith.ext i X

theorem LO.Arith.Exponential.zero_uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} (h : LO.Arith.Exponential 0 y) : y = 1

@[simp]

theorem LO.Arith.Exponential.zero_uniq_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} : LO.Arith.Exponential 0 y ↔ y = 1

theorem LO.Arith.Exponential.succ_lt_s {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (h : LO.Arith.Exponential (x + 1) y) : 2 ≤ y

theorem LO.Arith.Exponential.uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y₁ : V} {y₂ : V} : LO.Arith.Exponential x y₁ → LO.Arith.Exponential x y₂ → y₁ = y₂

theorem LO.Arith.Exponential.inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y : V} : LO.Arith.Exponential x₁ y → LO.Arith.Exponential x₂ y → x₁ = x₂

theorem LO.Arith.Exponential.exponential_elim {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : LO.Arith.Exponential x y ↔ x = 0 ∧ y = 1 ∨ ∃ (x' : V) (y' : V), x = x' + 1 ∧ y = 2 * y' ∧ LO.Arith.Exponential x' y'

theorem LO.Arith.Exponential.monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} : LO.Arith.Exponential x₁ y₁ → LO.Arith.Exponential x₂ y₂ → x₁ < x₂ → y₁ < y₂

theorem LO.Arith.Exponential.monotone_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} (h₁ : LO.Arith.Exponential x₁ y₁) (h₂ : LO.Arith.Exponential x₂ y₂) : x₁ ≤ x₂ → y₁ ≤ y₂

theorem LO.Arith.Exponential.monotone_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} (h₁ : LO.Arith.Exponential x₁ y₁) (h₂ : LO.Arith.Exponential x₂ y₂) : x₁ < x₂ ↔ y₁ < y₂

theorem LO.Arith.Exponential.monotone_le_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} (h₁ : LO.Arith.Exponential x₁ y₁) (h₂ : LO.Arith.Exponential x₂ y₂) : x₁ ≤ x₂ ↔ y₁ ≤ y₂

theorem LO.Arith.Exponential.add_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {y₁ : V} {y₂ : V} (h₁ : LO.Arith.Exponential x₁ y₁) (h₂ : LO.Arith.Exponential x₂ y₂) : LO.Arith.Exponential (x₁ + x₂) (y₁ * y₂)

theorem LO.Arith.Exponential.range_exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : ∃ (y : V), LO.Arith.Exponential x y

theorem LO.Arith.Exponential.range_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : ∃! y : V, LO.Arith.Exponential x y

instance LO.Arith.instExp_arithmetization {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : Exp V

Equations

• LO.Arith.instExp_arithmetization = { exp := fun (a : V) => Classical.choose! ⋯ }

theorem LO.Arith.exponential_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : LO.Arith.Exponential a (exp a)

theorem LO.Arith.exponential_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} : a = exp b ↔ LO.Arith.Exponential b a

def LO.FirstOrder.Arith.expDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.exp_defined_deltaZero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ exp via LO.FirstOrder.Arith.expDef

@[simp]

theorem LO.Arith.exp_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.expDef) ↔ v 0 = exp v 1

instance LO.Arith.exp_definable_deltaZero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ exp

Equations

• ⋯ = ⋯

theorem LO.Arith.exp_of_exponential {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : LO.Arith.Exponential a b) : exp a = b

theorem LO.Arith.exp_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : Function.Injective exp

@[simp]

theorem LO.Arith.exp_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : exp 0 = 1

@[simp]

theorem LO.Arith.exp_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : exp 1 = 2

theorem LO.Arith.exp_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : exp (a + 1) = 2 * exp a

theorem LO.Arith.exp_even {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : exp (2 * a) = exp a ^ 2

@[simp]

theorem LO.Arith.lt_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : a < exp a

@[simp]

theorem LO.Arith.exp_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : 0 < exp a

@[simp]

theorem LO.Arith.one_le_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : 1 ≤ exp a

@[simp]

theorem LO.Arith.exp_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : LO.Arith.Pow2 (exp a)

@[simp]

theorem LO.Arith.exp_monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} : exp a < exp b ↔ a < b

@[simp]

theorem LO.Arith.exp_monotone_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} : exp a ≤ exp b ↔ a ≤ b

theorem LO.Arith.nat_cast_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : ℕ) : ↑(exp n) = exp ↑n