Book IV · Proposition 13

IV.13

In a given pentagon, which is equilateral and equiangular, to inscribe a circle.Heath, 1908

Every regular polygon has an inscribed circle for the same reason: the centre is as far from every side as from every other.

Every step, checked

• the circle has positive radiusgiven
• the centre is equally distant from every sideby I.4
• and meets each at right anglesby I.12
• so the circle touches all five sidesby III.16

What it needs, and what needs it

Needs: I.4 I.10 I.12 III.16 IV.11

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 (×35)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×39)continuity

The proposition as code

@proposition(
    "IV.13",
    CONSTRUCTION,
    sample=samples.segment,
    note="Every regular polygon has an inscribed circle for the same reason: the "
    "centre is as far from every side as from every other.",
)
def prop_IV_13(o: Point, a: Point) -> Out:
    """The pentagon is the one IV.11 inscribes; inscribe a circle in it."""
    hypothesis("the circle has positive radius", o != a)
    vertices = prop_IV_11(o, a).pentagon
    outline(*vertices)

    feet = [posit(prop_I_10(vertices[i], vertices[(i + 1) % 5]).midpoint, "FGHKL"[i])
            for i in range(5)]
    for foot in feet:
        line(o, foot)
    inscribed = circle(o, feet[0], "the inscribed circle")

    because(prop_I_4, o, feet[0], vertices[0], o, feet[1], vertices[1])
    because(prop_I_12, vertices[0], vertices[1], o)
    because(prop_III_16, o, feet[0])

    claim("the centre is equally distant from every side", "I.4",
          all(eq_len(o, foot, o, feet[0]) for foot in feet))
    claim("and meets each at right angles", "I.12",
          all(right_angle(o, feet[i], vertices[i]) for i in range(5)))
    claim("so the circle touches all five sides", "III.16",
          all(on_circle(foot, inscribed) for foot in feet))
    return Out(centre=o, circle=inscribed, pentagon=vertices)