have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₁ b p j • ζ ^ j := by
  convert hdiv using 1
  have h : 1 ≠ p.pred := fun h => by linarith [pred_eq_succ_iff.1 h.symm]
  simp_rw [f0k₁, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h,
    Finset.range_filter_eq]
  simp [hpri.one_lt, Nat.sub_lt hpri.pos, sub_eq_add_neg]
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ False
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j
⊢ False