let A, B, C be Point of (TOP-REAL 2); ( A,C,B is_a_triangle & angle (A,C,B) < PI & |((A - C),(A - B))| <> 0 implies the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).| )
assume that
A1:
A,C,B is_a_triangle
and
A2:
angle (A,C,B) < PI
and
A3:
|((A - C),(A - B))| <> 0
; the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).|
A4:
|.(A - C).| = (|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))
by A1, A2, Th64;
A5:
( C,A,B is_a_triangle & A,C,B are_mutually_distinct )
by A1, EUCLID_6:20, MENELAUS:15;
then
( |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(C - A).| * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B))))) or |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(C - A).| * (- (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))) )
by A3, Th45, Th67;
then
( |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(A - C).| * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B))))) or |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(A - C).| * (- (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))) )
by EUCLID_6:43;
per cases then
( |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(A - B).| * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))) or |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(A - B).| * (- (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B))))))) )
by A4;
suppose A7:
|.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(A - B).| * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B))))))
;
the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).|
|.(A - B).| <> 0
by A5, EUCLID_6:42;
then A8:
0 <= ((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))
by A7;
the_length_of_the_altitude (
C,
A,
B) =
|.(C - (the_foot_of_the_altitude (C,A,B))).|
by A5, Def3
.=
|.((the_foot_of_the_altitude (C,A,B)) - C).|
by EUCLID_6:43
.=
|.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).|
by A7, A8, ABSVALUE:def 1
;
hence
the_length_of_the_altitude (
C,
A,
B)
= |.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).|
;
verum end; suppose A10:
|.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(A - B).| * (- (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))))
;
the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).|
|.(A - B).| <> 0
by A5, EUCLID_6:42;
then A11:
((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B))))) <= 0
by A10;
the_length_of_the_altitude (
C,
A,
B) =
|.(C - (the_foot_of_the_altitude (C,A,B))).|
by A5, Def3
.=
|.((the_foot_of_the_altitude (C,A,B)) - C).|
by EUCLID_6:43
.=
|.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).|
by A10, A11, ABSVALUE:30
;
hence
the_length_of_the_altitude (
C,
A,
B)
= |.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).|
;
verum end; end;