Book II · Proposition 1

II.1

If there be two straight lines, and one of them be cut into any number of segments whatever, the rectangle contained by the two straight lines is equal to the rectangles contained by the uncut straight line and each of the segments.Heath, 1908

The distributive law, a(x+y+z) = ax+ay+az, stated about areas. Every later proposition in the book is a special case of it.

Every step, checked

• D and E cut BC, in that ordergiven
• BG is at right angles to BCgiven
• the three rectangles together fill the whole oneby C.N.2
• so the rectangle on the uncut line and the whole equals the rectangles on the uncut line and each segmentby C.N.2

What it needs, and what needs it

Needs: nothing earlier.

Rests on: C.N.2

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 figure (×3)order

The proposition as code

@proposition(
    "II.1",
    THEOREM,
    sample=_cut_and_lifted,
    note="The distributive law, a(x+y+z) = ax+ay+az, stated about areas. Every "
    "later proposition in the book is a special case of it.",
)
def prop_II_1(b: Point, c: Point, d: Point, e: Point, g: Point) -> Out:
    """BC is cut at D and E; BG is the uncut line, set up at right angles."""
    hypothesis("D and E cut BC, in that order",
               between(b, d, c) and between(b, e, c) and between(d, e, c))
    hypothesis("BG is at right angles to BC", right_angle(g, b, c))

    lift = (g.x - b.x, g.y - b.y)
    whole = _rectangle(b, c, lift, "G", "H")
    first = _rectangle(b, d, lift, "G", "K")
    middle = _rectangle(d, e, lift, "K", "L")
    last = _rectangle(e, c, lift, "L", "H")

    claim("the three rectangles together fill the whole one", "C.N.2",
          _area(*first) + _area(*middle) + _area(*last) == _area(*whole))
    claim("so the rectangle on the uncut line and the whole equals the rectangles "
          "on the uncut line and each segment", "C.N.2",
          _area(*whole) == _area(*first) + _area(*middle) + _area(*last))
    return Out(whole=whole, parts=(first, middle, last))