Book IX · Proposition 14

IX.14

If a number be the least that is measured by prime numbers, it will not be measured by any other prime number except those originally measuring it.Heath, 1908

Unique factorisation, in the only form Euclid states it.

Every step, checked

• the given numbers are primegiven
• the number found is the least measured by them allby VII.36
• and no other prime measures itby VII.30

What it needs, and what needs it

Needs: VII.30 VII.36

Rests on: Def.VII.3

Depth: 2 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.14",
    THEOREM,
    sample=lambda rng: tuple(sorted(rng.sample([p for p in range(2, 30) if is_prime(p)],
                                               rng.randint(2, 3)))),
    note="Unique factorisation, in the only form Euclid states it.",
)
def prop_IX_14(*primes: int) -> Out:
    hypothesis("the given numbers are prime", all(is_prime(p) for p in primes))
    least = 1
    for prime in primes:
        least *= prime
    because(prop_VII_36, 2, 3, 5)
    for _p in primes:
        because(prop_VII_30, _p, primes[0], least // primes[0])

    claim("the number found is the least measured by them all", "VII.36",
          all(measures(p, least) for p in primes)
          and not any(all(measures(p, m) for p in primes) for m in range(1, least)))
    claim("and no other prime measures it", "VII.30",
          all(measures(p, least) == (p in primes)
              for p in range(2, least + 1) if is_prime(p)))
    return Out(least=least)