Book X · Proposition 3

X.3

Given two commensurable magnitudes, to find their greatest common measure.Heath, 1908

Every step, checked

• the magnitudes are positivegiven
• they are commensurablegiven
• the measure found measures bothby X.3
• it measures them a whole number of timesby Def.X.1
• and it is the greatest such, the two counts having no common factorby VII.22

What it needs, and what needs it

Needs: VII.22

Used by: X.4

Rests on: Def.X.1

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(
    "X.3",
    CONSTRUCTION,
    sample=_commensurable_pair,
)
def prop_X_3(a, b) -> Out:
    hypothesis("the magnitudes are positive", sign(a) > 0 and sign(b) > 0, guard=True)
    hypothesis("they are commensurable", commensurable(a, b))
    measure = common_measure(a, b)

    because(prop_VII_22, 2, 3)

    claim("the measure found measures both", "X.3",
          isinstance(a / measure, Fraction) and isinstance(b / measure, Fraction))
    claim("it measures them a whole number of times", "Def.X.1",
          (a / measure).denominator == 1 and (b / measure).denominator == 1)
    claim("and it is the greatest such, the two counts having no common factor",
          "VII.22", gcd_int(int(a / measure), int(b / measure)) == 1)
    return Out(measure=measure)