let A, B, C, D be Point of (TOP-REAL 2); :: thesis: for a, b, c, d being Real st A,C,B is_a_triangle & angle (A,C,B) < PI & A,D,B is_a_triangle & angle (A,D,B) < PI & a = angle (C,B,A) & b = angle (B,A,C) & c = angle (D,B,A) & d = angle (C,A,D) holds
|.(D - C).| ^2 = (|.(A - B).| ^2) * (((((sin a) / (sin (a + b))) ^2) + (((sin c) / (sin ((b + d) + c))) ^2)) - (((2 * ((sin a) / (sin (b + a)))) * ((sin c) / (sin ((b + d) + c)))) * (cos d)))
let a, b, c, d be Real; :: thesis: ( A,C,B is_a_triangle & angle (A,C,B) < PI & A,D,B is_a_triangle & angle (A,D,B) < PI & a = angle (C,B,A) & b = angle (B,A,C) & c = angle (D,B,A) & d = angle (C,A,D) implies |.(D - C).| ^2 = (|.(A - B).| ^2) * (((((sin a) / (sin (a + b))) ^2) + (((sin c) / (sin ((b + d) + c))) ^2)) - (((2 * ((sin a) / (sin (b + a)))) * ((sin c) / (sin ((b + d) + c)))) * (cos d))) )
assume that
A1: A,C,B is_a_triangle and
A2: angle (A,C,B) < PI and
A3: A,D,B is_a_triangle and
A4: angle (A,D,B) < PI and
A5: ( a = angle (C,B,A) & b = angle (B,A,C) & c = angle (D,B,A) & d = angle (C,A,D) ) ; :: thesis: |.(D - C).| ^2 = (|.(A - B).| ^2) * (((((sin a) / (sin (a + b))) ^2) + (((sin c) / (sin ((b + d) + c))) ^2)) - (((2 * ((sin a) / (sin (b + a)))) * ((sin c) / (sin ((b + d) + c)))) * (cos d)))
set e = b + d;
A6: ( b + d = angle (B,A,D) or b + d = (angle (B,A,D)) + (2 * PI) ) by A5, EUCLID_6:4;
A7: sin ((b + d) + c) = sin ((angle (B,A,D)) + (angle (D,B,A)))
proof
sin (((angle (B,A,D)) + c) + (2 * PI)) = sin ((angle (B,A,D)) + c) by SIN_COS:79;
hence sin ((b + d) + c) = sin ((angle (B,A,D)) + (angle (D,B,A))) by A5, A6; :: thesis: verum
end;
A8: |.(C - A).| = |.(A - C).| by EUCLID_6:43
.= (|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))) by A1, A2, Th64 ;
then A9: |.(C - A).| ^2 = (|.(A - B).| * ((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))))) ^2
.= (|.(A - B).| ^2) * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) ^2) by SQUARE_1:9 ;
A10: |.(D - A).| = |.(A - D).| by EUCLID_6:43
.= (|.(A - B).| * (sin (angle (D,B,A)))) / (sin ((angle (B,A,D)) + (angle (D,B,A)))) by A3, A4, Th64 ;
then A11: |.(D - A).| ^2 = (|.(A - B).| * ((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A)))))) ^2
.= (|.(A - B).| ^2) * (((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) ^2) by SQUARE_1:9 ;
|.(D - C).| ^2 = (((|.(A - B).| ^2) * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) ^2)) + ((|.(A - B).| ^2) * (((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) ^2))) - (((2 * ((|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))))) * ((|.(A - B).| * (sin (angle (D,B,A)))) / (sin ((angle (B,A,D)) + (angle (D,B,A)))))) * (cos (angle (C,A,D)))) by A8, A9, A10, A11, EUCLID_6:7
.= (((|.(A - B).| ^2) * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) ^2)) + ((|.(A - B).| ^2) * (((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) ^2))) - ((((2 * (((|.(A - B).| * |.(A - B).|) * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))))) * (sin (angle (D,B,A)))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) * (cos (angle (C,A,D))))
.= (((|.(A - B).| ^2) * (((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) ^2)) + ((|.(A - B).| ^2) * (((sin (angle (D,B,A))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) ^2))) - ((((2 * (((|.(A - B).| ^2) * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))))) * (sin (angle (D,B,A)))) / (sin ((angle (B,A,D)) + (angle (D,B,A))))) * (cos (angle (C,A,D)))) by SQUARE_1:def 1
.= (|.(A - B).| ^2) * (((((sin a) / (sin (a + b))) ^2) + (((sin c) / (sin ((b + d) + c))) ^2)) - (((2 * ((sin a) / (sin (b + a)))) * ((sin c) / (sin ((b + d) + c)))) * (cos d))) by A5, A7 ;
hence |.(D - C).| ^2 = (|.(A - B).| ^2) * (((((sin a) / (sin (a + b))) ^2) + (((sin c) / (sin ((b + d) + c))) ^2)) - (((2 * ((sin a) / (sin (b + a)))) * ((sin c) / (sin ((b + d) + c)))) * (cos d))) ; :: thesis: verum