Book II · Proposition 4

II.4

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

(a+b)^2 = a^2 + 2ab + b^2, four centuries before algebraic notation.

Every step, checked

• B cuts ACgiven
• the segments together make the wholeby C.N.2
• the two cuts leave four figures that fill the squareby C.N.2
• the squares on the segments stand about the diameterby I.43
• two of them are the squares on the segmentsby I.46
• and the other two, being the complements about the diameter, are each the rectangle contained by the segmentsby I.43
• so the square on the whole equals the squares on the parts together with twice the rectangle they containby I.43, I.46

What it needs, and what needs it

Needs: I.43 I.46

Used by: II.7 II.8 II.9 II.10 II.12

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

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×8)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×18)continuity
• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "II.4",
    THEOREM,
    sample=_adjacent_segments,
    note="(a+b)^2 = a^2 + 2ab + b^2, four centuries before algebraic notation.",
)
def prop_II_4(a: Point, b: Point, c: Point) -> Out:
    """AC is cut at B, and the square on AC is cut both ways through B."""
    hypothesis("B cuts AC", between(a, b, c))

    # The square on the whole, divided as Euclid divides it: the two cuts
    # through B leave the squares on the two segments at opposite corners, and
    # the rectangle they contain twice over between them.
    low, high = _across(a, b), _across(b, c)
    lift = (low[0] + high[0], low[1] + high[1])
    d = posit(Point(a.x + lift[0], a.y + lift[1]), "D")
    e = posit(Point(c.x + lift[0], c.y + lift[1]), "E")
    outline(a, c, e, d)
    f = posit(Point(b.x + lift[0], b.y + lift[1]), "F")
    g = posit(Point(a.x + low[0], a.y + low[1]), "G")
    h = posit(Point(b.x + low[0], b.y + low[1]), "H")
    k = posit(Point(c.x + low[0], c.y + low[1]), "K")
    line(b, f, "BF")
    line(g, k, "GK")
    # Euclid draws the diameter, because his reason for the two rectangles being
    # equal is I.43: they are the complements of the figures about it. Drawing
    # it is what makes the cited step visible in the figure.
    line(a, e, "the diameter AE")

    on_first, on_second = (a, b, h, g), (h, k, e, f)
    between_them = ((b, c, k, h), (g, h, f, d))
    whole = length(a, c)
    first, second = length(a, b), length(b, c)

    # ACED is the parallelogram, AE its diameter and H the point on it, which
    # is I.43's own configuration; and the two figures said to be squares are
    # built as such, on AB and on HK.
    because(prop_I_43, a, c, e, d, h)
    because(prop_I_46, a, b)
    because(prop_I_46, h, k)

    claim("the segments together make the whole", "C.N.2", first + second == whole)
    claim("the two cuts leave four figures that fill the square", "C.N.2",
          _area(a, c, e, d)
          == _area(*on_first) + _area(*on_second)
          + _area(*between_them[0]) + _area(*between_them[1]))
    claim("the squares on the segments stand about the diameter", "I.43",
          on_line(h, Line.through(a, e)))
    claim("two of them are the squares on the segments", "I.46",
          _area(*on_first) == first * first and _area(*on_second) == second * second)
    claim("and the other two, being the complements about the diameter, are each the "
          "rectangle contained by the segments", "I.43",
          _area(*between_them[0]) == first * second
          and _area(*between_them[1]) == first * second)
    claim("so the square on the whole equals the squares on the parts together with "
          "twice the rectangle they contain", ["I.43", "I.46"],
          whole * whole == first * first + second * second + 2 * first * second)
    return Out(square=(a, c, e, d), pieces=(on_first, on_second) + between_them)