Book XIII · Proposition 10

XIII.10

If an equilateral pentagon be inscribed in a circle, the square on the side of the pentagon is equal to the squares on the side of the hexagon and on that of the decagon inscribed in the same circle.Heath, 1908

The three inscribed figures in one relation, and the one XIII.16 will need to put the icosahedron in its sphere.

Every step, checked

• the circle has positive radiusgiven
• K bisects the arc, so AK is the side of the decagonby III.30
• the square on the side of the pentagon equals the squares on the sides of the hexagon and of the decagonby I.47, IV.15

What it needs, and what needs it

Needs: I.47 III.30 IV.11 IV.15

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

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

The proposition as code

@proposition(
    "XIII.10",
    THEOREM,
    sample=samples.segment,
    note="The three inscribed figures in one relation, and the one XIII.16 will "
    "need to put the icosahedron in its sphere.",
)
def prop_XIII_10(o: Point, a: Point) -> Out:
    hypothesis("the circle has positive radius", o != a)
    around = circle(o, a, "the given circle")
    corners = prop_IV_11(o, a).pentagon
    tenth = posit(_arc_midpoint(o, corners[0], corners[1], around), "K")
    result(tenth)

    pentagon = len2(corners[0], corners[1])
    hexagon = len2(o, a)  # IV.15: the side of the hexagon is the radius
    decagon = len2(corners[0], tenth)
    because(prop_III_30, o, corners[0], corners[1])
    because(prop_IV_15, o, a)
    # The perpendicular from the centre to the pentagon side makes the right
    # angle I.47 speaks of.
    because(prop_I_47, o, midpoint_of(corners[0], corners[1]), corners[0])

    claim("K bisects the arc, so AK is the side of the decagon", "III.30",
          on_circle(tenth, around) and eq_len(tenth, corners[0], tenth, corners[1]))
    claim("the square on the side of the pentagon equals the squares on the "
          "sides of the hexagon and of the decagon", ["I.47", "IV.15"],
          pentagon == hexagon + decagon)
    return Out(pentagon=pentagon, hexagon=hexagon, decagon=decagon)