Skip to content

Instantly share code, notes, and snippets.

@jorendorff
Last active July 15, 2020 16:11
  • Star 2 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save jorendorff/e50832fc9d58722015c7a488cd62c860 to your computer and use it in GitHub Desktop.
-- 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
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment