Book II · Proposition 9

II.9

If a straight line be cut into equal and unequal segments, the squares on the unequal segments of the whole are double of the square on the half and of the square on the straight line between the points of section.Heath, 1908

Every step, checked

• D cuts ABgiven
• the two sections are distinctgiven
• CE is the half set up at right anglesby I.11
• the squares on the unequal segments are double the square on the half and the square on the line between the sectionsby 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.9",
    THEOREM,
    sample=_equal_and_unequal,
)
def prop_II_9(a: Point, b: Point, d: Point) -> Out:
    """AB is bisected at C and cut unequally at D."""
    hypothesis("D cuts AB", between(a, d, b))
    c = posit(prop_I_10(a, b).midpoint, "C")
    hypothesis("the two sections are distinct", c != d)
    outline(a, b, close=False)

    # Euclid raises a right-angled isosceles triangle on the half; drawing it is
    # what makes the doubling visible rather than merely algebraic.
    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, and the right-angled triangles
    # standing on it are I.47's; the cut line itself is II.4's.
    because(prop_I_11, a, b, 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, d, b)

    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 unequal segments are double the square on the half "
          "and the square on the line between the sections", ["I.47", "II.4"],
          len2(a, d) + len2(d, b) == 2 * (len2(a, c) + len2(c, d)))
    return Out(midpoint=c, apex=apex)