Exp

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg0] (X Y u : V) : Prop

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg0] (X Y u : V) : Prop

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg0] (y X Y : V) : Prop

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg0] (x y X Y : V) : Prop

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg0] (x y : V) : Prop

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg0] (y X Y : V) : Seqₛ y X Y ↔ ∀ u ≤ y, u ≠ 2 → PPow2 u → ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧ ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨ (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧ ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y

def LO.Arith.Exponential.Seqₛ.def : FirstOrder.Arith.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.Exponential.Seqₛ.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg0] : FirstOrder.Arith.Sg0-Relation₃ Seqₛ via «def»

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

def LO.FirstOrder.Arith.exponentialDef : 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.Exponential.defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg0] : FirstOrder.Arith.Sg0-Relation Exponential via FirstOrder.Arith.exponentialDef

@[simp]

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

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.Exponential.seqX₀ = 4

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

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

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

@[implicit_reducible]

noncomputable instance LO.Arith.instExp {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : Exp V

Equations

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

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

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

def LO.FirstOrder.Arith.expDef : 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.exp_defined_deltaZero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₁ «exp» via FirstOrder.Arith.expDef

@[simp]

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

instance LO.Arith.exp_definable_deltaZero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₁ «exp»

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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