exact hpri.out
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
key : ↑↑p ∣ ∑ i : Fin p, f a b ↑k₁ ↑k₂ ↑i • ζ ^ ↑i
⊢ (↑⟨p, ⋯⟩).Prime
no goals