let a be Real; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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
proof
A6: now :: thesis: ( D <> B & B <> C & D <> C )
A,B,D are_mutually_distinct by A2, EUCLID_6:20;
hence D <> B ; :: thesis: ( B <> C & D <> C )
A,B,C are_mutually_distinct by A1, EUCLID_6:20;
hence B <> C ; :: thesis: D <> C
thus D <> C by A3; :: thesis: verum
end;
then A7: D,B,C are_mutually_distinct ;
now :: thesis: ( not angle (D,B,C) = PI & not angle (B,C,D) = PI & not angle (C,D,B) = PI )
hereby :: thesis: verum
assume ( angle (D,B,C) = PI or angle (B,C,D) = PI or angle (C,D,B) = PI ) ; :: thesis: contradiction
per cases then ( angle (D,B,C) = PI or angle (B,C,D) = PI or angle (C,D,B) = PI ) ;
end;
end;
end;
hence D,B,C is_a_triangle by A7, EUCLID_6:20; :: thesis: verum
end;
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;
now :: thesis: ( A <> B & B <> C & A <> C & B <> D & C <> D )
A,B,C are_mutually_distinct by A1, EUCLID_6:20;
hence ( A <> B & B <> C & A <> C ) ; :: thesis: ( B <> D & C <> D )
D,B,C are_mutually_distinct by A5, EUCLID_6:20;
hence ( B <> D & C <> D ) ; :: thesis: verum
end;
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 :: thesis: ( 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)) ; :: thesis: 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 ; :: thesis: verum
end;
now :: thesis: ( 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))) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum