let A, B, C, P be Point of (TOP-REAL 2); ( 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
; |.(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)))
; verum