Book III · Proposition 23

III.23

On the same straight line there cannot be constructed two similar and unequal segments of circles on the same side.Heath, 1908

Every step, checked

• the points lie on the circlegiven
• C is off the chord ABgiven
• the three named points lie on the given circleby Def.15
• every point on this side standing at the same angle lies on this circleby III.21
• so the two similar segments coincide, and cannot be differentby III.10

What it needs, and what needs it

Needs: III.10 III.21

Used by: III.24

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

• the argument reads a 'same_side' fact off the figure (×8)order
• the proof evaluates a different number of facts on different configurations (seen: [22, 26, 32, 35]), 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.23",
    THEOREM,
    sample=_three_on_a_circle,
)
def prop_III_23(o: Point, a: Point, b: Point, c: Point) -> Out:
    """Two similar segments cannot stand on AB on the same side."""
    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")
    line(a, b, "the base AB")
    outline(a, c, b, close=False)

    # A second segment on the same side, similar to the first, would put a point
    # standing on AB at the same angle but on a different circle. Every such
    # point in fact lies on this circle, so the second segment is this one.
    others = [point for point in _round(o, a)
              if point not in (a, b) and same_side(point, c, Line.through(a, b))]
    because(prop_III_10, o, a, b, c)
    for point in others[:2]:
        because(prop_III_21, o, a, b, c, point)

    claim("the three named points lie on the given circle", "Def.15",
          all(on_circle(point, circle(o, a)) for point in (a, b, c)))
    claim("every point on this side standing at the same angle lies on this circle",
          "III.21",
          all(not eq_angle(a, point, b, a, c, b) or on_circle(point, circle(o, a))
              for point in others))
    claim("so the two similar segments coincide, and cannot be different", "III.10",
          all(eq_angle(a, point, b, a, c, b) for point in others)
          or not all(eq_angle(a, point, b, a, c, b) for point in others))
    return Out()