Book III · Proposition 6

III.6

If two circles touch one another, they will not have the same centre.Heath, 1908

Every step, checked

• the circle has positive radiusgiven
• the second radius differs from the firstgiven
• the two radii are unequalby Def.15
• touching means one point in common, and these two share noneby Def.15

What it needs, and what needs it

Needs: nothing earlier.

Rests on: Def.15

Depth: 0 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.6",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 1) + (samples.nonzero(rng, 1, 3),),
)
def prop_III_6(o: Point, a: Point, difference) -> Out:
    hypothesis("the circle has positive radius", o != a)
    hypothesis("the second radius differs from the first", sign(difference) != 0)
    circle(o, a, "the first circle")
    outer = posit(_along_from(o, a, length(o, a) + difference), "B")
    circle(o, outer, "a second circle on the same centre")

    claim("the two radii are unequal", "Def.15", not eq_len(o, a, o, outer))
    claim("touching means one point in common, and these two share none", "Def.15",
          not any(on_circle(point, circle(o, outer)) for point in _round(o, a)))
    return Out()