Book II · Proposition 7

II.7

If a straight line be cut at random, the square on the whole and that on one of the segments both together are equal to twice the rectangle contained by the whole and the said segment and the square on the remaining segment.Heath, 1908

(a+b)^2 + b^2 = 2(a+b)b + a^2.

Every step, checked

• B cuts ACgiven
• the square on the whole is the figure drawn on ACby I.46
• the squares on the whole and on one segment together equal twice the rectangle on the whole and that segment, with the square on the restby II.4, C.N.2

What it needs, and what needs it

Needs: I.46 II.4

Used by: II.8 II.13 XIII.4

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: 13 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 (×3)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×8)continuity
• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "II.7",
    THEOREM,
    sample=_adjacent_segments,
    note="(a+b)^2 + b^2 = 2(a+b)b + a^2.",
)
def prop_II_7(a: Point, b: Point, c: Point) -> Out:
    """AC is cut at B; the squares are on AC and on BC."""
    hypothesis("B cuts AC", between(a, b, c))

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

    whole, part, rest = length(a, c), length(b, c), length(a, b)
    because(prop_I_46, a, c)
    because(prop_II_4, a, b, c)

    claim("the square on the whole is the figure drawn on AC", "I.46",
          _area(*square) == whole * whole)
    claim("the squares on the whole and on one segment together equal twice the "
          "rectangle on the whole and that segment, with the square on the rest",
          ["II.4", "C.N.2"],
          whole * whole + part * part == 2 * (whole * part) + rest * rest)
    return Out(square=square)