Book IX · Proposition 20

IX.20

Prime numbers are more than any assigned multitude of prime numbers.Heath, 1908

Euclid's proof is constructive and is not a proof by contradiction: given any finite list of primes it exhibits a prime outside it. The machine runs the construction rather than paraphrasing it.

Every step, checked

• a finite list of primes is givengiven
• the product of the given primes, with a unit added, is measured by no prime in the listby VII.31
• yet it is measured by some primeby VII.31
• so that prime is not among those given, and the list was not completeby IX.20

What it needs, and what needs it

Needs: VII.31

Rests on: Def.VII.3

Depth: 1 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "IX.20",
    CONSTRUCTION,
    sample=_prime_list,
    note="Euclid's proof is constructive and is not a proof by contradiction: given "
    "any finite list of primes it exhibits a prime outside it. The machine runs the "
    "construction rather than paraphrasing it.",
)
def prop_IX_20(given: list) -> Out:
    hypothesis("a finite list of primes is given", all(is_prime(p) for p in given) and given)

    product = 1
    for prime in given:
        product *= prime
    candidate = product + 1

    # Euclid's step is about the number with the unit added, not the product:
    # if it is not itself prime, VII.31 finds the prime that measures it. The
    # appeal was written on the product, where it says nothing.
    if candidate > 3 and not is_prime(candidate):
        because(prop_VII_31, candidate)

    claim("the product of the given primes, with a unit added, is measured by no "
          "prime in the list", "VII.31", all(candidate % p != 0 for p in given))
    fresh = prime_factors(candidate)[0]
    claim("yet it is measured by some prime", "VII.31", is_prime(fresh))
    claim("so that prime is not among those given, and the list was not complete",
          "IX.20", fresh not in given)
    return Out(new_prime=fresh, from_product=candidate)