primes-euclid.lean

import data.nat.prime
import data.finset
import algebra.big_operators
import tactic
open_locale big_operators

-- Each element of a finite set divides the product of all that set's elements.
lemma dvd_product_of_mem {S : finset ℕ} {x : ℕ} (hx : x ∈ S)
  : x ∣ ∏ y in S, y
:= by {
  use ∏ y in S.erase x, y,
  rw ←(finset.prod_insert (S.not_mem_erase x)), congr, rwa finset.insert_erase hx
}

-- There are infinitely many primes.
-- (Literally, "there is no finite set of all primes".)
theorem exists_infinite_primes : ¬∃ P : finset ℕ, ∀ k : ℕ, k ∈ P ↔ k.prime
:= by {
  -- Suppose there were. Call that set P.
  rintro ⟨P, hP⟩,

  -- Construct n such that no number in P divides n.
  let n := (∏ p in P, p) + 1,
  have no_dvd: ¬∃ p ∈ P, p ∣ n, by {
    rintro ⟨p, hp, hpn⟩,
    have : p ∣ 1, from (nat.dvd_add_iff_right (dvd_product_of_mem hp)).mpr hpn,
    have : ¬ p ∣ 1, from ((hP p).mp hp).not_dvd_one,
    contradiction
  },

  -- And now for the most difficult part of the proof: showing that n isn't 1.
  have n_ne_1 : ¬ n = 1, by {
    by_contradiction hn1,                                     -- if n were 1, then
    have : (∏ p in P, p) = 0 := nat.succ.inj hn1,             -- the product would be 0, so
    obtain ⟨p, hpP, hpz⟩ := finset.prod_eq_zero_iff.mp this,  -- some p ∈ P would have to be 0,
    rw hP at hpP, exact ne_of_gt hpP.pos hpz                  -- but all primes are positive.
  },

  -- Now this number n has some prime factor p.
  let p := n.min_fac,
  have pn : p ∣ n, from nat.min_fac_dvd n,
  have pp : p.prime, from nat.min_fac_prime n_ne_1,

  -- But this is a prime number not in P, a contradiction.
  apply no_dvd, use p, finish
}