let a be Real; :: thesis: for A, B, C 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) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r holds
the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)
let A, B, C 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) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r holds
the_diameter_of_the_circumcircle (A,B,C) = - (2 * r)
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) & not the_diameter_of_the_circumcircle (A,B,C) = 2 * r implies the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
assume that
A1: A,B,C is_a_triangle and
A2: ( A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) ) ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
A3: r is positive by A1, A2, EUCLID10:37;
then consider D being Point of (TOP-REAL 2) such that
A4: C <> D and
A5: D in circle (a,b,r) and
A6: |[a,b]| in LSeg (C,D) by A2, EUCLID_6:32;
A7: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
per cases ( D = B or D <> B ) ;
suppose A8: D = B ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
then A9: ( B,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg (B,C) ) by A6, A7, A2, A3, EUCLID10:38;
A10: B,A,C is_a_triangle by A1, MENELAUS:15;
A11: the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C)) by A1, EUCLID10:47
.= - (|.(C - B).| / (sin (angle (C,A,B)))) by A10, EUCLID10:44 ;
( angle (B,A,C) in ].0,PI.[ or angle (B,A,C) in ].PI,(2 * PI).[ )
proof
A12: ( ( 0 <= angle (B,A,C) & angle (B,A,C) < PI ) or angle (B,A,C) = PI or ( PI < angle (B,A,C) & angle (B,A,C) < 2 * PI ) ) by EUCLID11:3;
( ( 0 < angle (B,A,C) & angle (B,A,C) < PI ) or ( PI < angle (B,A,C) & angle (B,A,C) < 2 * PI ) ) by A12, A1, EUCLID10:30, A2, A7, EUCLID_6:35;
hence ( angle (B,A,C) in ].0,PI.[ or angle (B,A,C) in ].PI,(2 * PI).[ ) by XXREAL_1:4; :: thesis: verum
end;
per cases then ( angle (B,A,C) in ].0,PI.[ or angle (B,A,C) in ].PI,(2 * PI).[ ) ;
suppose A13: angle (B,A,C) in ].0,PI.[ ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
then ( 0 < angle (B,A,C) & angle (B,A,C) < PI & B,A,C are_mutually_distinct ) by A7, XXREAL_1:4;
then ( 0 < angle (A,C,B) & angle (A,C,B) < PI ) by EUCLID11:5;
then A14: ( C,A,B is_a_triangle & angle (B,A,C) in ].0,PI.[ & angle (A,C,B) in ].0,PI.[ & |[a,b]| in LSeg (C,B) ) by A13, A1, MENELAUS:15, A6, A8, XXREAL_1:4;
angle (C,A,B) = (2 * PI) - (angle (B,A,C)) by A1, EUCLID10:31
.= (2 * PI) - (PI / 2) by A14, A2, EUCLID10:39
.= (3 * PI) / 2 ;
then the_diameter_of_the_circumcircle (A,B,C) = |.(B - C).| by EUCLID_6:43, A11, SIN_COS:77
.= 2 * r by A9, A2, A3, EUCLID10:58 ;
hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum
end;
suppose angle (B,A,C) in ].PI,(2 * PI).[ ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
then ( PI < angle (B,A,C) & angle (B,A,C) < 2 * PI & B,A,C are_mutually_distinct ) by A7, XXREAL_1:4;
then ( PI < angle (A,C,B) & angle (A,C,B) < 2 * PI ) by EUCLID11:2, EUCLID11:8;
then ( (2 * PI) - (angle (A,C,B)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (A,C,B)) & angle (B,C,A) = (2 * PI) - (angle (A,C,B)) ) by A1, EUCLID10:31, XREAL_1:15, XREAL_1:50;
then ( 0 < angle (B,C,A) & angle (B,C,A) < PI & B,C,A are_mutually_distinct ) by A7;
then ( 0 < angle (A,B,C) & angle (A,B,C) < PI & 0 < angle (C,A,B) & angle (C,A,B) < PI ) by EUCLID11:5;
then ( B,A,C is_a_triangle & angle (C,A,B) in ].0,PI.[ & angle (A,B,C) in ].0,PI.[ & |[a,b]| in LSeg (B,C) ) by A1, MENELAUS:15, A6, A8, XXREAL_1:4;
then sin (angle (C,A,B)) = 1 by SIN_COS:77, A2, EUCLID10:39;
then the_diameter_of_the_circumcircle (A,B,C) = - |.(B - C).| by A11, EUCLID_6:43
.= - (2 * r) by A9, A2, A3, EUCLID10:58 ;
hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum
end;
end;
end;
suppose A15: D <> B ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
then A16: D,B,C are_mutually_distinct by A4, A7;
A17: 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 ) ;
suppose angle (D,B,C) = PI ; :: thesis: contradiction
then A18: B in LSeg (D,C) by EUCLID_6:11;
( B in LSeg (D,B) & B <> C & B in circle (a,b,r) & C in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A7, RLTOPSP1:68;
hence contradiction by A15, A18, EUCLID_6:30; :: thesis: verum
end;
suppose angle (B,C,D) = PI ; :: thesis: contradiction
then A19: C in LSeg (B,D) by EUCLID_6:11;
( C in LSeg (B,C) & C <> D & B in circle (a,b,r) & C in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A4, RLTOPSP1:68;
hence contradiction by A7, A19, EUCLID_6:30; :: thesis: verum
end;
suppose angle (C,D,B) = PI ; :: thesis: contradiction
then A20: D in LSeg (C,B) by EUCLID_6:11;
( D in LSeg (C,D) & D <> B & B in circle (a,b,r) & C in circle (a,b,r) & D in circle (a,b,r) ) by A15, A2, A5, RLTOPSP1:68;
hence contradiction by A4, A20, EUCLID_6:30; :: thesis: verum
end;
end;
end;
end;
then A21: D,B,C is_a_triangle by A16, EUCLID_6:20;
per cases ( A = D or A <> D ) ;
suppose A22: A = D ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
A23: ( A,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg (A,C) ) by A22, A6, A7, A2, A3, EUCLID10:38;
A24: the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (sin (angle (C,B,A))) by A1, EUCLID10:44;
( angle (C,B,A) in ].0,PI.[ or angle (C,B,A) in ].PI,(2 * PI).[ )
proof
( ( 0 <= angle (C,B,A) & angle (C,B,A) < PI ) or angle (C,B,A) = PI or ( PI < angle (C,B,A) & angle (C,B,A) < 2 * PI ) ) by EUCLID11:3;
then ( ( 0 < angle (C,B,A) & angle (C,B,A) < PI ) or ( PI < angle (C,B,A) & angle (C,B,A) < 2 * PI ) ) by A2, A7, EUCLID_6:35, A1, EUCLID10:30;
hence ( angle (C,B,A) in ].0,PI.[ or angle (C,B,A) in ].PI,(2 * PI).[ ) by XXREAL_1:4; :: thesis: verum
end;
per cases then ( angle (C,B,A) in ].0,PI.[ or angle (C,B,A) in ].PI,(2 * PI).[ ) ;
suppose angle (C,B,A) in ].PI,(2 * PI).[ ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
then ( PI < angle (C,B,A) & 2 * PI <= 2 * PI & angle (C,B,A) < 2 * PI ) by XXREAL_1:4;
then A26: ( (2 * PI) - (angle (C,B,A)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (C,B,A)) & angle (A,B,C) = (2 * PI) - (angle (C,B,A)) ) by A1, EUCLID10:31, XREAL_1:15, XREAL_1:50;
then ( 0 < angle (B,C,A) & angle (B,C,A) < PI & 0 < angle (C,A,B) & angle (C,A,B) < PI ) by A7, EUCLID11:5;
then A27: ( C,B,A is_a_triangle & angle (A,B,C) in ].0,PI.[ & angle (B,C,A) in ].0,PI.[ & |[a,b]| in LSeg (C,A) ) by A26, XXREAL_1:4, A1, MENELAUS:15, A6, A22;
angle (C,B,A) = (2 * PI) - (angle (A,B,C)) by A1, EUCLID10:31
.= (2 * PI) - (PI / 2) by A27, A2, EUCLID10:39
.= (3 * PI) / 2 ;
then the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (- 1) by A1, EUCLID10:44, SIN_COS:77
.= - |.(C - A).|
.= - |.(A - C).| by EUCLID_6:43
.= - (2 * r) by A23, A2, A3, EUCLID10:58 ;
hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) ; :: thesis: verum
end;
end;
end;
suppose A28: A <> D ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
then A29: A,B,D are_mutually_distinct by A15, A7;
A30: D,B,C are_mutually_distinct by A15, A4, A7;
A31: ( D,C,|[a,b]| are_mutually_distinct & |[a,b]| in LSeg (D,C) ) by A6, A5, A4, A2, A3, EUCLID10:38;
A32: ( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ )
proof
( ( 0 <= angle (C,B,D) & angle (C,B,D) < PI ) or angle (C,B,D) = PI or ( PI < angle (C,B,D) & angle (C,B,D) < 2 * PI ) ) by EUCLID11:3;
then ( ( 0 < angle (C,B,D) & angle (C,B,D) < PI ) or ( PI < angle (C,B,D) & angle (C,B,D) < 2 * PI ) ) by A21, EUCLID10:30, A5, A2, EUCLID_6:35, A15, A7;
hence ( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ ) by XXREAL_1:4; :: thesis: verum
end;
now :: thesis: ( not angle (A,B,D) = PI & not angle (B,D,A) = PI & not angle (D,A,B) = PI )
hereby :: thesis: verum
assume ( angle (A,B,D) = PI or angle (B,D,A) = PI or angle (D,A,B) = PI ) ; :: thesis: contradiction
per cases then ( angle (A,B,D) = PI or angle (B,D,A) = PI or angle (D,A,B) = PI ) ;
suppose angle (A,B,D) = PI ; :: thesis: contradiction
then A33: B in LSeg (A,D) by EUCLID_6:11;
( B in LSeg (A,B) & B <> D & B in circle (a,b,r) & A in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A15, RLTOPSP1:68;
hence contradiction by A7, A33, EUCLID_6:30; :: thesis: verum
end;
suppose angle (B,D,A) = PI ; :: thesis: contradiction
then A34: D in LSeg (B,A) by EUCLID_6:11;
( D in LSeg (B,D) & D <> A & B in circle (a,b,r) & A in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A28, RLTOPSP1:68;
hence contradiction by A15, A34, EUCLID_6:30; :: thesis: verum
end;
suppose angle (D,A,B) = PI ; :: thesis: contradiction
then A35: A in LSeg (D,B) by EUCLID_6:11;
( A in LSeg (D,A) & A <> B & B in circle (a,b,r) & A in circle (a,b,r) & D in circle (a,b,r) ) by A2, A5, A7, RLTOPSP1:68;
hence contradiction by A28, A35, EUCLID_6:30; :: thesis: verum
end;
end;
end;
end;
then ( A,B,D is_a_triangle & A,B,C is_a_triangle ) by A29, A1, EUCLID_6:20;
per cases then ( 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 A4, A5, A2, Th51;
suppose A36: the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (D,B,C) ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
per cases ( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ ) by A32;
suppose A37: angle (C,B,D) in ].0,PI.[ ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
now :: thesis: ( angle (C,B,D) in ].0,PI.[ & angle (B,D,C) in ].0,PI.[ & |[a,b]| in LSeg (D,C) )
thus angle (C,B,D) in ].0,PI.[ by A37; :: thesis: ( angle (B,D,C) in ].0,PI.[ & |[a,b]| in LSeg (D,C) )
( 0 < angle (C,B,D) & angle (C,B,D) < PI & C,B,D are_mutually_distinct ) by A37, A15, A4, A7, XXREAL_1:4;
then ( 0 < angle (B,D,C) & angle (B,D,C) < PI ) by EUCLID11:5;
hence angle (B,D,C) in ].0,PI.[ by XXREAL_1:4; :: thesis: |[a,b]| in LSeg (D,C)
thus |[a,b]| in LSeg (D,C) by A6; :: thesis: verum
end;
then sin (angle (C,B,D)) = 1 by SIN_COS:77, A17, A16, EUCLID_6:20, A5, A2, EUCLID10:39;
then the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / 1 by A17, A16, EUCLID_6:20, EUCLID10:44
.= |.(D - C).| by EUCLID_6:43
.= 2 * r by A31, A5, A2, A3, EUCLID10:58 ;
hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A36; :: thesis: verum
end;
suppose angle (C,B,D) in ].PI,(2 * PI).[ ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
then ( PI < angle (C,B,D) & 2 * PI <= 2 * PI & angle (C,B,D) < 2 * PI ) by XXREAL_1:4;
then A38: ( (2 * PI) - (angle (C,B,D)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (C,B,D)) & angle (D,B,C) = (2 * PI) - (angle (C,B,D)) ) by A21, EUCLID10:31, XREAL_1:15, XREAL_1:50;
( 0 < angle (B,C,D) & angle (B,C,D) < PI & 0 < angle (C,D,B) & angle (C,D,B) < PI ) by A38, A30, EUCLID11:5;
then A39: ( C,B,D is_a_triangle & angle (D,B,C) in ].0,PI.[ & angle (B,C,D) in ].0,PI.[ & |[a,b]| in LSeg (C,D) ) by A38, XXREAL_1:4, A21, MENELAUS:15, A6;
A40: angle (C,B,D) = (2 * PI) - (angle (D,B,C)) by A21, EUCLID10:31
.= (2 * PI) - (PI / 2) by A39, A5, A2, EUCLID10:39
.= (3 * PI) / 2 ;
the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / (sin (angle (C,B,D))) by A17, A16, EUCLID_6:20, EUCLID10:44
.= - (|.(C - D).| / 1) by A40, SIN_COS:77
.= - |.(D - C).| by EUCLID_6:43
.= - (2 * r) by A31, A5, A2, A3, EUCLID10:58 ;
hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A36; :: thesis: verum
end;
end;
end;
suppose A41: the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (D,B,C)) ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
per cases ( angle (C,B,D) in ].0,PI.[ or angle (C,B,D) in ].PI,(2 * PI).[ ) by A32;
suppose A42: angle (C,B,D) in ].0,PI.[ ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
A43: now :: thesis: ( angle (C,B,D) in ].0,PI.[ & angle (B,D,C) in ].0,PI.[ & |[a,b]| in LSeg (D,C) )
thus angle (C,B,D) in ].0,PI.[ by A42; :: thesis: ( angle (B,D,C) in ].0,PI.[ & |[a,b]| in LSeg (D,C) )
( 0 < angle (C,B,D) & angle (C,B,D) < PI & C,B,D are_mutually_distinct ) by A42, A15, A4, A7, XXREAL_1:4;
then ( 0 < angle (B,D,C) & angle (B,D,C) < PI ) by EUCLID11:5;
hence angle (B,D,C) in ].0,PI.[ by XXREAL_1:4; :: thesis: |[a,b]| in LSeg (D,C)
thus |[a,b]| in LSeg (D,C) by A6; :: thesis: verum
end;
the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / (sin (angle (C,B,D))) by A17, A16, EUCLID_6:20, EUCLID10:44
.= |.(C - D).| / 1 by A43, SIN_COS:77, A17, A16, EUCLID_6:20, A5, A2, EUCLID10:39
.= |.(D - C).| by EUCLID_6:43
.= 2 * r by A31, A2, A5, A3, EUCLID10:58 ;
hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A41; :: thesis: verum
end;
suppose angle (C,B,D) in ].PI,(2 * PI).[ ; :: thesis: ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) )
then ( PI < angle (C,B,D) & 2 * PI <= 2 * PI & angle (C,B,D) < 2 * PI ) by XXREAL_1:4;
then A44: ( (2 * PI) - (angle (C,B,D)) < (2 * PI) - PI & 0 < (2 * PI) - (angle (C,B,D)) & angle (D,B,C) = (2 * PI) - (angle (C,B,D)) ) by A21, EUCLID10:31, XREAL_1:15, XREAL_1:50;
then ( 0 < angle (B,C,D) & angle (B,C,D) < PI & 0 < angle (C,D,B) & angle (C,D,B) < PI ) by A30, EUCLID11:5;
then A45: ( C,B,D is_a_triangle & angle (D,B,C) in ].0,PI.[ & angle (B,C,D) in ].0,PI.[ & |[a,b]| in LSeg (C,D) ) by XXREAL_1:4, A44, A21, MENELAUS:15, A6;
A46: angle (C,B,D) = (2 * PI) - (angle (D,B,C)) by A21, EUCLID10:31
.= (2 * PI) - (PI / 2) by A45, A5, A2, EUCLID10:39
.= (3 * PI) / 2 ;
the_diameter_of_the_circumcircle (D,B,C) = |.(C - D).| / (- 1) by A46, SIN_COS:77, A17, A16, EUCLID_6:20, EUCLID10:44
.= - |.(C - D).|
.= - |.(D - C).| by EUCLID_6:43
.= - (2 * r) by A31, A5, A2, A3, EUCLID10:58 ;
hence ( the_diameter_of_the_circumcircle (A,B,C) = 2 * r or the_diameter_of_the_circumcircle (A,B,C) = - (2 * r) ) by A41; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;