let a be Real; for A, B, C, D being Point of (TOP-REAL 2)
for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) & C <> D & not the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) holds
the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C))
let A, B, C, D be Point of (TOP-REAL 2); for b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) & C <> D & not the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) holds
the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C))
let b, r be Real; ( A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) & C <> D & not the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) implies the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C)) )
assume that
A1:
( A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) )
and
A2:
( A,B,D is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) & D in circle (a,b,r) )
and
A3:
C <> D
; ( the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) or the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C)) )
A4:
B,A,C is_a_triangle
by A1, MENELAUS:15;
A5:
D,B,C is_a_triangle
then A11:
( B,D,C is_a_triangle & B,A,C is_a_triangle )
by A1, MENELAUS:15;
A12:
( the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C)) & the_diameter_of_the_circumcircle (D,B,C) = - (the_diameter_of_the_circumcircle (B,D,C)) )
by A1, A5, EUCLID10:47;
then A13:
( angle (B,A,C) = angle (B,D,C) or angle (B,A,C) = (angle (B,D,C)) - PI or angle (B,A,C) = (angle (B,D,C)) + PI )
by A1, A2, EUCLID_6:34;
A14:
now ( sin (angle (B,A,C)) = sin (angle (B,D,C)) implies the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) )assume A15:
sin (angle (B,A,C)) = sin (angle (B,D,C))
;
the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C)thus the_diameter_of_the_circumcircle (
A,
B,
C) =
- (the_diameter_of_the_circumcircle (B,A,C))
by A1, EUCLID10:47
.=
- (- (|.(C - B).| / (sin (angle (B,A,C)))))
by A4, EUCLID10:45
.=
- (the_diameter_of_the_circumcircle (B,D,C))
by A11, EUCLID10:45, A15
.=
the_diameter_of_the_circumcircle (
D,
B,
C)
by A5, EUCLID10:47
;
verum end;
now ( sin (angle (B,A,C)) = - (sin (angle (B,D,C))) implies the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (B,D,C) )assume A16:
sin (angle (B,A,C)) = - (sin (angle (B,D,C)))
;
the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (B,D,C)thus the_diameter_of_the_circumcircle (
A,
B,
C) =
- (the_diameter_of_the_circumcircle (B,A,C))
by A1, EUCLID10:47
.=
- (- (|.(C - B).| / (sin (angle (B,A,C)))))
by A11, EUCLID10:45
.=
(- |.(C - B).|) / (sin (angle (B,D,C)))
by A16, XCMPLX_1:192
.=
- (|.(C - B).| / (sin (angle (B,D,C))))
.=
the_diameter_of_the_circumcircle (
B,
D,
C)
by A11, EUCLID10:45
;
verum end;
hence
( the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) or the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C)) )
by A13, Lm2, SIN_COS:79, A14, A12; verum