Book VII · Proposition 20

VII.20

The least numbers of those which have the same ratio with them measure those which have the same ratio the same number of times, the greater the greater and the less the less.Heath, 1908

The least pair of a ratio divides every other pair of it -- which is why 'lowest terms' is well defined.

Every step, checked

• the four are proportionalgiven
• all four are numbersgiven
• the least terms measure the greater the same number of times as the lessby VII.20
• and they measure the second pair the same wayby VII.20

What it needs, and what needs it

Needs: nothing earlier.

Used by: VII.21 VIII.1 IX.16

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.20",
    THEOREM,
    sample=_proportional_numbers,
    note="The least pair of a ratio divides every other pair of it -- which is "
    "why 'lowest terms' is well defined.",
)
def prop_VII_20(a: int, b: int, c: int, d: int) -> Out:
    hypothesis("the four are proportional", a * d == b * c)
    hypothesis("all four are numbers", all(n > 1 for n in (a, b, c, d)), guard=True)
    least = least_terms(a, b)
    claim("the least terms measure the greater the same number of times as the "
          "less", "VII.20",
          measures(least[0], a) and measures(least[1], b)
          and a // least[0] == b // least[1])
    claim("and they measure the second pair the same way", "VII.20",
          measures(least[0], c) and measures(least[1], d)
          and c // least[0] == d // least[1])
    return Out(least=least)