let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle & angle (C,A,B) = (3 / 2) * PI implies the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (C,B,A))) )
assume that
A1:
A,B,C is_a_triangle
and
A2:
angle (C,A,B) = (3 / 2) * PI
; the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (C,B,A)))
A3:
A,B,C are_mutually_distinct
by A1, EUCLID_6:20;
then
|((C - A),(B - A))| = 0
by A2, EUCLID_3:45;
then A4:
|((A - B),(A - C))| = 0
by Th10;
angle (B,A,C) =
(2 * PI) - ((3 / 2) * PI)
by A1, A2, EUCLID10:31
.=
PI / 2
;
then (tan (angle (C,B,A))) * |.(A - B).| =
(|.(A - C).| / |.(A - B).|) * |.(A - B).|
by A1, EUCLID10:35
.=
|.(A - C).|
by A3, EUCLID_6:42, XCMPLX_1:87
.=
|.(C - A).|
by EUCLID_6:43
;
then |.(A - B).| * (tan (angle (C,B,A))) =
|.((the_foot_of_the_altitude (C,A,B)) - C).|
by A4, A3, Th47
.=
|.(C - (the_foot_of_the_altitude (C,A,B))).|
by EUCLID_6:43
;
hence
the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (C,B,A)))
by A3, Def3; verum