Book III · Proposition 18

III.18

If a straight line touch a circle, and a straight line be joined from the centre to the point of contact, the straight line so joined will be perpendicular to the tangent.Heath, 1908

Every step, checked

• the circle has positive radiusgiven
• a point of the tangent is takengiven
• the radius to the point of contact is perpendicular to the tangentby I.19
• and the radius is the shortest line from the centre to the tangentby I.19

What it needs, and what needs it

Needs: I.19

Used by: III.19 III.32 III.36 III.37

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

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

What it takes on trust

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

The proposition as code

@proposition(
    "III.18",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 1) + (samples.nonzero(rng, 1, 4),),
)
def prop_III_18(o: Point, a: Point, reach) -> Out:
    """The tangent at A, and the radius drawn to A."""
    hypothesis("the circle has positive radius", o != a)
    hypothesis("a point of the tangent is taken", sign(reach) > 0, guard=True)
    circle(o, a, "the given circle")
    tangent = _tangent_at(o, a, "the tangent at A")
    across = _across(o, a)
    on_tangent = posit(Point(a.x + reach * across[0], a.y + reach * across[1]), "C")
    line(o, a, "the radius OA")

    # OAC is right-angled at A, so I.19 turns its angles into its sides.
    because(prop_I_19, o, a, on_tangent)

    claim("the radius to the point of contact is perpendicular to the tangent",
          "I.19", right_angle(o, a, on_tangent))
    claim("and the radius is the shortest line from the centre to the tangent", "I.19",
          sign(length(o, on_tangent) - length(o, a)) > 0)
    return Out(tangent=tangent)