case pp
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ Nat.Prime 2

case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)

case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) = 2 ^ (p' + 2)
apply Nat.eq_prime_pow_of_dvd_least_prime_pow
no goals
case pp
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ Nat.Prime 2
exact Nat.prime_two
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
⊢ False
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
intro o
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ωUnit (p' + 2) ^ 2 ^ (p' + 1) = 1
⊢ False
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
⊢ False
have ω_pow := orderOf_dvd_iff_pow_eq_one.1 o
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ↑(Units.coeHom (X (q (p' + 2)))) (ωUnit (p' + 2) ^ 2 ^ (p' + 1)) = ↑(Units.coeHom (X (q (p' + 2)))) 1
⊢ False
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ωUnit (p' + 2) ^ 2 ^ (p' + 1) = 1
⊢ False
replace ω_pow :=
  congr_arg (Units.coeHom (X (q (p' + 2))) : Units (X (q (p' + 2))) → X (q (p' + 2))) ω_pow
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
⊢ False
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ↑(Units.coeHom (X (q (p' + 2)))) (ωUnit (p' + 2) ^ 2 ^ (p' + 1)) = ↑(Units.coeHom (X (q (p' + 2)))) 1
⊢ False
simp at ω_pow
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
⊢ False
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
⊢ False
have h : (1 : ZMod (q (p' + 2))) = -1 :=
  congr_arg Prod.fst (ω_pow.symm.trans (ω_pow_eq_neg_one p' h))
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
this : Fact (2 < ↑(q (p' + 2)))
⊢ False
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
⊢ False
haveI : Fact (2 < (q (p' + 2) : ℕ)) := ⟨two_lt_q _⟩
no goals
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : ω ^ 2 ^ (p' + 1) = 1
h : 1 = -1
this : Fact (2 < ↑(q (p' + 2)))
⊢ False
apply ZMod.neg_one_ne_one h.symm
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1) = 1
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)
apply orderOf_dvd_iff_pow_eq_one.2
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1)) = ↑1
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1) = 1
apply Units.ext
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2)) ^ 2 ^ (p' + 1 + 1) = 1
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1)) = ↑1
push_cast
no goals
case h₂.a
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2)) ^ 2 ^ (p' + 1 + 1) = 1
exact ω_pow_eq_one p' h