Book IV · Proposition 5

IV.5

About a given triangle to circumscribe a circle.Heath, 1908

The circumcircle. Its centre is where the perpendicular bisectors cross, and stays rational when the vertices are.

Every step, checked

• ABC is a genuine trianglegiven
• the centre is equidistant from all three verticesby I.10, I.11
• so the circle through A passes through B and C tooby Def.15

What it needs, and what needs it

Needs: I.10 I.11

Rests on: C.N.1, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.4

Depth: 8 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×10)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×12)continuity

The proposition as code

@proposition(
    "IV.5",
    CONSTRUCTION,
    sample=samples.triangle,
    note="The circumcircle. Its centre is where the perpendicular bisectors "
    "cross, and stays rational when the vertices are.",
)
def prop_IV_5(a: Point, b: Point, c: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    outline(a, b, c)

    centre = posit(_centre_of(a, b, c), "O")
    around = circle(centre, a, "the circumscribed circle")
    line(centre, a, "a radius")
    line(centre, b, "a radius")
    line(centre, c, "a radius")

    because(prop_I_10, a, b)
    because(prop_I_11, a, b, prop_I_10(a, b).midpoint)

    claim("the centre is equidistant from all three vertices", ["I.10", "I.11"],
          eq_len(centre, a, centre, b) and eq_len(centre, a, centre, c))
    claim("so the circle through A passes through B and C too", "Def.15",
          on_circle(b, around) and on_circle(c, around))
    return Out(centre=centre, circle=around)