Documentation

Arithmetization.ISigmaZero.Exponential.PPow2

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

Equations

LO.Arith.SPPow2 m = (¬LO.Arith.LenBit 1 m ∧ LO.Arith.LenBit 2 m ∧ ∀ i ≤ m, LO.Arith.Pow2 i → 2 < i → (LO.Arith.LenBit i m ↔ (√i) ^ 2 = i ∧ LO.Arith.LenBit (√i) m))

def LO.FirstOrder.Arith.sppow2Def :

𝚺₀.Semisentence 1

Equations

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

theorem LO.Arith.sppow2_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

𝚺₀ -Predicate SPPow2 via FirstOrder.Arith.sppow2Def

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

Equations

LO.Arith.PPow2 i = (LO.Arith.Pow2 i ∧ ∃ m < 2 * i, LO.Arith.SPPow2 m ∧ LO.Arith.LenBit i m)

Instances For

LO.Arith.ppow2_definable

def LO.FirstOrder.Arith.ppow2Def :

𝚺₀.Semisentence 1

Equations

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

theorem LO.Arith.ppow2_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

𝚺₀ -Predicate PPow2 via FirstOrder.Arith.ppow2Def

instance LO.Arith.ppow2_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

𝚺₀ -Predicate PPow2

theorem LO.Arith.SPPow2.not_lenbit_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) :

theorem LO.Arith.SPPow2.lenbit_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) :

theorem LO.Arith.SPPow2.lenbit_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : i ≤ m) (pi : Pow2 i) (lt2 : 2 < i) :

LenBit i m ↔ (√i) ^ 2 = i ∧ LenBit (√i) m

theorem LO.Arith.SPPow2.one_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : LenBit i m) :

1 < i

theorem LO.Arith.SPPow2.two_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : LenBit i m) (ne2 : i ≠ 2) :

2 < i

theorem LO.Arith.SPPow2.sqrt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : LenBit i m) (pi : Pow2 i) (ne2 : i ≠ 2) :

LenBit (√i) m

theorem LO.Arith.SPPow2.sq_sqrt_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (hi : LenBit i m) (pi : Pow2 i) (ne2 : i ≠ 2) :

(√i) ^ 2 = i

theorem LO.Arith.SPPow2.of_sqrt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) {i : V} (pi : Pow2 i) (him : i ≤ m) (hsqi : (√i) ^ 2 = i) (hi : LenBit (√i) m) :

@[simp]

theorem LO.Arith.SPPow2.two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

@[simp]

theorem LO.Arith.SPPow2.not_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

@[simp]

theorem LO.Arith.SPPow2.not_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

theorem LO.Arith.SPPow2.sq_le_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) {i j : V} (pi : Pow2 i) (pj : Pow2 j) (hi : LenBit i m) (hj : LenBit j m) :

i < j → i ^ 2 ≤ j

theorem LO.Arith.SPPow2.last_uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {m : V} (hm : SPPow2 m) {i j : V} (pi : Pow2 i) (pj : Pow2 j) (hi : LenBit i m) (hj : LenBit j m) (hsqi : m < i ^ 2) (hsqj : m < j ^ 2) :

i = j

theorem LO.Arith.PPow2.pow2 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (h : PPow2 i) :

theorem LO.Arith.PPow2.pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (ppi : PPow2 i) :

0 < i

theorem LO.Arith.PPow2.one_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (ppi : PPow2 i) :

1 < i

theorem LO.Arith.PPow2.sq_sqrt_eq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (ppi : PPow2 i) (ne2 : i ≠ 2) :

(√i) ^ 2 = i

theorem LO.Arith.PPow2.sqrt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (ppi : PPow2 i) (ne2 : i ≠ 2) :

theorem LO.Arith.PPow2.exists_spp {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (h : PPow2 i) :

∃ m < 2 * i, SPPow2 m ∧ LenBit i m

theorem LO.Arith.PPow2.sq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (ppi : PPow2 i) :

PPow2 (i ^ 2)

@[simp]

theorem LO.Arith.PPow2.two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

@[simp]

theorem LO.Arith.PPow2.not_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

@[simp]

theorem LO.Arith.PPow2.not_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

theorem LO.Arith.PPow2.elim {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} :

PPow2 i ↔ i = 2 ∨ ∃ (b : V), i = b ^ 2 ∧ PPow2 b

theorem LO.Arith.PPow2.elim' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} :

PPow2 i ↔ i = 2 ∨ 2 < i ∧ ∃ (j : V), i = j ^ 2 ∧ PPow2 j

@[simp]

theorem LO.Arith.PPow2.four {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

theorem LO.Arith.PPow2.two_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (hi : PPow2 i) :

2 ≤ i

theorem LO.Arith.PPow2.not_three {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

theorem LO.Arith.PPow2.two_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (hi : PPow2 i) (ne : i ≠ 2) :

2 < i

theorem LO.Arith.PPow2.four_le {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (hi : PPow2 i) (ne : i ≠ 2) :

4 ≤ i

theorem LO.Arith.PPow2.four_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (hi : PPow2 i) (ne2 : i ≠ 2) (ne4 : i ≠ 4) :

4 < i

theorem LO.Arith.PPow2.sq_ne_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (hi : PPow2 i) :

i ^ 2 ≠ 2

theorem LO.Arith.PPow2.sqrt_ne_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (hi : PPow2 i) (ne2 : i ≠ 2) (ne4 : i ≠ 4) :

theorem LO.Arith.PPow2.sq_ne_four {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} (hi : PPow2 i) (ne2 : i ≠ 2) :

i ^ 2 ≠ 4

theorem LO.Arith.PPow2.sq_le_of_lt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i j : V} (hi : PPow2 i) (hj : PPow2 j) :

i < j → i ^ 2 ≤ j

theorem LO.Arith.PPow2.sq_uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y i j : V} (py : Pow2 y) (ppi : PPow2 i) (ppj : PPow2 j) (hi : y < i ∧ i ≤ y ^ 2) (hj : y < j ∧ j ≤ y ^ 2) :

i = j

theorem LO.Arith.PPow2.two_mul_sq_uniq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y i j : V} (py : Pow2 y) (ppi : PPow2 i) (ppj : PPow2 j) (hi : y < i ∧ i ≤ 2 * y ^ 2) (hj : y < j ∧ j ≤ 2 * y ^ 2) :

i = j