Book III · Proposition 22

III.22

The opposite angles of quadrilaterals in circles are equal to two right angles.Heath, 1908

The cyclic quadrilateral. Its opposite angles sum to two right angles, which is what makes 'concyclic' testable without finding the centre.

Every step, checked

• the four points lie on the circlegiven
• they are taken in order round itgiven
• the opposite angles are together equal to two right anglesby III.21
• and so are the other pairby III.21

What it needs, and what needs it

Needs: III.21

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

Depth: 14 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.22",
    THEOREM,
    sample=_four_on_a_circle,
    note="The cyclic quadrilateral. Its opposite angles sum to two right angles, "
    "which is what makes 'concyclic' testable without finding the centre.",
)
def prop_III_22(o: Point, a: Point, b: Point, c: Point, d: Point) -> Out:
    """ABCD is inscribed in order round the circle."""
    hypothesis("the four points lie on the circle",
               all(eq_len(o, p, o, a) for p in (b, c, d)))
    hypothesis("they are taken in order round it",
               not collinear(a, b, c) and not collinear(b, c, d))
    circle(o, a, "the given circle")
    outline(a, b, c, d)
    line(a, c, "the diagonal AC")
    line(b, d, "the diagonal BD")

    because(prop_III_21, o, a, b, c, d)

    claim("the opposite angles are together equal to two right angles", "III.21",
          angle_at(d, a, b) + angle_at(b, c, d) == STRAIGHT)
    claim("and so are the other pair", "III.21",
          angle_at(a, b, c) + angle_at(c, d, a) == STRAIGHT)
    return Out()