Book VII · Proposition 3

VII.3

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

Every step, checked

• all three are greater than a unitgiven
• the measure found measures all threeby VII.2
• and every common measure of the three measures itby VII.2

What it needs, and what needs it

Needs: VII.2

Rests on: Def.VII.12

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(
    "VII.3",
    CONSTRUCTION,
    sample=three_numbers,
)
def prop_VII_3(a: int, b: int, c: int) -> Out:
    hypothesis("all three are greater than a unit", a > 1 and b > 1 and c > 1, guard=True)
    measure = gcd(gcd(a, b), c)
    because(prop_VII_2, a, b)

    claim("the measure found measures all three", "VII.2",
          all(measures(measure, n) for n in (a, b, c)))
    claim("and every common measure of the three measures it", "VII.2",
          all(measures(d, measure) for d in range(1, min(a, b, c) + 1)
              if all(measures(d, n) for n in (a, b, c))))
    return Out(measure=measure)