p' : ℕ
h : sZMod (p' + 2) (p' + 2 - 2) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
dsimp [lucasLehmerResidue] at h
p' : ℕ
h : ↑(s (p' + 2 - 2)) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
p' : ℕ
h : sZMod (p' + 2) (p' + 2 - 2) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
rw [sZMod_eq_s p'] at h
p' : ℕ
h : 2 ^ (p' + 2) - 1 ∣ s p'
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
p' : ℕ
h : ↑(s (p' + 2 - 2)) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
simp [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h
case intro
p' : ℕ
k : ℤ
h : s p' = (2 ^ (p' + 2) - 1) * k
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
p' : ℕ
h : 2 ^ (p' + 2) - 1 ∣ s p'
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
cases' h with k h
case intro
p' : ℕ
k : ℤ
h : s p' = (2 ^ (p' + 2) - 1) * k
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : s p' = (2 ^ (p' + 2) - 1) * k
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
use k
case intro
p' : ℕ
k : ℤ
h : (fun n => ↑n) (s p') = (fun n => ↑n) ((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : s p' = (2 ^ (p' + 2) - 1) * k
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
replace h := congr_arg (fun n : ℤ => (n : X (q (p' + 2)))) h
case intro
p' : ℕ
k : ℤ
h : ↑(s p') = ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : (fun n => ↑n) (s p') = (fun n => ↑n) ((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
dsimp at h
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' + ωb ^ 2 ^ p' = ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : ↑(s p') = ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
rw [closed_form] at h
case intro
p' : ℕ
k : ℤ
h : (fun x => ω ^ 2 ^ p' * x) (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = (fun x => ω ^ 2 ^ p' * x) ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' + ωb ^ 2 ^ p' = ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
replace h := congr_arg (fun x => ω ^ 2 ^ p' * x) h
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : (fun x => ω ^ 2 ^ p' * x) (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = (fun x => ω ^ 2 ^ p' * x) ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
dsimp at h
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
have t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1) := by ring
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
rw [mul_add, ← pow_add ω, t, ← mul_pow ω ωb (2 ^ p'), ω_mul_ωb, one_pow] at h
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑(2 ^ (p' + 2) - 1) * ↑k * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
rw [mul_comm, coe_mul] at h
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑(2 ^ (p' + 2) - 1) * ↑k * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
rw [mul_comm _ (k : X (q (p' + 2)))] at h
case intro
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
replace h := eq_sub_of_add_eq h
case intro
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
this : 1 ≤ 2 ^ (p' + 2)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
case intro
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
have : 1 ≤ 2 ^ (p' + 2) := Nat.one_le_pow _ _ (by decide)
no goals
case intro
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
this : 1 ≤ 2 ^ (p' + 2)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
exact_mod_cast h
no goals
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
⊢ 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
ring
no goals
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
⊢ 0 < 2
decide