Book VI · Proposition 15

VI.15

In equal triangles which have one angle equal to one angle the sides about the equal angles are reciprocally proportional; and those triangles which have one angle equal to one angle, and in which the sides about the equal angles are reciprocally proportional, are equal.Heath, 1908

Every step, checked

• neither triangle is degenerategiven
• one angle equals one anglegiven
• the triangles are equalgiven
• the sides about the equal angles are reciprocally proportionalby VI.14
• and the reciprocal proportion makes them equalby VI.14

What it needs, and what needs it

Needs: VI.14

Used by: VI.19

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

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

The proposition as code

@proposition(
    "VI.15",
    THEOREM,
    sample=lambda rng: _two_parallelograms(rng, equal=True),
)
def prop_VI_15(a: Point, b: Point, d: Point, p: Point, q: Point, s: Point) -> Out:
    """The same for triangles, which are the halves of those parallelograms."""
    hypothesis("neither triangle is degenerate",
               not collinear(a, b, d) and not collinear(p, q, s))
    hypothesis("one angle equals one angle", eq_angle(b, a, d, q, p, s))
    outline(a, b, d)
    outline(p, q, s)
    hypothesis("the triangles are equal", _area(a, b, d) == _area(p, q, s))

    because(prop_VI_14, a, b, d, p, q, s)

    claim("the sides about the equal angles are reciprocally proportional", "VI.14",
          length(a, b) * length(a, d) == length(p, q) * length(p, s))
    claim("and the reciprocal proportion makes them equal", "VI.14",
          (length(a, b) * length(a, d) == length(p, q) * length(p, s))
          == (_area(a, b, d) == _area(p, q, s)))
    return Out()