Book III · Proposition 31

III.31

In a circle the angle in the semicircle is right, that in a greater segment less than a right angle, and that in a less segment greater than a right angle; and further the angle of the greater segment is greater than a right angle, and the angle of the less segment less than a right angle.Heath, 1908

Thales' theorem, which Euclid gets as a corollary of III.20.

Every step, checked

• AB is a diametergiven
• C lies on the circle, off the diametergiven
• the angle at the centre on the diameter is two right anglesby Def.17
• the angle at the circumference is half of itby III.20
• therefore the angle ACB is rightby Def.10

What it needs, and what needs it

Needs: III.20

Used by: III.35 IV.6 VI.13

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

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

What it takes on trust

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

The proposition as code

@proposition(
    "III.31",
    THEOREM,
    sample=_points_on_a_circle,
    note="Thales' theorem, which Euclid gets as a corollary of III.20.",
)
def prop_III_31(o: Point, a: Point, b: Point, c: Point) -> Out:
    hypothesis("AB is a diameter", collinear(a, o, b) and eq_len(o, a, o, b))
    hypothesis("C lies on the circle, off the diameter",
               eq_len(o, c, o, a) and not collinear(a, b, c))
    circle(o, a, "the given circle")
    line(a, b, "the diameter AB")
    line(a, c)
    line(b, c)

    because(prop_III_20, o, a, c, b)

    claim("the angle at the centre on the diameter is two right angles", "Def.17",
          angle_at(a, o, b) == STRAIGHT)
    claim("the angle at the circumference is half of it", "III.20",
          angle_at(a, c, b) == RIGHT)
    claim("therefore the angle ACB is right", "Def.10", right_angle(a, c, b))
    return Out()