p : ℕ
w : 1 < p
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0
p : ℕ
w : 1 < p
⊢ lucasLehmerResidue p = 0 ↔ sMod p (p - 2) = 0
dsimp [lucasLehmerResidue]
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 ↔ sMod p (p - 2) = 0
p : ℕ
w : 1 < p
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0
rw [sZMod_eq_sMod p]
case mp
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 → sMod p (p - 2) = 0

case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 ↔ sMod p (p - 2) = 0
constructor
case mp
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ sMod p (p - 2) = 0
case mp
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 → sMod p (p - 2) = 0
intro h
case mp
p : ℕ
w : 1 < p
h : 2 ^ p - 1 ∣ sMod p (p - 2)
⊢ sMod p (p - 2) = 0
case mp
p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ sMod p (p - 2) = 0
simp [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h
p : ℕ
w : 1 < p
⊢ 0 ≤ sMod p (p - 2)

p : ℕ
w : 1 < p
⊢ sMod p (p - 2) < 2 ^ p - 1
case mp
p : ℕ
w : 1 < p
h : 2 ^ p - 1 ∣ sMod p (p - 2)
⊢ sMod p (p - 2) = 0
apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _ h <;> clear h
no goals
p : ℕ
w : 1 < p
⊢ 0 ≤ sMod p (p - 2)
apply sMod_nonneg _ (Nat.lt_of_succ_lt w)
no goals
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) < 2 ^ p - 1
exact sMod_lt _ (Nat.lt_of_succ_lt w) (p - 2)
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑(sMod p (p - 2)) = 0
case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0
intro h
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑0 = 0
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑(sMod p (p - 2)) = 0
rw [h]
no goals
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑0 = 0
simp