Book III · Proposition 32

III.32

If a straight line touch a circle, and from the point of contact there be drawn across, in the circle, a straight line cutting the circle, the angles which it makes with the tangent will be equal to the angles in the alternate segments of the circle.Heath, 1908

The tangent-chord angle. It is the limiting case of III.21, and the step IV.3 leans on to circumscribe a triangle.

Every step, checked

• the points lie on the circlegiven
• ABC is a genuine trianglegiven
• the tangent meets the radius at right anglesby III.18
• the angle between tangent and chord equals the angle in the alternate segmentby III.21

What it needs, and what needs it

Needs: III.18 III.21

Used by: IV.3 IV.10

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

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

What it takes on trust

• the argument reads a 'same_side' fact off the figure (×9)order
• the proof evaluates a different number of facts on different configurations (seen: [13, 14]), so it is following more than one route through the diagramcase
• the 'same_side' fact (occurrence 1) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 2) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 3) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 4) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 5) is true in some configurations and false in otherscase

The proposition as code

@proposition(
    "III.32",
    THEOREM,
    sample=_three_on_a_circle,
    note="The tangent-chord angle. It is the limiting case of III.21, and the "
    "step IV.3 leans on to circumscribe a triangle.",
)
def prop_III_32(o: Point, a: Point, b: Point, c: Point) -> Out:
    """The tangent at A, and the chord AB, with C in the alternate segment."""
    hypothesis("the points lie on the circle",
               eq_len(o, a, o, b) and eq_len(o, a, o, c))
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    circle(o, a, "the given circle")
    outline(a, b, c)
    _tangent_at(o, a, "the tangent at A")

    across = _across(o, a)
    reach = length(o, a)
    ends = [
        posit(Point(a.x + across[0], a.y + across[1]), "T"),
        posit(Point(a.x - across[0], a.y - across[1]), "S"),
    ]
    # The chord AB divides the tangent's two directions between the two
    # segments; the one on the far side from C answers the alternate segment.
    alternate = ends[0] if not same_side(ends[0], c, Line.through(a, b)) else ends[1]

    # The angle in the alternate segment wants a second point of that segment
    # for III.21 to compare C with.
    alongside = [point for point in _round(o, a)
                 if point not in (a, b, c) and same_side(point, c, Line.through(a, b))]
    because(prop_III_18, o, a, reach)
    if alongside:
        because(prop_III_21, o, a, b, c, alongside[0])

    claim("the tangent meets the radius at right angles", "III.18",
          right_angle(o, a, ends[0]) and sign(reach) > 0)
    claim("the angle between tangent and chord equals the angle in the alternate "
          "segment", "III.21", eq_angle(alternate, a, b, a, c, b))
    return Out(tangent_angle=angle_at(alternate, a, b))