Book VII · Proposition 2

VII.2

Given two numbers not prime to one another, to find their greatest common measure.Heath, 1908

The Euclidean algorithm. Euclid states it as continual subtraction of the less from the greater -- the same procedure that, applied to magnitudes rather than numbers, becomes the anthyphairesis of Book X.

Every step, checked

• both numbers are greater than a unitgiven
• the result measures both numbersby VII.1
• and every common measure measures itby VII.2

What it needs, and what needs it

Needs: VII.1

Used by: VII.3

Rests on: Def.VII.12

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(
    "VII.2",
    CONSTRUCTION,
    sample=_two_numbers,
    note="The Euclidean algorithm. Euclid states it as continual subtraction of the "
    "less from the greater -- the same procedure that, applied to magnitudes rather "
    "than numbers, becomes the anthyphairesis of Book X.",
)
def prop_VII_2(a: int, b: int) -> Out:
    hypothesis("both numbers are greater than a unit", a > 1 and b > 1, guard=True)
    measure = gcd(a, b)
    because(prop_VII_1, a, b) if a > b > 1 else None

    claim("the result measures both numbers", "VII.1", a % measure == 0 and b % measure == 0)
    claim("and every common measure measures it", "VII.2",
          all(measure % d == 0 for d in range(1, min(a, b) + 1) if a % d == 0 and b % d == 0))
    return Out(measure=measure, remainders=anthyphairesis_integers(max(a, b), min(a, b)))