Book VI · Proposition 6

VI.6

If two triangles have one angle equal to one angle and the sides about the equal angles proportional, the triangles will be equiangular and will have those angles equal which the corresponding sides subtend.Heath, 1908

Every step, checked

• neither triangle is degenerategiven
• one angle equals one anglegiven
• the sides about those angles are proportionalgiven
• the triangles are equiangularby VI.4, I.4
• and so similar throughoutby VI.4

What it needs, and what needs it

Needs: I.4 I.23 VI.4

Used by: VI.20

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

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×2)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×2)continuity

The proposition as code

@proposition(
    "VI.6",
    THEOREM,
    sample=_similar_triangles,
)
def prop_VI_6(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("neither triangle is degenerate",
               not collinear(a, b, c) and not collinear(d, e, f))
    hypothesis("one angle equals one angle", eq_angle(b, a, c, e, d, f))
    hypothesis("the sides about those angles are proportional",
               len2(a, b) * len2(d, f) == len2(d, e) * len2(a, c))
    outline(a, b, c)
    outline(d, e, f)

    because(prop_VI_4, a, b, c, d, e, f)
    # Euclid raises at D an angle equal to A and cuts off DG, DH equal to AB,
    # AC; the triangle so made has two sides and the included angle of ABC, and
    # I.4 is what makes it congruent to it.
    _built = _carried_over(a, b, c, d, e, beside=f)
    because(prop_I_4, a, b, c, _built[0], _built[1], _built[2])

    claim("the triangles are equiangular", ["VI.4", "I.4"],
          eq_angle(a, b, c, d, e, f) and eq_angle(a, c, b, d, f, e))
    claim("and so similar throughout", "VI.4", similar((a, b, c), (d, e, f)))
    return Out()