Book VI · Proposition 7

VI.7

If two triangles have one angle equal to one angle, the sides about other angles proportional, and the remaining angles either both less or both not less than a right angle, the triangles will be equiangular and will have those angles equal, the sides about which are proportional.Heath, 1908

The ambiguous case, made unambiguous by Euclid's proviso that the remaining angles are both acute or both not acute.

Every step, checked

• neither triangle is degenerategiven
• one angle equals one anglegiven
• the sides about other angles are proportionalgiven
• the remaining angles are both less, or both not less, than a right anglegiven
• the triangles are equiangularby VI.5
• and the sides about the proportional angles correspondby VI.5

What it needs, and what needs it

Needs: VI.5

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

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "VI.7",
    THEOREM,
    sample=_similar_triangles,
    note="The ambiguous case, made unambiguous by Euclid's proviso that the "
    "remaining angles are both acute or both not acute.",
)
def prop_VI_7(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(a, b, c, d, e, f))
    hypothesis("the sides about other angles are proportional",
               len2(b, a) * len2(e, f) == len2(e, d) * len2(b, c))
    remaining = (angle_at(b, c, a), angle_at(e, f, d))
    hypothesis("the remaining angles are both less, or both not less, than a right angle",
               (remaining[0] < RIGHT) == (remaining[1] < RIGHT))
    outline(a, b, c)
    outline(d, e, f)

    because(prop_VI_5, a, b, c, d, e, f) if similar((a, b, c), (d, e, f)) else None

    claim("the triangles are equiangular", "VI.5", eq_angle(b, c, a, e, f, d))
    claim("and the sides about the proportional angles correspond", "VI.5",
          similar((a, b, c), (d, e, f)))
    return Out()