English
Fermat's theorem on the sum of two squares: every prime p not congruent to 3 mod 4 can be written as a^2 + b^2 for some a,b ∈ ℕ.
Русский
Теорема Ферма о сумме двух квадратов: каждое простое p, которое не равно 3 по модулю 4, можно представить как p = a^2 + b^2.
LaTeX
$$$\forall p\in\mathbb{N},\ p\text{ prime},\ p\not\equiv 3\pmod{4} \Rightarrow \exists a,b \in \mathbb{N},\ a^2+b^2=p$$$
Lean4
/-- The series over `p^r` for primes `p` converges if and only if `r < -1`. -/
theorem summable_rpow {r : ℝ} : Summable (fun p : Nat.Primes ↦ (p : ℝ) ^ r) ↔ r < -1 :=
by
by_cases h : r < -1
· -- case `r < -1`
simp only [h, iff_true]
exact (Real.summable_nat_rpow.mpr h).subtype _
· -- case `-1 ≤ r`
simp only [h, iff_false]
refine fun H ↦ Nat.Primes.not_summable_one_div <| H.of_nonneg_of_le (fun _ ↦ by positivity) ?_
intro p
rw [one_div, ← Real.rpow_neg_one]
exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast p.prop.one_lt.le) <| not_lt.mp h
