Skip to content
Theorem·T11

Euclid's theorem: infinitude of primes

Above every number there is a prime: the primes never run out.

where "is prime" is the notion of D031, is divisibility, and is the order of D029. There are arbitrarily large, hence infinitely many, primes.
In words
For every n, if n is a natural number then there is a p such that p is prime and p is strictly greater than n. In other words, the primes go on forever.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Fix and let with the factorial and addition.
  2. 2
    exceeds : by L21 (i), so by L15 (v). Adding to both sides ( gives by L17 (iii), with the equality case by substitutivity) and by D027: . Since (L15 (vi): ), transitivity (L15 (ii), equality case by substitutivity) gives .
  3. 3
    By L20, has a prime divisor: a prime with .
  4. 4
    Claim: . Suppose not; then by L16, . Since is prime, , so certainly . With , L21 (ii) applies:
  5. 5
    Now divides both and , so by L19 (vi),
  6. 6
    But ((P3): ), so L19 (vii) gives . Chaining with : (L15 (ii), equality case by substitutivity), contradicting irreflexivity (L15 (i)). The supposition fails (negation, excluded middle), so .

Remarks

Euclid, Elements Book IX, Proposition 20, around 300 BC: perhaps the oldest proof in this library, and still among the most beautiful. Euclid multiplied a given finite list of primes and added one; the factorial variant used here avoids needing finite products of lists while keeping his idea intact: is built to dodge every candidate divisor up to . Note what the proof does not say: need not be prime itself. For : is not prime, but its prime divisor does exceed , exactly as promised. The formal statement "arbitrarily large primes" is the cleanest rendering of "infinitely many" available before infinite cardinalities are developed; with finiteness in hand one checks easily that no finite set can contain all primes, since it would have a largest element.