Book IV · Proposition 2

IV.2

In a given circle to inscribe a triangle equiangular with a given triangle.Heath, 1908

An angle at the circumference stands on twice its own arc (III.20), so laying off twice each given angle round the centre settles the triangle.

Every step, checked

• the circle has positive radiusgiven
• DEF is a genuine trianglegiven
• all three vertices lie on the given circleby Def.15
• the angle at each vertex is half the arc it stands onby III.20
• so the inscribed triangle is equiangular with the given oneby III.20

What it needs, and what needs it

Needs: III.20

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

Depth: 13 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.2",
    CONSTRUCTION,
    sample=lambda rng: samples.segment(rng) + samples.triangle(rng),
    note="An angle at the circumference stands on twice its own arc (III.20), so "
    "laying off twice each given angle round the centre settles the triangle.",
)
def prop_IV_2(o: Point, a: Point, d: Point, e: Point, f: Point) -> Out:
    """Inscribe in the circle about O 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)

    # An angle stands on the arc it does *not* touch, so the arc AB is twice the
    # angle at F, and the arc BC twice the angle at D. Laying those two off
    # leaves the third arc, and with it the third angle, no longer free.
    at_d, at_f = angle_at(f, d, e), angle_at(e, f, d)
    b = posit(_turn(o, a, at_f.doubled()), "B")
    c = posit(_turn(o, b, at_d.doubled()), "C")
    outline(a, b, c)

    if not collinear(a, b, c):
        because(prop_III_20, o, b, a, c)

    claim("all three vertices lie on the given circle", "Def.15",
          on_circle(b, around) and on_circle(c, around))
    claim("the angle at each vertex is half the arc it stands on", "III.20",
          angle_at(b, a, c).doubled() == angle_at(b, o, c)
          or angle_at(b, a, c).doubled() == STRAIGHT + STRAIGHT - angle_at(b, o, c))
    claim("so the inscribed triangle is equiangular with the given one", "III.20",
          eq_angle(b, a, c, f, d, e) and eq_angle(a, b, c, d, e, f))
    return Out(triangle=(a, b, c))