Book VII · Proposition 4

VII.4

Any number is either a part or parts of any number, the less of the greater.Heath, 1908

Every ratio of numbers is a fraction -- Euclid's 'part' when the numerator is a unit, 'parts' when it is not.

Every step, checked

• the numbers are unequal and greater than a unitgiven
• the less is a part of the greater when it measures itby Def.VII.3
• and parts of it otherwise, so many of the greater's parts as the numerator countsby Def.VII.4
• the two counts have no common measure but a unit, so the description is the plainest there isby Def.VII.12

What it needs, and what needs it

Needs: nothing earlier.

Rests on: Def.VII.12, Def.VII.3, Def.VII.4

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.4",
    THEOREM,
    sample=_two_unequal,
    note="Every ratio of numbers is a fraction -- Euclid's 'part' when the "
    "numerator is a unit, 'parts' when it is not.",
)
def prop_VII_4(a: int, b: int) -> Out:
    hypothesis("the numbers are unequal and greater than a unit", a > b > 1, guard=True)
    numerator, denominator = least_terms(b, a)
    claim("the less is a part of the greater when it measures it", "Def.VII.3",
          (numerator == 1) == measures(b, a))
    claim("and parts of it otherwise, so many of the greater's parts as the "
          "numerator counts", "Def.VII.4",
          b * denominator == a * numerator)
    claim("the two counts have no common measure but a unit, so the description "
          "is the plainest there is", "Def.VII.12", coprime(numerator, denominator))
    return Out(terms=(numerator, denominator))