Book IV · Proposition 3

IV.3

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

The dual of IV.2. A tangent meets its radius at right angles, so the angle at a vertex and the arc between its two contact points make two right angles between them.

Every step, checked

• the circle has positive radiusgiven
• DEF is a genuine trianglegiven
• each side touches the circle, meeting a radius at right anglesby III.16
• so the circumscribed triangle is equiangular with the given oneby III.32

What it needs, and what needs it

Needs: III.16 III.32

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

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

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "IV.3",
    CONSTRUCTION,
    sample=lambda rng: samples.segment(rng) + samples.triangle(rng),
    note="The dual of IV.2. A tangent meets its radius at right angles, so the "
    "angle at a vertex and the arc between its two contact points make two right "
    "angles between them.",
)
def prop_IV_3(o: Point, a: Point, d: Point, e: Point, f: Point) -> Out:
    """Circumscribe about the circle a triangle equiangular with DEF."""
    hypothesis("the circle has positive radius", o != a)
    hypothesis("DEF is a genuine triangle", not collinear(d, e, f), guard=True)
    around = circle(o, a, "the given circle")
    outline(d, e, f)

    at_d, at_e = angle_at(f, d, e), angle_at(d, e, f)
    # The arc between two contact points is the supplement of the angle between
    # the tangents there, so lay the contact points off by those supplements.
    touch_b = posit(_turn(o, a, STRAIGHT - at_d), "P")
    touch_c = posit(_turn(o, touch_b, STRAIGHT - at_e), "Q")
    touches = (a, touch_b, touch_c)
    tangents = [_tangent_at(o, point, f"the tangent at {point.label}") for point in touches]
    for point in touches:
        line(o, point, "a radius")

    corners = [
        posit(meet_one(tangents[index], tangents[(index + 1) % 3]), "GHK"[index])
        for index in range(3)
    ]
    outline(*corners)

    for touch in touches:
        because(prop_III_16, o, touch)
    # The angle between a tangent and the chord equals the angle in the
    # alternate segment, which is what carries the given angles round to the
    # circumscribed triangle.
    for index in range(3):
        because(prop_III_32, o, touches[index], touches[(index + 1) % 3],
                touches[(index + 2) % 3])

    claim("each side touches the circle, meeting a radius at right angles", "III.16",
          all(on_circle(point, around) for point in touches)
          and all(right_angle(o, touches[i], corners[i]) for i in range(3)))
    claim("so the circumscribed triangle is equiangular with the given one", "III.32",
          eq_angle(corners[2], corners[0], corners[1], f, d, e)
          and eq_angle(corners[0], corners[1], corners[2], d, e, f))
    return Out(triangle=tuple(corners), touching=touches)