Book I · Proposition 6

I.6

If in a triangle two angles be equal to one another, the sides which subtend the equal angles will also be equal to one another.Heath, 1908

Converse of I.5, proved by Euclid's first reductio.

Every step, checked

• angle ABC = angle ACBgiven
• were AB unequal to AC, the greater could be cut down to the less (I.3) and I.4 would make a part equal the whole, which is absurd; so AB = ACby I.3, I.4, C.N.5

What it needs, and what needs it

Needs: I.3 I.4

Used by: IV.9 IV.14

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

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

What it takes on trust

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

The proposition as code

@proposition(
    "I.6",
    THEOREM,
    sample=samples.isosceles,
    note="Converse of I.5, proved by Euclid's first reductio.",
)
def prop_I_6(a: Point, b: Point, c: Point) -> Out:
    hypothesis("angle ABC = angle ACB", eq_angle(a, b, c, a, c, b))
    outline(a, b, c)

    # D is set on BA at the distance AC, which is the point Euclid's reductio
    # cuts off, and I.4 then compares DBC with ACB. The cutting itself is done
    # under the supposition AB > AC, and I.3 will not take two equal lines, so
    # that citation cannot be run on a figure meeting this hypothesis.
    reach = circle_with_radius2(b, len2(a, c), "circle centre B with radius AC")
    d = posit(meet(line(b, a), reach)[1], "D")
    line(d, c, "join DC")
    because(prop_I_4, b, d, c, c, a, b)

    claim("were AB unequal to AC, the greater could be cut down to the less (I.3) and "
          "I.4 would make a part equal the whole, which is absurd; so AB = AC",
          ["I.3", "I.4", "C.N.5"], eq_len(a, b, a, c))
    return Out()