Book III · Proposition 24

III.24

Similar segments of circles on equal straight lines are equal to one another.Heath, 1908

Every step, checked

• the points lie on the circlegiven
• C is off the chord ABgiven
• the segment stands on the given circleby Def.15
• the bases are equal, the second being the first movedby I.4
• the segments admit equal anglesby III.21
• so similar segments on equal straight lines are equalby III.23

What it needs, and what needs it

Needs: I.4 III.21 III.23

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

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

What it takes on trust

• the argument reads a 'same_side' fact off the figure (×8)order
• the proof evaluates a different number of facts on different configurations (seen: [17, 18]), so it is following more than one route through the diagramcase
• the 'same_side' fact (occurrence 1) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 2) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 3) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 4) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 5) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 6) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 7) is true in some configurations and false in otherscase
• the 'same_side' fact (occurrence 8) is true in some configurations and false in otherscase

The proposition as code

@proposition(
    "III.24",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 3)
    + (samples.isometry(rng),),
)
def prop_III_24(o: Point, a: Point, b: Point, c: Point, move) -> Out:
    """A segment on AB, and its image on an equal straight line."""
    hypothesis("the points lie on the circle",
               eq_len(o, a, o, b) and eq_len(o, a, o, c))
    hypothesis("C is off the chord AB", not collinear(a, b, c))
    circle(o, a, "the given circle")
    outline(a, c, b, close=False)
    line(a, b, "the base AB")

    d, e, f = posit(move(a), "D"), posit(move(b), "E"), posit(move(c), "F")
    outline(d, f, e, close=False)
    line(d, e, "the equal base DE")

    # III.21 wants two points in the one segment, so a second is taken from the
    # arc on C's side; III.23 then says the two segments cannot differ.
    alongside = [point for point in _round(o, a)
                 if point not in (a, b, c) and same_side(point, c, Line.through(a, b))]
    because(prop_I_4, c, a, b, f, d, e)
    if alongside:
        because(prop_III_21, o, a, b, c, alongside[0])
    because(prop_III_23, o, a, b, c)

    claim("the segment stands on the given circle", "Def.15",
          all(on_circle(point, circle(o, a)) for point in (a, b, c)))
    claim("the bases are equal, the second being the first moved", "I.4",
          eq_len(a, b, d, e))
    claim("the segments admit equal angles", "III.21", eq_angle(a, c, b, d, f, e))
    claim("so similar segments on equal straight lines are equal", "III.23",
          eq_len(a, c, d, f) and eq_len(b, c, e, f))
    return Out()