Book VI · Proposition 16

VI.16

If four straight lines be proportional, the rectangle contained by the extremes is equal to the rectangle contained by the means; and, if the rectangle contained by the extremes be equal to the rectangle contained by the means, the four straight lines will be proportional.Heath, 1908

The rule of three, stated about rectangles: the product of the extremes equals the product of the means.

Every step, checked

• the four lines are genuine magnitudesgiven
• the four are proportionalgiven
• the rectangle contained by the extremes equals that by the meansby VI.14
• and conversely, equal rectangles leave no equimultiples that separate the ratiosby VI.14

What it needs, and what needs it

Needs: VI.14

Used by: VI.17 X.112 X.113

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.4, Post.5, V.Def.5

Depth: 16 steps of argument above the first principles. Parallel postulate: needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "VI.16",
    THEOREM,
    sample=_four_proportional_lines,
    note="The rule of three, stated about rectangles: the product of the extremes "
    "equals the product of the means.",
)
def prop_VI_16(a: Point, b: Point, c: Point, d: Point,
               e: Point, f: Point, g: Point, h: Point) -> Out:
    """The four lines are AB, CD, EF and GH, drawn one under another."""
    for pair in ((a, b), (c, d), (e, f), (g, h)):
        line(*pair)
    first, second = length(a, b), length(c, d)
    third, fourth = length(e, f), length(g, h)
    hypothesis("the four lines are genuine magnitudes",
               all(sign(x) > 0 for x in (first, second, third, fourth)), guard=True)
    # Proportion for magnitudes is Eudoxus' Definition 5, which is decided by
    # looking for equimultiples that separate the ratios. Stating the hypothesis
    # that way keeps the two halves of this proposition from collapsing into one
    # rewriting of the same product.
    hypothesis("the four are proportional",
               separating_witness(first, second, third, fourth) is None)

    # The two rectangles, built and drawn, so the claim is about figures.
    by_extremes = _standing_on(a, b, fourth)
    by_means = _standing_on(c, d, third)
    outline(*by_extremes)
    outline(*by_means)

    because(prop_VI_14, by_extremes[0], by_extremes[1], by_extremes[3],
            by_means[0], by_means[1], by_means[3])

    claim("the rectangle contained by the extremes equals that by the means",
          "VI.14", _area(*by_extremes) == _area(*by_means))
    claim("and conversely, equal rectangles leave no equimultiples that separate "
          "the ratios", "VI.14",
          (_area(*by_extremes) == _area(*by_means))
          == (separating_witness(first, second, third, fourth) is None))
    return Out(rectangles=(by_extremes, by_means))