let A, B, C, P be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & A,B,P is_a_triangle & angle (C,B,A) < PI & angle (A,P,B) < PI & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0 implies |.(A - P).| = - (((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((angle (C,B,A)) / 3))) )
assume that
A1: A,B,C is_a_triangle and
A2: A,B,P is_a_triangle and
A3: angle (C,B,A) < PI and
A4: angle (A,P,B) < PI and
A5: angle (P,B,A) = (angle (C,B,A)) / 3 and
A6: angle (B,A,P) = (angle (B,A,C)) / 3 and
A7: sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0 ; :: thesis: |.(A - P).| = - (((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((angle (C,B,A)) / 3)))
A8: (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3 by A1, A3, Lm12;
A,B,P are_mutually_distinct by A2, EUCLID_6:20;
then A9: |.(A - P).| * (sin (((2 * PI) / 3) + ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3)) by A5, A6, A4, A8, Thm35;
sin (angle (A,C,B)) = sin (3 * ((angle (A,C,B)) / 3))
.= ((4 * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) by Thm18 ;
then A10: |.(A - P).| * (sin (((2 * PI) / 3) + ((angle (A,C,B)) / 3))) = ((the_diameter_of_the_circumcircle (A,B,C)) * (((4 * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3))))) * (sin ((angle (C,B,A)) / 3)) by A9, A1, Thm34;
|.(A - P).| * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) = ((the_diameter_of_the_circumcircle (A,B,C)) * (((4 * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3))))) * (sin ((angle (C,B,A)) / 3)) by A10, Thm7;
then |.(A - P).| = ((((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((angle (C,B,A)) / 3))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3)))) / (sin ((PI / 3) - ((angle (A,C,B)) / 3))) by A7, XCMPLX_1:89;
then A11: |.(A - P).| = (((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((angle (C,B,A)) / 3))) * ((sin ((PI / 3) - ((angle (A,C,B)) / 3))) / (sin ((PI / 3) - ((angle (A,C,B)) / 3)))) by XCMPLX_1:74;
(sin ((PI / 3) - ((angle (A,C,B)) / 3))) / (sin ((PI / 3) - ((angle (A,C,B)) / 3))) = 1 by A7, XCMPLX_1:60;
then |.(A - P).| = ((((- (the_diameter_of_the_circumcircle (C,B,A))) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((angle (C,B,A)) / 3)) by A11, A1, Thm33;
hence |.(A - P).| = - (((((the_diameter_of_the_circumcircle (C,B,A)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((angle (C,B,A)) / 3))) ; :: thesis: verum