let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & angle (B,A,C) = PI / 2 implies ( tan (angle (A,C,B)) = |.(A - B).| / |.(A - C).| & tan (angle (C,B,A)) = |.(A - C).| / |.(A - B).| ) )
assume that
A1: A,B,C is_a_triangle and
A2: angle (B,A,C) = PI / 2 ; :: thesis: ( tan (angle (A,C,B)) = |.(A - B).| / |.(A - C).| & tan (angle (C,B,A)) = |.(A - C).| / |.(A - B).| )
A3: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
( |.(C - B).| * (sin (angle (A,C,B))) = |.(A - B).| & |.(C - B).| * (cos (angle (A,C,B))) = |.(A - C).| ) by A1, A2, Thm21;
then ((|.(C - B).| / |.(C - B).|) * (sin (angle (A,C,B)))) / (cos (angle (A,C,B))) = |.(A - B).| / |.(A - C).| by XCMPLX_1:83;
then A4: (1 * (sin (angle (A,C,B)))) / (cos (angle (A,C,B))) = |.(A - B).| / |.(A - C).| by A3, EUCLID_6:42, XCMPLX_1:60;
hence tan (angle (A,C,B)) = |.(A - B).| / |.(A - C).| by SIN_COS4:def 1; :: thesis: tan (angle (C,B,A)) = |.(A - C).| / |.(A - B).|
((angle (B,A,C)) + (angle (A,C,B))) + (angle (C,B,A)) = PI by A2, A3, COMPTRIG:5, EUCLID_3:47;
then tan (angle (C,B,A)) = (sin ((PI / 2) - (angle (A,C,B)))) / (cos ((PI / 2) - (angle (A,C,B)))) by A2, SIN_COS4:def 1
.= (cos (angle (A,C,B))) / (cos ((PI / 2) - (angle (A,C,B)))) by SIN_COS:79
.= (cos (angle (A,C,B))) / (sin (angle (A,C,B))) by SIN_COS:79
.= 1 / ((sin (angle (A,C,B))) / (cos (angle (A,C,B)))) by XCMPLX_1:57
.= |.(A - C).| / |.(A - B).| by A4, XCMPLX_1:57 ;
hence tan (angle (C,B,A)) = |.(A - C).| / |.(A - B).| ; :: thesis: verum