Book VI · Proposition 22

VI.22

If four straight lines be proportional, the rectilineal figures similar and similarly described upon them will also be proportional; and, if the rectilineal figures similar and similarly described upon them be proportional, the straight lines will themselves also be proportional.Heath, 1908

Every step, checked

• the four lines are genuine magnitudesgiven
• they are proportionalgiven
• the similar figures on them are proportionalby VI.20
• and conversely, proportional figures make the lines proportionalby VI.20

What it needs, and what needs it

Needs: VI.20

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

Depth: 19 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.22",
    THEOREM,
    sample=_four_proportional_lines,
)
def prop_VI_22(a: Point, b: Point, c: Point, d: Point,
               e: Point, f: Point, g: Point, h: Point) -> Out:
    """Similar figures described on four proportional lines are proportional."""
    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)
    hypothesis("they are proportional", first * fourth == second * third)
    for pair in ((a, b), (c, d), (e, f), (g, h)):
        line(*pair)

    # Squares are the simplest similar figures to describe on them.
    squares = []
    _corners = []
    for start, end in ((a, b), (c, d), (e, f), (g, h)):
        across = (-(end.y - start.y), end.x - start.x)
        corner = (start, end, Point(end.x + across[0], end.y + across[1]),
                  Point(start.x + across[0], start.y + across[1]))
        _corners.append(corner)
        squares.append(_area(*corner))


    # The figures described are squares, and any two squares are similar, so
    # VI.20 speaks of them as it speaks of any similar rectilineal figures.
    because(prop_VI_20, *_corners[0], *_corners[1])

    claim("the similar figures on them are proportional", "VI.20",
          squares[0] * squares[3] == squares[1] * squares[2])
    claim("and conversely, proportional figures make the lines proportional", "VI.20",
          (squares[0] * squares[3] == squares[1] * squares[2])
          == (first * fourth == second * third))
    return Out()