Book III · Proposition 12

III.12

If two circles touch one another externally, the straight line joining their centres will pass through the point of contact.Heath, 1908

Every step, checked

• the circles have positive radiigiven
• they touch at Agiven
• the point of contact lies on the line joining the centresby I.20
• and the distance between the centres is the sum of the radiiby C.N.2

What it needs, and what needs it

Needs: I.20

Rests on: C.N.1, C.N.2, 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.12",
    THEOREM,
    sample=lambda rng: _touching_circles(rng, internally=False),
)
def prop_III_12(o: Point, a: Point, p: Point) -> Out:
    hypothesis("the circles have positive radii", o != a and o != p)
    first = circle(o, a, "the first circle")
    second = circle(p, a, "the second, touching it without")
    hypothesis("they touch at A", on_circle(a, first) and on_circle(a, second))
    joined = line(o, p, "the line joining the centres")

    # The centres and the point of contact make no triangle when they are in
    # one straight line, which is exactly what this proposition proves.
    if not collinear(o, p, a):
        because(prop_I_20, o, p, a)

    claim("the point of contact lies on the line joining the centres", "I.20",
          on_line(a, joined))
    claim("and the distance between the centres is the sum of the radii", "C.N.2",
          length(o, p) == length(o, a) + length(p, a))
    return Out(contact=a)