Book III · Proposition 17

III.17

From a given point to draw a straight line touching a given circle.Heath, 1908

Every step, checked

• the circle has positive radiusgiven
• the point is outsidegiven
• OD and OT are radii of the given circle, OE and OP of the wider oneby Def.15
• so the triangles ODE and OTP have two sides and the angle between them equalby I.4
• the angle at D being right, the angle at the point of contact is right tooby I.4
• so PT touches the circle and does not cut itby III.16

What it needs, and what needs it

Needs: I.4 III.16

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

• a line-circle intersection is used, though no postulate asserts that a line meets a circlecontinuity

The proposition as code

@proposition(
    "III.17",
    CONSTRUCTION,
    sample=lambda rng: samples.points_round_a_circle(rng, 1)
    + (1 + Fraction(rng.randint(2, 8), 4),),
)
def prop_III_17(o: Point, a: Point, beyond) -> Out:
    """From a point outside the circle, draw a line touching it."""
    hypothesis("the circle has positive radius", o != a)
    hypothesis("the point is outside", sign(beyond - 1) > 0)
    around = circle(o, a, "the given circle")
    outside = posit(Point(o.x + beyond * (a.x - o.x), o.y + beyond * (a.y - o.y)), "P")

    # Euclid's own construction, which needs nothing from later in the book.
    # The circle on OP as diameter would give the right angle at once, but that
    # is III.31 and comes after; instead a second circle about O through P, a
    # perpendicular at D, and I.4 on the two triangles.
    d = posit(_along_from(o, outside, length(o, a)), "D")
    wider = circle(o, outside, "the circle about O through P")
    upright = _tangent_at(o, d, "the perpendicular to OP at D")
    e = posit(meet(upright, wider)[0], "E")
    line(o, e, "the join OE")
    touch = posit(_along_from(o, e, length(o, a)), "T")
    tangent = line(outside, touch, "the tangent PT")
    line(o, touch, "the radius to the point of contact")

    claim("OD and OT are radii of the given circle, OE and OP of the wider one",
          "Def.15",
          eq_len(o, d, o, a) and eq_len(o, touch, o, a)
          and eq_len(o, e, o, outside))
    claim("so the triangles ODE and OTP have two sides and the angle between "
          "them equal", "I.4",
          eq_angle(d, o, e, touch, o, outside) and eq_len(d, e, touch, outside))
    claim("the angle at D being right, the angle at the point of contact is right "
          "too", "I.4",
          right_angle(o, d, e) and right_angle(o, touch, outside))
    because(prop_I_4, o, d, e, o, touch, outside)
    because(prop_III_16, o, touch)

    claim("so PT touches the circle and does not cut it", "III.16",
          on_circle(touch, around)
          and not any(inside_circle(Point(touch.x + Fraction(k, 4) * (outside.x - touch.x),
                                          touch.y + Fraction(k, 4) * (outside.y - touch.y)),
                                    around) for k in range(1, 5)))
    return Out(tangent=tangent, contact=touch)