Book I · Proposition 7

I.7

Given two straight lines constructed on a straight line (from its extremities) and meeting in a point, there cannot be constructed on the same straight line (from its extremities), and on the same side of it, two other straight lines meeting in another point and equal to the former two respectively, namely each to that which has the same extremity with it.Heath, 1908

The uniqueness of the apex. Stated here as: equal legs on the same side force the same point.

Every step, checked

• AC = ADgiven
• BC = BDgiven
• C and D lie on the same side of AB, or on itgiven
• if C and D were distinct, I.5 would give an angle both greater and less than another; so C and D coincideby I.5

What it needs, and what needs it

Needs: I.5

Used by: I.8

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

Depth: 4 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 circle (×6)continuity

The proposition as code

@proposition(
    "I.7",
    THEOREM,
    sample=_apex_pair,
    note="The uniqueness of the apex. Stated here as: equal legs on the same side force "
    "the same point.",
)
def prop_I_7(a: Point, b: Point, c: Point, d: Point) -> Out:
    hypothesis("AC = AD", eq_len(a, c, a, d))
    hypothesis("BC = BD", eq_len(b, c, b, d))
    hypothesis("C and D lie on the same side of AB, or on it",
               not (Line.through(a, b).side_of(c) * Line.through(a, b).side_of(d) < 0))
    outline(a, c, b)
    outline(a, d, b)

    # The only other point answering to AC = AD and BC = BD is the reflection of
    # C in AB, and it is drawable. ACD' is isosceles on it, so I.5 gives the
    # equal angles Euclid's reductio turns against itself.
    mirror = _reflect(c, a, b)
    if mirror != c:
        line(c, mirror, "join CD")
        because(prop_I_5, a, c, mirror)

    claim("if C and D were distinct, I.5 would give an angle both greater and less than "
          "another; so C and D coincide", "I.5", c == d)
    return Out()