English
For every n, there exists a prime p with p ≥ n.
Русский
Для каждого n существует простое p, такое что p ≥ n.
LaTeX
$$$\\forall n \\\\in \\\\mathbb{N}, \\\\exists p \\\\ge n \\\\land \\\\mathrm{Prime}(p)$$$
Lean4
/-- Euclid's theorem on the **infinitude of primes**.
Here given in the form: for every `n`, there exists a prime number `p ≥ n`. -/
theorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Prime p :=
let p := minFac (n ! + 1)
have f1 : n ! + 1 ≠ 1 := ne_of_gt <| succ_lt_succ <| factorial_pos _
have pp : Prime p := minFac_prime f1
have np : n ≤ p :=
le_of_not_ge fun h =>
have h₁ : p ∣ n ! := dvd_factorial (minFac_pos _) h
have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
pp.not_dvd_one h₂
⟨p, np, pp⟩
