Book II · Proposition 3

II.3

If a straight line be cut at random, the rectangle contained by the whole and one of the segments is equal to the rectangle contained by the segments and the square on the aforesaid segment.Heath, 1908

Every step, checked

• B cuts ACgiven
• BF divides the rectangle into twoby C.N.2
• the far piece is the square on BCby Def.22
• so the rectangle on the whole and one segment equals the rectangle on the segments together with the square on that segmentby C.N.2

What it needs, and what needs it

Needs: nothing earlier.

Rests on: C.N.2, Def.22

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

What it takes on trust

• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "II.3",
    THEOREM,
    sample=_adjacent_segments,
)
def prop_II_3(a: Point, b: Point, c: Point) -> Out:
    """AC is cut at B; the rectangle stands on AC with height BC."""
    hypothesis("B cuts AC", between(a, b, c))

    lift = _across(b, c)
    whole = _rectangle(a, c, lift, "E", "D")
    cut = posit(Point(b.x + lift[0], b.y + lift[1]), "F")
    line(b, cut, "BF, dividing the rectangle")

    on_segments = (a, b, cut, whole[3])
    square = (b, c, whole[2], cut)
    claim("BF divides the rectangle into two", "C.N.2",
          _area(*on_segments) + _area(*square) == _area(*whole))
    claim("the far piece is the square on BC", "Def.22",
          _area(*square) == len2(b, c) and right_angle(a, b, cut) and eq_len(b, c, b, cut))
    claim("so the rectangle on the whole and one segment equals the rectangle on the "
          "segments together with the square on that segment", "C.N.2",
          _area(*whole) == _area(*on_segments) + len2(b, c))
    return Out(rectangle=whole)