Theorem: LO.FirstOrder.Arith.Model.Exponential.pow2_ext_of_seq₀_of_seqₛ (Arithmetization/ISigmaZero/Exponential/Exp.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ Pow2 (ext i Y)
Tactic:
induction i using order_induction_iSigmaZero
State after:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
⊢ 𝚺₀-Predicate fun {i} => i ≠ 2 → i ≤ y ^ 2 → PPow2 i → Pow2 (ext i Y)

case ind
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
x✝ : M
a✝ : ∀ y_1 < x✝, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : x✝ ≠ 2
hi : x✝ ≤ y ^ 2
ppi : PPow2 x✝
⊢ Pow2 (ext x✝ Y)

State before:
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
⊢ 𝚺₀-Predicate fun {i} => i ≠ 2 → i ≤ y ^ 2 → PPow2 i → Pow2 (ext i Y)
Tactic:
definability
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
⊢ Pow2 (ext i Y)
Tactic:
by_cases ei : i = 4
State after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : i = 4
⊢ Pow2 (ext i Y)

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ Pow2 (ext i Y)

State before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : i = 4
⊢ Pow2 (ext i Y)
Tactic:
rcases ei with rfl
State after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
IH : ∀ y_1 < 4, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ Pow2 (ext 4 Y)

State before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
IH : ∀ y_1 < 4, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : 4 ≠ 2
hi : 4 ≤ y ^ 2
ppi : PPow2 4
⊢ Pow2 (ext 4 Y)
Tactic:
simp [h₀.2]
State after:
no goals

State before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ Pow2 (ext i Y)
Tactic:
have ppsq : Pow2 (ext (√i) Y) :=
  IH (√i) (sqrt_lt_self_of_one_lt ppi.one_lt) (ppi.sqrt_ne_two ne2 ei) (le_trans (by simp) hi) (ppi.sqrt ne2)
State after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
⊢ Pow2 (ext i Y)

State before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
⊢ Pow2 (ext i Y)
Tactic:
rcases show Seqₛ.Even X Y (√i) ∨ Seqₛ.Odd X Y (√i) from
  hₛ (√i) (sqrt_le_of_le_sq $ hi) (ppi.sqrt_ne_two ne2 ei) (ppi.sqrt ne2) with (heven | hodd)
State after:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
heven : Seqₛ.Even X Y (√i)
⊢ Pow2 (ext i Y)

case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
hodd : Seqₛ.Odd X Y (√i)
⊢ Pow2 (ext i Y)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
⊢ √i ≤ i
Tactic:
simp
State after:
no goals

State before:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
heven : Seqₛ.Even X Y (√i)
⊢ Pow2 (ext i Y)
Tactic:
have : ext i Y = (ext (√i) Y)^2 := by simpa [ppi.sq_sqrt_eq ne2] using heven.2
State after:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ Pow2 (ext i Y)

State before:
case neg.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
heven : Seqₛ.Even X Y (√i)
this : ext i Y = ext (√i) Y ^ 2
⊢ Pow2 (ext i Y)
Tactic:
simp [this, ppsq]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
heven : Seqₛ.Even X Y (√i)
⊢ ext i Y = ext (√i) Y ^ 2
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using heven.2
State after:
no goals

State before:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
hodd : Seqₛ.Odd X Y (√i)
⊢ Pow2 (ext i Y)
Tactic:
have : ext i Y = 2*(ext (√i) Y)^2 := by simpa [ppi.sq_sqrt_eq ne2] using hodd.2
State after:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ Pow2 (ext i Y)

State before:
case neg.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
hodd : Seqₛ.Odd X Y (√i)
this : ext i Y = 2 * ext (√i) Y ^ 2
⊢ Pow2 (ext i Y)
Tactic:
simp [this, ppsq]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
h₀ : Seq₀ X Y
hₛ : Seqₛ y X Y
i : M
IH : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → Pow2 (ext y_1 Y)
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ei : ¬i = 4
ppsq : Pow2 (ext (√i) Y)
hodd : Seqₛ.Odd X Y (√i)
⊢ ext i Y = 2 * ext (√i) Y ^ 2
Tactic:
simpa [ppi.sq_sqrt_eq ne2] using hodd.2
State after:
no goals