Book XIII · Proposition 3

XIII.3

If a straight line be cut in extreme and mean ratio, the square on the lesser segment added to the half of the greater segment is five times the square on the half of the greater segment.Heath, 1908

XIII.1 read of the greater segment instead of the whole.

Every step, checked

• A and B are distinctgiven
• D bisects the greater segment ACby I.10
• the square on DB is five times the square on DCby II.6

What it needs, and what needs it

Needs: I.10 II.6 VI.30

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.22, Def.3, Def.4, Post.1, Post.5, V.Def.5

Depth: 19 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 (×15)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×22)continuity

The proposition as code

@proposition(
    "XIII.3",
    THEOREM,
    sample=samples.segment,
    note="XIII.1 read of the greater segment instead of the whole.",
)
def prop_XIII_3(a: Point, b: Point) -> Out:
    hypothesis("A and B are distinct", a != b)
    section = prop_VI_30(a, b).section
    half = prop_I_10(a, section).midpoint
    result(half)

    because(prop_II_6, a, half, section)

    claim("D bisects the greater segment AC", "I.10",
          4 * len2(a, half) == len2(a, section))
    claim("the square on DB is five times the square on DC", "II.6",
          len2(half, b) == 5 * len2(half, section))
    return Out(section=section, half=half)