Book I · Proposition 23

I.23

On a given straight line and at a point on it to construct a rectilineal angle equal to a given rectilineal angle.Heath, 1908

Every step, checked

• ABC is a genuine anglegiven
• P and Q are distinctgiven
• the triangle on PQ has sides equal to BA, AC and CBby I.22
• therefore the angle at P equals the given angle ABCby I.8

What it needs, and what needs it

Needs: I.8 I.22

Used by: I.24 I.31 I.42 I.44 VI.4 VI.6

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

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meetcontinuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circlecontinuity

The proposition as code

@proposition(
    "I.23",
    CONSTRUCTION,
    sample=_angle_and_ray,
)
def prop_I_23(
    a: Point,
    b: Point,
    c: Point,
    p: Point,
    q: Point,
    beside: "Point | None" = None,
    apart_from: "Point | None" = None,
) -> Out:
    hypothesis("ABC is a genuine angle", not collinear(a, b, c), guard=True)
    hypothesis("P and Q are distinct", p != q)

    outline(a, b, c, close=False)  # the arms of the given angle
    line(a, c, "join AC")
    built = prop_I_22(b, a, c, p, q, beside=beside, apart_from=apart_from)
    _, foot, apex = built.triangle
    line(p, apex, "the new side")

    claim("the triangle on PQ has sides equal to BA, AC and CB", "I.22",
          congruent_sss((p, foot, apex), (b, a, c)))
    because(prop_I_8, p, foot, apex, b, a, c)
    claim("therefore the angle at P equals the given angle ABC", "I.8",
          eq_angle(foot, p, apex, a, b, c))
    return Out(vertex=p, ray_through=apex)