primes.lean

-- A One-Line Proof of the Infinitude of Primes
-- [The American Mathematical Monthly, Vol. 122, No. 5 (May 2015), p. 466]
-- https://twitter.com/pickover/status/1281229359349719043

import data.finset.basic -- for finset, finset.insert_erase
import data.nat.prime -- for nat.{prime,min_fac} and related lemmas
import data.real.basic -- for real.nontrivial, real.domain
import analysis.special_functions.trigonometric -- for real.sin and related identities
import algebra.big_operators -- for notation `∏`, finset.prod_*
import algebra.ring -- for domain.to_no_zero_divisors
import algebra.ordered_ring -- for lt_mul_of_one_lt_right'
import algebra.ordered_field -- for div_lt_iff
import tactic
import tactic.nth_rewrite.default  -- for nth_rewrite_rhs

open_locale big_operators

notation `π` := real.pi

-- The sine function has a period of 2π.
lemma sin_periodic (x : ℝ) (n : ℕ)
  : real.sin x = real.sin (x + 2 * real.pi * n)
:= by {
  induction n with n' ih, { simp },
  rw [nat.cast_succ, mul_add, mul_one, ←add_assoc, real.sin_add_two_pi], exact ih,
}

-- 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
}

-- Given a finite set of all primes, a certain product of sines is positive.
lemma product_sin_pos {P : finset ℕ} (hP : ∀ k : ℕ, k ∈ P ↔ k.prime)
  : 0 < ∏ p in P, real.sin (π / p)
:= by {
  apply finset.prod_pos,  -- because each multiplicand is positive.
  intros p hp, rw hP at hp,
  have p_pos : 0 < (p : ℝ) := by exact_mod_cast hp.pos,
  -- In turn each sine is positive because π/p is between 0 and π.
  apply real.sin_pos_of_pos_of_lt_pi,
  { exact div_pos real.pi_pos p_pos },
  rw div_lt_iff p_pos,
  apply lt_mul_of_one_lt_right', { exact real.pi_pos },
  rw ←nat.cast_one,
  norm_cast,
  exact hp.two_le
}

-- Given a finite set of all primes, two products of sines are equal.
lemma product_sin_eq {P : finset ℕ} (hP : ∀ k : ℕ, k ∈ P ↔ k.prime)
  : ∏ p in P, real.sin (π / p) = ∏ p in P, real.sin (π * ↑(1 + 2 * ∏ p' in P, p') / p)
:= by {
  apply finset.prod_congr rfl,  -- because the multiplicands are equal.
  intros p hp,
  obtain ⟨n, hn⟩ := dvd_product_of_mem hp,
  push_cast, norm_num, rw [mul_add, add_div, mul_one, ←mul_assoc, mul_comm π 2, mul_div_assoc],
  rw (show ((∏ p' in P, p') : ℝ) / (p : ℝ) = n, by {
        norm_cast, rw hn, push_cast, apply mul_div_cancel_left_of_imp, intro hpz,
        have : 0 < (p : ℝ) := by { rw hP at hp, exact_mod_cast hp.pos }, linarith,
     }),
  apply sin_periodic
}

-- Given a finite set of all primes, a certain product of sines is zero.
lemma product_sin_pi_mul_eq_zero {P : finset ℕ} (hP : ∀ k : ℕ, k ∈ P ↔ k.prime)
  : ∏ p in P, real.sin (π * ↑(1 + 2 * (∏ p' in P, p')) / p) = 0
:= by {
  rw finset.prod_eq_zero_iff,  -- because at least one of the multiplicands is zero.

  -- The numerator of the fraction is > 1.
  let n := 1 + 2 * ∏ p' in P, p',
  have n_gt_one : n > 1 := by {
    dsimp [n], nth_rewrite_rhs 0 ←add_zero 1,
    rw gt_iff_lt, rw add_lt_add_iff_left,
    suffices h : (0 < ∏ p' in P, p'), { finish },
    rw ←(@nat.cast_lt ℝ), push_cast,
    apply finset.prod_pos,
    intro p', rw hP, intro hp', change 0 < (p' : ℝ), exact_mod_cast hp'.pos
  },

  -- Let p be any prime factor of the numerator of the fraction (we pick
  -- the minimum prime factor).
  let p := n.min_fac,
  use p,
  split, { rw hP, apply nat.min_fac_prime, exact ne_of_gt n_gt_one },

  -- Then the argument to `sin` is a multiple of pi, which makes the sine zero.
  dsimp [←n],
  rw real.sin_eq_zero_iff,
  obtain ⟨q, hq⟩ := n.min_fac_dvd,
  use q, rw [mul_comm, mul_div_assoc, hq], dsimp [p],
  push_cast, rw [mul_div_cancel_left],
  norm_cast, nlinarith
}

-- 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 {
  rintro ⟨P, hP⟩,  -- For suppose there were. Then we have 0 < 0, by:
  have := calc
      0 < ∏ p in P, real.sin (π / p)                              : product_sin_pos hP
    ... = ∏ p in P, real.sin (π * ↑(1 + 2 * (∏ p' in P, p')) / p) : product_sin_eq hP
    ... = 0                                                       : product_sin_pi_mul_eq_zero hP,
  linarith
}