Book VII · Proposition 19

VII.19

If four numbers be proportional, the number produced from the first and fourth will be equal to the number produced from the second and third; and, if the number produced from the first and fourth be equal to that produced from the second and third, the four numbers will be proportional.Heath, 1908

The rule of three for numbers, and its converse: proportion and equal products say the same thing.

Every step, checked

• all four are numbersgiven
• the four are proportional in Euclid's sensegiven
• the product of the extremes equals the product of the meansby VII.19
• and conversely, equal products bring the pairs to the same least termsby VII.19

What it needs, and what needs it

Needs: nothing earlier.

Used by: IX.18 IX.19

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.19",
    THEOREM,
    sample=_proportional_numbers,
    note="The rule of three for numbers, and its converse: proportion and equal "
    "products say the same thing.",
)
def prop_VII_19(a: int, b: int, c: int, d: int) -> Out:
    hypothesis("all four are numbers", all(n > 1 for n in (a, b, c, d)), guard=True)
    # Def.VII.20: numbers are proportional when the first is the same multiple,
    # part or parts of the second that the third is of the fourth -- which is to
    # say the two pairs agree once reduced to least terms.
    hypothesis("the four are proportional in Euclid's sense",
               least_terms(a, b) == least_terms(c, d))
    claim("the product of the extremes equals the product of the means", "VII.19",
          a * d == b * c)
    claim("and conversely, equal products bring the pairs to the same least terms",
          "VII.19",
          all(least_terms(x, y) == least_terms(z, w)
              for x, y, z, w in ((a, b, c, d), (c, d, a, b))
              if x * w == y * z))
    return Out()