Book VII · Proposition 1

VII.1

Two unequal numbers being set out, and the less being continually subtracted in turn from the greater, if the number which is left never measures the one before it until an unit is left, the original numbers will be prime to one another.Heath, 1908

The termination test of the Euclidean algorithm, read as a criterion: the subtraction runs down to a unit exactly when the numbers are coprime.

Every step, checked

• the numbers are unequal and greater than a unitgiven
• the subtraction terminatesby VII.1
• what is left when it does is the only common measure the two admitby Def.VII.12
• so if a unit is left, the numbers are prime to one anotherby Def.VII.12

What it needs, and what needs it

Needs: nothing earlier.

Used by: VII.2

Rests on: Def.VII.12

Depth: 0 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(
    "VII.1",
    THEOREM,
    sample=_two_unequal,
    note="The termination test of the Euclidean algorithm, read as a criterion: "
    "the subtraction runs down to a unit exactly when the numbers are coprime.",
)
def prop_VII_1(a: int, b: int) -> Out:
    hypothesis("the numbers are unequal and greater than a unit", a > b > 1, guard=True)
    trail = anthyphairesis_integers(a, b)
    reached_a_unit = gcd(a, b) == 1

    claim("the subtraction terminates", "VII.1", trail and trail[-1] == 0)
    claim("what is left when it does is the only common measure the two admit",
          "Def.VII.12",
          not any(measures(d, a) and measures(d, b) for d in range(2, b + 1))
          == reached_a_unit)
    claim("so if a unit is left, the numbers are prime to one another",
          "Def.VII.12", reached_a_unit == coprime(a, b))
    return Out(remainders=trail, coprime=reached_a_unit)