Documentation

Arithmetization.ISigmaZero.Exponential.PPow2

def LO.Arith.SPPow2 {V : Type u_1} [LO.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))

Instances For

def LO.FirstOrder.Arith.sppow2Def :

𝚺₀.Semisentence 1

Equations

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

Instances For

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

𝚺₀ -Predicate LO.Arith.SPPow2 via LO.FirstOrder.Arith.sppow2Def

def LO.Arith.PPow2 {V : Type u_1} [LO.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

def LO.FirstOrder.Arith.ppow2Def :

𝚺₀.Semisentence 1

Equations

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

Instances For

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

𝚺₀ -Predicate LO.Arith.PPow2 via LO.FirstOrder.Arith.ppow2Def

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

𝚺₀ -Predicate LO.Arith.PPow2

Equations

⋯ = ⋯

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

¬LO.Arith.LenBit 1 m

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

LO.Arith.LenBit 2 m

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

LO.Arith.LenBit i m ↔ (√i) ^ 2 = i ∧ LO.Arith.LenBit (√i) m

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

1 < i

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

2 < i

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

LO.Arith.LenBit (√i) m

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

(√i) ^ 2 = i

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

LO.Arith.LenBit i m

@[simp]

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

LO.Arith.SPPow2 2

@[simp]

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

¬LO.Arith.SPPow2 0

@[simp]

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

¬LO.Arith.SPPow2 1

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

i < j → i ^ 2 ≤ j

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

i = j

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

LO.Arith.Pow2 i

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

0 < i

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

1 < i

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

(√i) ^ 2 = i

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

LO.Arith.PPow2 (√i)

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

∃ m < 2 * i, LO.Arith.SPPow2 m ∧ LO.Arith.LenBit i m

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

LO.Arith.PPow2 (i ^ 2)

@[simp]

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

LO.Arith.PPow2 2

@[simp]

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

¬LO.Arith.PPow2 0

@[simp]

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

¬LO.Arith.PPow2 1

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

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

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

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

@[simp]

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

LO.Arith.PPow2 4

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

2 ≤ i

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

¬LO.Arith.PPow2 3

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

2 < i

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

4 ≤ i

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

4 < i

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

i ^ 2 ≠ 2

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

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

i ^ 2 ≠ 4

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

i < j → i ^ 2 ≤ j

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

i = j