Book VI · Proposition 17

VI.17

If three straight lines be proportional, the rectangle contained by the extremes is equal to the square on the mean; and, if the rectangle contained by the extremes be equal to the square on the mean, the three straight lines will be proportional.Heath, 1908

The special case of VI.16 where the means coincide, and the one that makes a mean proportional the side of an equal square.

Every step, checked

• the three lines are genuine magnitudesgiven
• they are proportionalgiven
• the drawn figures really are the rectangle and the squareby Def.22
• so the rectangle contained by the extremes equals the square on the meanby VI.16
• and conversely the equality makes the three proportionalby VI.16

What it needs, and what needs it

Needs: VI.16

Used by: VI.30

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

Depth: 17 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.17",
    THEOREM,
    sample=_three_proportional_lines,
    note="The special case of VI.16 where the means coincide, and the one that "
    "makes a mean proportional the side of an equal square.",
)
def prop_VI_17(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    """The three lines are AB, CD and EF, laid out one under another."""
    for pair in ((a, b), (c, d), (e, f)):
        line(*pair)
    first, mean, last = length(a, b), length(c, d), length(e, f)
    hypothesis("the three lines are genuine magnitudes",
               all(sign(x) > 0 for x in (first, mean, last)), guard=True)
    hypothesis("they are proportional", first * last == mean * mean)

    # The rectangle contained by the extremes, and the square on the mean, both
    # built and drawn: the claim is then about figures rather than products.
    rectangle = _standing_on(a, b, last)
    square = _standing_on(c, d, mean)
    outline(*rectangle)
    outline(*square)

    # Three proportionals are four with the mean written twice, which is the
    # figure VI.16 speaks of.
    because(prop_VI_16, a, b, c, d, c, d, e, f)

    claim("the drawn figures really are the rectangle and the square", "Def.22",
          _area(*rectangle) == first * last and _area(*square) == mean * mean)

    claim("so the rectangle contained by the extremes equals the square on the mean",
          "VI.16", _area(*rectangle) == _area(*square))
    claim("and conversely the equality makes the three proportional", "VI.16",
          (_area(*rectangle) == _area(*square)) == (first * last == mean * mean))
    return Out(rectangle=rectangle, square=square)