Book II · Proposition 10

II.10

If a straight line be bisected, and a straight line be added to it in a straight line, the square on the whole with the added straight line and the square on the added straight line both together are double of the square on the half and of the square described on the straight line made up of the half and the added straight line as on one straight line.Heath, 1908

Every step, checked

• B lies between A and Dgiven
• CE is the half set up at right anglesby I.11
• the squares on the whole with the addition and on the addition are double the square on the half and the square on the half with the additionby I.47, II.4

What it needs, and what needs it

Needs: I.10 I.11 I.47 II.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: 15 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 (×36)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×83)continuity
• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "II.10",
    THEOREM,
    sample=_bisected_and_produced,
)
def prop_II_10(a: Point, b: Point, d: Point) -> Out:
    """AB is bisected at C and produced to D."""
    hypothesis("B lies between A and D", between(a, b, d))
    c = posit(prop_I_10(a, b).midpoint, "C")
    outline(a, d, close=False)

    apex = posit(Point(c.x + _across(c, b)[0], c.y + _across(c, b)[1]), "E")
    outline(a, apex, b, close=False)
    line(apex, d, "ED")

    # CE is the perpendicular I.11 erects at C, the right-angled triangles
    # standing on it are I.47's, and the produced line is II.4's.
    because(prop_I_11, a, d, c)
    because(prop_I_47, a, c, apex)
    because(prop_I_47, d, c, apex)
    because(prop_I_47, b, c, apex)
    because(prop_II_4, a, b, d)

    claim("CE is the half set up at right angles", "I.11",
          right_angle(apex, c, b) and eq_len(c, apex, c, b))
    claim("the squares on the whole with the addition and on the addition are double "
          "the square on the half and the square on the half with the addition",
          ["I.47", "II.4"],
          len2(a, d) + len2(b, d) == 2 * (len2(a, c) + len2(c, d)))
    return Out(midpoint=c, apex=apex)