Exponential function

This file provides a proof of the theorem states that the graph of exponential function is definable by $\Sigma_0$-formula and it's inductive property is provable in $\mathsf{I}\Sigma_0$.

noncomputable def LO.FirstOrder.Arithmetic.ext {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (u z : V) : V

Equations

• LO.FirstOrder.Arithmetic.ext u z = z / u % u

theorem LO.FirstOrder.Arithmetic.ext_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a b c : V) : a = ext b c ↔ ∃ x ≤ c, x = c / b ∧ a = x % b

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

Equations

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

instance LO.FirstOrder.Arithmetic.ext_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : 𝚺₀-Function₂ ext via extDef

instance LO.FirstOrder.Arithmetic.ext_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : 𝚺₀-Function₂ ext

@[simp]

theorem LO.FirstOrder.Arithmetic.ext_le_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (u z : V) : ext u z ≤ z

instance LO.FirstOrder.Arithmetic.instBounded₂Ext {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : Bounded₂ ext

@[simp]

theorem LO.FirstOrder.Arithmetic.ext_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {u : V} (z : V) (pos : 0 < u) : ext u z < u

theorem LO.FirstOrder.Arithmetic.ext_add_of_dvd_sq_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {u z₁ z₂ : V} (pos : 0 < u) (h : u ^ 2 ∣ z₂) : ext u (z₁ + z₂) = ext u z₁

theorem LO.FirstOrder.Arithmetic.ext_add_of_dvd_sq_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {u z₁ z₂ : V} (pos : 0 < u) (h : u ^ 2 ∣ z₁) : ext u (z₁ + z₂) = ext u z₂

theorem LO.FirstOrder.Arithmetic.ext_rem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i j z : V} (ppi : PPow2 i) (ppj : PPow2 j) (hij : i < j) : ext i (z % j) = ext i z

def LO.FirstOrder.Arithmetic.Exponential.Seq₀ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (X Y : V) : Prop

Equations

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

def LO.FirstOrder.Arithmetic.Exponential.Seqₛ.Even {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (X Y u : V) : Prop

Equations

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

def LO.FirstOrder.Arithmetic.Exponential.Seqₛ.Odd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (X Y u : V) : Prop

Equations

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

def LO.FirstOrder.Arithmetic.Exponential.Seqₛ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (y X Y : V) : Prop

Equations

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

def LO.FirstOrder.Arithmetic.Exponential.Seqₘ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (x y X Y : V) : Prop

Equations

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

def LO.FirstOrder.Arithmetic.Exponential {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (x y : V) : Prop

The graph of the exponential function

Equations

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

theorem LO.FirstOrder.Arithmetic.Exponential.Seqₛ.iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (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.FirstOrder.Arithmetic.Exponential.Seqₛ.def : 𝚺₀.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Exponential.Seqₛ.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : 𝚺₀-Relation₃ Seqₛ via «def»

theorem LO.FirstOrder.Arithmetic.Exponential.graph_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (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.Arithmetic.exponentialDef : 𝚺₀.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.Exponential.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : 𝚺₀-Relation Exponential via exponentialDef

The graph of the exponential function can be defined by the $\Delta_0$-formula.

instance LO.FirstOrder.Arithmetic.exponential_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : 𝚺₀-Relation Exponential

The graph of the exponential function can be defined by the $\Delta_0$-formula.

@[simp]

instance LO.FirstOrder.Arithmetic.exponential_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (Γ : HierarchySymbol) : Γ-Relation Exponential

def LO.FirstOrder.Arithmetic.Exponential.seqX₀ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : V

Equations

• LO.FirstOrder.Arithmetic.Exponential.seqX₀ = 4

def LO.FirstOrder.Arithmetic.Exponential.seqY₀ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : V

Equations

• LO.FirstOrder.Arithmetic.Exponential.seqY₀ = 2 * 4

theorem LO.FirstOrder.Arithmetic.Exponential.one_lt_four {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : 1 < 4

theorem LO.FirstOrder.Arithmetic.Exponential.two_lt_three {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : 2 < 3

theorem LO.FirstOrder.Arithmetic.Exponential.three_lt_four {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : 3 < 4

theorem LO.FirstOrder.Arithmetic.Exponential.two_lt_four {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : 2 < 4

theorem LO.FirstOrder.Arithmetic.Exponential.seq₀_zero_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : Seq₀ seqX₀ seqY₀

theorem LO.FirstOrder.Arithmetic.Exponential.Seq₀.rem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {X Y i : V} (h : Seq₀ X Y) (ppi : PPow2 i) (hi : 4 < i) : Seq₀ (X % i) (Y % i)

theorem LO.FirstOrder.Arithmetic.Exponential.Seqₛ.rem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.seqₛ_one_zero_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : Seqₛ 1 seqX₀ seqY₀

noncomputable def LO.FirstOrder.Arithmetic.Exponential.append {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (i X z : V) : V

Equations

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

theorem LO.FirstOrder.Arithmetic.Exponential.append_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (i X : V) {z : V} (hz : z < i) : append i X z < i ^ 2

theorem LO.FirstOrder.Arithmetic.Exponential.ext_append_last {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (i X : V) {z : V} (hz : z < i) : ext i (append i X z) = z

theorem LO.FirstOrder.Arithmetic.Exponential.ext_append_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.Seq₀.append {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.Seqₛ.append {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.exponential_zero_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : Exponential 0 1

@[simp]

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_one_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : Exponential 1 2

theorem LO.FirstOrder.Arithmetic.Exponential.pow2_ext_of_seq₀_of_seqₛ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.range_pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (h : Exponential x y) : Pow2 y

theorem LO.FirstOrder.Arithmetic.Exponential.le_sq_ext_of_seq₀_of_seqₛ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.exponential_exists_sq_of_exponential_even {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential (2 * x) y → ∃ (y' : V), y = y' ^ 2 ∧ Exponential x y'

theorem LO.FirstOrder.Arithmetic.Exponential.bit_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential x y → Exponential (2 * x) (y ^ 2)

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_even {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential (2 * x) y ↔ ∃ (y' : V), y = y' ^ 2 ∧ Exponential x y'

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_even_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential (2 * x) (y ^ 2) ↔ Exponential x y

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_exists_sq_of_exponential_odd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential (2 * x + 1) y → ∃ (y' : V), y = 2 * y' ^ 2 ∧ Exponential x y'

theorem LO.FirstOrder.Arithmetic.Exponential.bit_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential x y → Exponential (2 * x + 1) (2 * y ^ 2)

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_odd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential (2 * x + 1) y ↔ ∃ (y' : V), y = 2 * y' ^ 2 ∧ Exponential x y'

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_odd_two_mul_sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential (2 * x + 1) (2 * y ^ 2) ↔ Exponential x y

theorem LO.FirstOrder.Arithmetic.Exponential.two_le_ext_of_seq₀_of_seqₛ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.ext_le_ext_of_seq₀_of_seqₛ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.range_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (h : Exponential x y) : 0 < y

theorem LO.FirstOrder.Arithmetic.Exponential.lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (h : Exponential x y) : x < y

theorem LO.FirstOrder.Arithmetic.Exponential.not_exponential_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (h : x ≤ y) : ¬Exponential y x

@[simp]

theorem LO.FirstOrder.Arithmetic.Exponential.one_not_even {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) : 1 ≠ 2 * a

@[simp]

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_two_four {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] : Exponential 2 4

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential (x + 1) y ↔ ∃ (z : V), y = 2 * z ∧ Exponential x z

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_succ_mul_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential (x + 1) (2 * y) ↔ Exponential x y

theorem LO.FirstOrder.Arithmetic.Exponential.of_succ_two_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential (x + 1) (2 * y) → Exponential x y

Alias of the forward direction of LO.FirstOrder.Arithmetic.Exponential.exponential_succ_mul_two.

theorem LO.FirstOrder.Arithmetic.Exponential.succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} : Exponential x y → Exponential (x + 1) (2 * y)

Alias of the reverse direction of LO.FirstOrder.Arithmetic.Exponential.exponential_succ_mul_two.

theorem LO.FirstOrder.Arithmetic.Exponential.one_le_ext_of_seq₀_of_seqₛ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.zero_uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y : V} (h : Exponential 0 y) : y = 1

@[simp]

theorem LO.FirstOrder.Arithmetic.Exponential.zero_uniq_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y : V} : Exponential 0 y ↔ y = 1

theorem LO.FirstOrder.Arithmetic.Exponential.succ_lt_s {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (h : Exponential (x + 1) y) : 2 ≤ y

theorem LO.FirstOrder.Arithmetic.Exponential.uniq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y₁ y₂ : V} : Exponential x y₁ → Exponential x y₂ → y₁ = y₂

theorem LO.FirstOrder.Arithmetic.Exponential.inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x₁ x₂ y : V} : Exponential x₁ y → Exponential x₂ y → x₁ = x₂

theorem LO.FirstOrder.Arithmetic.Exponential.exponential_elim {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {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.FirstOrder.Arithmetic.Exponential.monotone {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x₁ x₂ y₁ y₂ : V} : Exponential x₁ y₁ → Exponential x₂ y₂ → x₁ < x₂ → y₁ < y₂

theorem LO.FirstOrder.Arithmetic.Exponential.monotone_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x₁ x₂ y₁ y₂ : V} (h₁ : Exponential x₁ y₁) (h₂ : Exponential x₂ y₂) : x₁ ≤ x₂ → y₁ ≤ y₂

theorem LO.FirstOrder.Arithmetic.Exponential.monotone_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x₁ x₂ y₁ y₂ : V} (h₁ : Exponential x₁ y₁) (h₂ : Exponential x₂ y₂) : x₁ < x₂ ↔ y₁ < y₂

theorem LO.FirstOrder.Arithmetic.Exponential.monotone_le_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x₁ x₂ y₁ y₂ : V} (h₁ : Exponential x₁ y₁) (h₂ : Exponential x₂ y₂) : x₁ ≤ x₂ ↔ y₁ ≤ y₂

theorem LO.FirstOrder.Arithmetic.Exponential.add_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x₁ x₂ y₁ y₂ : V} (h₁ : Exponential x₁ y₁) (h₂ : Exponential x₂ y₂) : Exponential (x₁ + x₂) (y₁ * y₂)

theorem LO.FirstOrder.Arithmetic.Exponential.range_exists {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x : V) : ∃ (y : V), Exponential x y

The exponential function is proved to be total in $\mathsf I Σ_1$.

theorem LO.FirstOrder.Arithmetic.Exponential.range_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x : V) : ∃! y : V, Exponential x y

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.instExp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Exp V

Equations

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

theorem LO.FirstOrder.Arithmetic.exponential_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : Exponential a (Exp.exp a)

theorem LO.FirstOrder.Arithmetic.exponential_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} : a = Exp.exp b ↔ Exponential b a

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

Equations

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

instance LO.FirstOrder.Arithmetic.exp_defined_deltaZero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ Exp.exp via expDef

instance LO.FirstOrder.Arithmetic.exp_definable_deltaZero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ Exp.exp

theorem LO.FirstOrder.Arithmetic.exp_of_exponential {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} (h : Exponential a b) : Exp.exp a = b

theorem LO.FirstOrder.Arithmetic.exp_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Function.Injective Exp.exp

@[simp]

theorem LO.FirstOrder.Arithmetic.exp_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Exp.exp 0 = 1

@[simp]

theorem LO.FirstOrder.Arithmetic.exp_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : Exp.exp 1 = 2

theorem LO.FirstOrder.Arithmetic.exp_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : Exp.exp (a + 1) = 2 * Exp.exp a

theorem LO.FirstOrder.Arithmetic.exp_even {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : Exp.exp (2 * a) = Exp.exp a ^ 2

@[simp]

theorem LO.FirstOrder.Arithmetic.lt_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : a < Exp.exp a

@[simp]

theorem LO.FirstOrder.Arithmetic.exp_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : 0 < Exp.exp a

@[simp]

theorem LO.FirstOrder.Arithmetic.one_le_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : 1 ≤ Exp.exp a

@[simp]

theorem LO.FirstOrder.Arithmetic.exp_pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) : Pow2 (Exp.exp a)

@[simp]

theorem LO.FirstOrder.Arithmetic.exp_monotone {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} : Exp.exp a < Exp.exp b ↔ a < b

@[simp]

theorem LO.FirstOrder.Arithmetic.exp_monotone_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} : Exp.exp a ≤ Exp.exp b ↔ a ≤ b

theorem LO.FirstOrder.Arithmetic.nat_cast_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (n : ℕ) : ↑(Exp.exp n) = Exp.exp ↑n