let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,C,B is_a_triangle & angle (A,C,B) < PI implies tan (((angle (B,A,C)) - (angle (C,B,A))) / 2) = (cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)) )
assume that
A1: A,C,B is_a_triangle and
A2: angle (A,C,B) < PI ; :: thesis: tan (((angle (B,A,C)) - (angle (C,B,A))) / 2) = (cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|))
A3: A,C,B are_mutually_distinct by A1, EUCLID_6:20;
A4: A,B,C is_a_triangle by A1, MENELAUS:15;
then A5: ( (angle (B,A,C)) - (angle (C,B,A)) <> PI & (angle (B,A,C)) - (angle (C,B,A)) <> - PI ) by Th25, Th26;
set alpha = ((angle (B,A,C)) - (angle (C,B,A))) / 2;
set beta = ((angle (B,A,C)) + (angle (C,B,A))) / 2;
angle (A,C,B) = PI - ((angle (C,B,A)) + (angle (B,A,C))) by A1, A2, Th23;
then A8: ((angle (B,A,C)) + (angle (C,B,A))) / 2 = (PI / 2) - ((angle (A,C,B)) / 2) ;
set a2 = (angle (A,C,B)) / 2;
A9: ( sin (((angle (B,A,C)) + (angle (C,B,A))) / 2) = cos ((angle (A,C,B)) / 2) & cos (((angle (B,A,C)) + (angle (C,B,A))) / 2) = sin ((angle (A,C,B)) / 2) ) by A8, SIN_COS:79;
A10: sin ((angle (A,C,B)) / 2) <> 0 by A1, Th21;
A11: |.(C - B).| + |.(C - A).| <> 0
proof
( |.(C - B).| <> 0 & |.(C - A).| <> 0 ) by A3, EUCLID_6:42;
hence |.(C - B).| + |.(C - A).| <> 0 ; :: thesis: verum
end;
((sin (((angle (B,A,C)) + (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2))) * (|.(C - B).| - |.(C - A).|) = ((sin (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * (cos (((angle (B,A,C)) + (angle (C,B,A))) / 2))) * (|.(C - B).| + |.(C - A).|) by A3, Th58;
then (((|.(C - B).| - |.(C - A).|) * (cos ((angle (A,C,B)) / 2))) * (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2))) / (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2)) = (((|.(C - B).| + |.(C - A).|) * (sin ((angle (A,C,B)) / 2))) * (sin (((angle (B,A,C)) - (angle (C,B,A))) / 2))) / (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2)) by A9;
then ((|.(C - B).| - |.(C - A).|) * (cos ((angle (A,C,B)) / 2))) * ((cos (((angle (B,A,C)) - (angle (C,B,A))) / 2)) / (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2))) = ((|.(C - B).| + |.(C - A).|) * (sin ((angle (A,C,B)) / 2))) * ((sin (((angle (B,A,C)) - (angle (C,B,A))) / 2)) / (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2))) ;
then ((|.(C - B).| - |.(C - A).|) * (cos ((angle (A,C,B)) / 2))) * 1 = ((|.(C - B).| + |.(C - A).|) * (sin ((angle (A,C,B)) / 2))) * ((sin (((angle (B,A,C)) - (angle (C,B,A))) / 2)) / (cos (((angle (B,A,C)) - (angle (C,B,A))) / 2))) by A5, A4, Th59, XCMPLX_1:60;
then ((|.(C - B).| - |.(C - A).|) * (cos ((angle (A,C,B)) / 2))) / (sin ((angle (A,C,B)) / 2)) = (((|.(C - B).| + |.(C - A).|) * (tan (((angle (B,A,C)) - (angle (C,B,A))) / 2))) * (sin ((angle (A,C,B)) / 2))) / (sin ((angle (A,C,B)) / 2)) ;
then (|.(C - B).| - |.(C - A).|) * ((cos ((angle (A,C,B)) / 2)) / (sin ((angle (A,C,B)) / 2))) = ((|.(C - B).| + |.(C - A).|) * (tan (((angle (B,A,C)) - (angle (C,B,A))) / 2))) * ((sin ((angle (A,C,B)) / 2)) / (sin ((angle (A,C,B)) / 2)))
.= ((|.(C - B).| + |.(C - A).|) * (tan (((angle (B,A,C)) - (angle (C,B,A))) / 2))) * 1 by A10, XCMPLX_1:60 ;
then ((tan (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * (|.(C - B).| + |.(C - A).|)) / (|.(C - B).| + |.(C - A).|) = ((cot ((angle (A,C,B)) / 2)) * (|.(C - B).| - |.(C - A).|)) / (|.(C - B).| + |.(C - A).|) ;
then (tan (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * ((|.(C - B).| + |.(C - A).|) / (|.(C - B).| + |.(C - A).|)) = (cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)) ;
then (tan (((angle (B,A,C)) - (angle (C,B,A))) / 2)) * 1 = (cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)) by A11, XCMPLX_1:60;
hence tan (((angle (B,A,C)) - (angle (C,B,A))) / 2) = (cot ((angle (A,C,B)) / 2)) * ((|.(C - B).| - |.(C - A).|) / (|.(C - B).| + |.(C - A).|)) ; :: thesis: verum