Book III · Proposition 19

III.19

If a straight line touch a circle, and from the point of contact a straight line be drawn at right angles to the tangent, the centre of the circle will be on the straight line so drawn.Heath, 1908

Every step, checked

• the circle has positive radiusgiven
• a point of the tangent is takengiven
• the perpendicular raised at the point of contact passes through the centreby III.18

What it needs, and what needs it

Needs: III.18

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

Depth: 12 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.19",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 1) + (samples.nonzero(rng, 1, 4),),
)
def prop_III_19(o: Point, a: Point, reach) -> Out:
    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_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")
    upright = line(a, Point(a.x + (o.x - a.x), a.y + (o.y - a.y)), "the perpendicular at A")

    because(prop_III_18, o, a, reach)

    claim("the perpendicular raised at the point of contact passes through the centre",
          "III.18", on_line(o, upright) and right_angle(o, a, on_tangent))
    return Out()