euclid10.miz

begin

 theorem :: EUCLID10:1



 Thm1: for a be Real holds ( sin ( PI - a)) = ( sin a)

 proof

 let a be Real;

 ( sin ( PI - a)) = (( 0 * ( cos a)) - (( cos PI ) * ( sin a))) by SIN_COS: 77, SIN_COS: 82

 .= ( sin a) by SIN_COS: 77;

 hence thesis;

 end;

 theorem :: EUCLID10:2

 for a be Real holds ( cos ( PI - a)) = ( - ( cos a))

 proof

 let a be Real;

 ( cos ( PI - a)) = ((( cos PI ) * ( cos a)) + (( sin PI ) * ( sin a))) by SIN_COS: 83

 .= ( - ( cos a)) by SIN_COS: 77;

 hence thesis;

 end;

 theorem :: EUCLID10:3

 for a be Real holds ( sin ((2 * PI ) - a)) = ( - ( sin a))

 proof

 let a be Real;

 ( sin ((2 * PI ) - a)) = (( 0 * ( cos a)) - (( cos (2 * PI )) * ( sin a))) by SIN_COS: 77, SIN_COS: 82

 .= ( - ( sin a)) by SIN_COS: 77;

 hence thesis;

 end;

 theorem :: EUCLID10:4

 for a be Real holds ( cos ((2 * PI ) - a)) = ( cos a)

 proof

 let a be Real;

 ( cos ((2 * PI ) - a)) = ((1 * ( cos a)) + ( 0 * ( sin a))) by SIN_COS: 77, SIN_COS: 83

 .= ( cos a);

 hence thesis;

 end;

 theorem :: EUCLID10:5



 Thm2: for a be Real holds ( sin (( - (2 * PI )) + a)) = ( sin a)

 proof

 let a be Real;

 ( sin (( - (2 * PI )) + a)) = ( sin (a - (2 * PI )))

 .= ((( sin a) * 1) - (( cos a) * ( sin (2 * PI )))) by SIN_COS: 77, SIN_COS: 82

 .= ( sin a) by SIN_COS: 77;

 hence thesis;

 end;

 theorem :: EUCLID10:6

 for a be Real holds ( cos (( - (2 * PI )) + a)) = ( cos a)

 proof

 let a be Real;

 ( cos (( - (2 * PI )) + a)) = ( cos (a - (2 * PI )))

 .= ((( cos a) * 1) + (( sin a) * ( sin (2 * PI )))) by SIN_COS: 77, SIN_COS: 83

 .= ( cos a) by SIN_COS: 77;

 hence thesis;

 end;

 theorem :: EUCLID10:7



 Thm3: for a be Real holds ( sin (((3 * PI ) / 2) + a)) = ( - ( cos a))

 proof

 let a be Real;

 ( sin (((3 * PI ) / 2) + a)) = ((( sin ((3 * PI ) / 2)) * ( cos a)) + (( cos ((3 * PI ) / 2)) * ( sin a))) by SIN_COS: 75

 .= ( - ( cos a)) by SIN_COS: 77;

 hence thesis;

 end;

 theorem :: EUCLID10:8



 Thm4: for a be Real holds ( cos (((3 * PI ) / 2) + a)) = ( sin a)

 proof

 let a be Real;

 ( cos (((3 * PI ) / 2) + a)) = ((( cos ((3 * PI ) / 2)) * ( cos a)) - (( sin ((3 * PI ) / 2)) * ( sin a))) by SIN_COS: 75

 .= ( - ( - ( sin a))) by SIN_COS: 77;

 hence thesis;

 end;

 theorem :: EUCLID10:9

 for a be Real holds ( sin (((3 * PI ) / 2) + a)) = ( - ( sin (( PI / 2) - a)))

 proof

 let a be Real;

 ( sin (((3 * PI ) / 2) + a)) = ( - ( cos a)) by Thm3

 .= ( - ( sin (( PI / 2) - a))) by SIN_COS: 79;

 hence thesis;

 end;

 theorem :: EUCLID10:10

 for a be Real holds ( cos (((3 * PI ) / 2) + a)) = ( cos (( PI / 2) - a))

 proof

 let a be Real;

 ( cos (((3 * PI ) / 2) + a)) = ( sin a) by Thm4

 .= ( cos (( PI / 2) - a)) by SIN_COS: 79;

 hence thesis;

 end;

 theorem :: EUCLID10:11



 Thm5: for a be Real holds ( sin (((2 * PI ) / 3) - a)) = ( sin (( PI / 3) + a))

 proof

 let a be Real;

 ( sin (((2 * PI ) / 3) - a)) = ( sin ( PI - (( PI / 3) + a)))

 .= ((( sin PI ) * ( cos (( PI / 3) + a))) - (( cos PI ) * ( sin (( PI / 3) + a)))) by SIN_COS: 82

 .= ( sin (( PI / 3) + a)) by SIN_COS: 77;

 hence thesis;

 end;

 theorem :: EUCLID10:12



 Thm6: for a be Real holds ( cos (((2 * PI ) / 3) - a)) = ( - ( cos (( PI / 3) + a)))

 proof

 let a be Real;

 ( cos (((2 * PI ) / 3) - a)) = ( cos ( PI - (( PI / 3) + a)))

 .= ((( cos PI ) * ( cos (( PI / 3) + a))) + (( sin PI ) * ( sin (( PI / 3) + a)))) by SIN_COS: 83

 .= ( - ( cos (( PI / 3) + a))) by SIN_COS: 77;

 hence thesis;

 end;

 theorem :: EUCLID10:13



 Thm7: for a be Real holds ( sin (((2 * PI ) / 3) + a)) = ( sin (( PI / 3) - a))

 proof

 let a be Real;

 ( sin (((2 * PI ) / 3) + a)) = ( sin ( PI - (( PI / 3) - a)))

 .= ((( sin PI ) * ( cos (( PI / 3) - a))) - (( cos PI ) * ( sin (( PI / 3) - a)))) by SIN_COS: 82

 .= ( sin (( PI / 3) - a)) by SIN_COS: 77;

 hence thesis;

 end;



 Lm1: ( angle ( |[ 0 , 0 ]|, |[ 0 , 1]|, |[(( sqrt 3) / 2), (1 / 2)]|)) < PI

 proof

 set O = ( euc2cpx |[ 0 , 0 ]|);

 set A = ( euc2cpx |[ 0 , 1]|);

 set B = ( euc2cpx |[(( sqrt 3) / 2), (1 / 2)]|);

 ( |[ 0 , 0 ]| `1 ) = 0 & ( |[ 0 , 0 ]| `2 ) = 0 & ( |[ 0 , 1]| `1 ) = 0 & ( |[ 0 , 1]| `2 ) = 1 & ( |[(( sqrt 3) / 2), (1 / 2)]| `1 ) = (( sqrt 3) / 2) & ( |[(( sqrt 3) / 2), (1 / 2)]| `2 ) = (1 / 2) by EUCLID: 52;

 then

 A1: O = ( 0 + ( 0 * )) & A = ( 0 + (1 * )) & B = ((( sqrt 3) / 2) + ((1 / 2) * )) by EUCLID_3:def 2;



 A2: ( Arg (( - 1) * )) = ((3 / 2) * PI ) by COMPTRIG: 38;

 (B - A) = ((( sqrt 3) / 2) + (( - (1 / 2)) * )) by A1;

 then

 A3: ( Re (B - A)) = (( sqrt 3) / 2) & ( Im (B - A)) = ( - (1 / 2)) by COMPLEX1: 12;

 ( sqrt 3) > 0 by SQUARE_1: 25;

 then ( Arg (B - A)) in ].((3 / 2) * PI ), (2 * PI ).[ by A3, COMPTRIG: 44;

 then ((3 / 2) * PI ) < ( Arg (B - A)) & ( Arg (B - A)) < (2 * PI ) by XXREAL_1: 4;

 then

 A4: (((3 / 2) * PI ) - ((3 / 2) * PI )) < (( Arg (B - A)) - ((3 / 2) * PI )) & (( Arg (B - A)) - ((3 / 2) * PI )) < ((2 * PI ) - ((3 / 2) * PI )) by XREAL_1: 14;

 set th = (( Arg (B - A)) - ( Arg (O - A)));

 PI in ]. 0 , 4.[ by SIN_COS:def 28;

 then

 A5: 0 < PI by XXREAL_1: 4;

 th < ((1 / 2) * PI ) & ((1 / 2) * PI ) < PI by A1, A2, A4, A5, XREAL_1: 157;

 then

 A6: not PI <= th by XXREAL_0: 2;

 ( angle (O,A,B)) = th by A1, A2, A4, COMPLEX2:def 4;

 hence thesis by A6, EUCLID_3:def 4;

 end;



 Lm2: |. |[(( sqrt 3) / 2), (1 / 2)]|.| = 1

 proof

 set B = |[(( sqrt 3) / 2), (1 / 2)]|;

 (B `1 ) = (( sqrt 3) / 2) & (B `2 ) = (1 / 2) by EUCLID: 52;

 then

 A1: |.B.| = ( sqrt (((( sqrt 3) / 2) ^2 ) + ((1 / 2) ^2 ))) by JGRAPH_1: 30;



 A2: ((( sqrt 3) / 2) ^2 ) = ((( sqrt 3) / 2) * (( sqrt 3) / 2)) by SQUARE_1:def 1;



 A3: ((1 / 2) ^2 ) = ((1 / 2) * (1 / 2)) by SQUARE_1:def 1;

 (( sqrt 3) ^2 ) = 3 by SQUARE_1:def 2;

 then (((( sqrt 3) * ( sqrt 3)) / 2) / 2) = ((3 / 2) / 2) by SQUARE_1:def 1;

 hence thesis by A1, A2, A3, SQUARE_1: 18;

 end;



 Lm3: for O,A,B be Point of ( TOP-REAL 2) st O = |[ 0 , 0 ]| & A = |[ 0 , 1]| & B = |[(( sqrt 3) / 2), (1 / 2)]| holds |.(O - A).| = |.(O - B).| & |.(O - A).| = |.(A - B).| & |.(O - A).| = 1

 proof

 let O,A,B be Point of ( TOP-REAL 2) such that

 A1: O = |[ 0 , 0 ]| and

 A2: A = |[ 0 , 1]| and

 A3: B = |[(( sqrt 3) / 2), (1 / 2)]|;



 A4: (A `1 ) = 0 & (A `2 ) = 1 & (O `1 ) = 0 & (O `2 ) = 0 & (B `1 ) = (( sqrt 3) / 2) & (B `2 ) = (1 / 2) by A1, A2, A3, EUCLID: 52;

 then

 A5: (A - O) = |[( 0 - 0 ), (1 - 0 )]| by EUCLID: 61;

 ( 0 ^2 ) = ( 0 * 0 ) & (1 ^2 ) = (1 * 1) by SQUARE_1:def 1;

 then

 A6: |.A.| = ( sqrt (( 0 * 0 ) + (1 * 1))) by A4, JGRAPH_1: 30;



 A7: (B - O) = |[((( sqrt 3) / 2) - 0 ), ((1 / 2) - 0 )]| by A4, EUCLID: 61

 .= |[(( sqrt 3) / 2), (1 / 2)]|;

 (A - B) = |[( 0 - (( sqrt 3) / 2)), (1 - (1 / 2))]| by A4, EUCLID: 61;

 then ((A - B) `1 ) = ( - (( sqrt 3) / 2)) & ((A - B) `2 ) = (1 / 2) by EUCLID: 52;

 then

 A8: |.(A - B).| = ( sqrt ((( - (( sqrt 3) / 2)) ^2 ) + ((1 / 2) ^2 ))) by JGRAPH_1: 30;



 A9: (( - (( sqrt 3) / 2)) ^2 ) = (( - (( sqrt 3) / 2)) * ( - (( sqrt 3) / 2))) by SQUARE_1:def 1;



 A10: ((1 / 2) ^2 ) = ((1 / 2) * (1 / 2)) by SQUARE_1:def 1;

 (( sqrt 3) ^2 ) = 3 by SQUARE_1:def 2;

 then

 A11: (((( sqrt 3) * ( sqrt 3)) / 2) / 2) = ((3 / 2) / 2) by SQUARE_1:def 1;

 |.(O - B).| = |.(B - O).| by EUCLID_6: 43;

 hence thesis by EUCLID_6: 43, A6, A5, A2, A9, A10, A8, A11, SQUARE_1: 18, A7, Lm2;

 end;



 Lm4: for O,A,B be Point of ( TOP-REAL 2) st O = |[ 0 , 0 ]| & A = |[ 0 , 1]| & B = |[(( sqrt 3) / 2), (1 / 2)]| holds O <> A & A <> B & O <> B & A <> O & B <> A & B <> O

 proof

 let O,A,B be Point of ( TOP-REAL 2) such that

 A1: O = |[ 0 , 0 ]| and

 A2: A = |[ 0 , 1]| and

 A3: B = |[(( sqrt 3) / 2), (1 / 2)]|;

 O <> A & A <> B & O <> B

 proof

 (O `2 ) = 0 & (B `2 ) = (1 / 2) by A1, A3, EUCLID: 52;

 hence thesis by A2, EUCLID: 52;

 end;

 hence thesis;

 end;



 Lm5: for O,A,B be Point of ( TOP-REAL 2) st O = |[ 0 , 0 ]| & A = |[ 0 , 1]| & B = |[(( sqrt 3) / 2), (1 / 2)]| holds ( angle (B,O,A)) = ( angle (O,A,B)) & ( angle (O,A,B)) = ( angle (A,B,O))

 proof

 let O,A,B be Point of ( TOP-REAL 2) such that

 A1: O = |[ 0 , 0 ]| and

 A2: A = |[ 0 , 1]| and

 A3: B = |[(( sqrt 3) / 2), (1 / 2)]|;



 A4: |.(O - A).| = |.(O - B).| & |.(O - A).| = |.(A - B).| by A1, A2, A3, Lm3;

 then

 A5: |.(O - A).| = |.(B - O).| & |.(A - O).| = |.(O - B).| & |.(O - A).| = |.(B - A).| & |.(A - O).| = |.(A - B).| by EUCLID_6: 43;

 O <> A & A <> B & O <> B by A1, A2, A3, Lm4;

 hence thesis by A4, A5, EUCLID_6: 16;

 end;



 Lm6: for O,A,B be Point of ( TOP-REAL 2) st O = |[ 0 , 0 ]| & A = |[ 0 , 1]| & B = |[(( sqrt 3) / 2), (1 / 2)]| & ( angle (O,A,B)) < PI holds ( angle (B,O,A)) = ( PI / 3)

 proof

 let O,A,B be Point of ( TOP-REAL 2) such that

 A1: O = |[ 0 , 0 ]| and

 A2: A = |[ 0 , 1]| and

 A3: B = |[(( sqrt 3) / 2), (1 / 2)]| and

 A4: ( angle (O,A,B)) < PI ;

 A <> O & O <> B & B <> A by A1, A2, A3, Lm4;

 then

 A5: ((( angle (O,A,B)) + ( angle (A,B,O))) + ( angle (B,O,A))) = PI by A4, EUCLID_3: 47;

 ( angle (B,O,A)) = ( angle (O,A,B)) & ( angle (O,A,B)) = ( angle (A,B,O)) by A1, A2, A3, Lm5;

 hence thesis by A5;

 end;

 theorem :: EUCLID10:14



 Thm8: ( cos ( PI / 3)) = (1 / 2)

 proof

 set O = |[ 0 , 0 ]|;

 set A = |[ 0 , 1]|;

 set B = |[(( sqrt 3) / 2), (1 / 2)]|;

 set a = |.(B - O).|;

 set b = |.(A - O).|;

 set c = |.(A - B).|;

 |.(O - A).| = |.(O - B).| & |.(O - A).| = |.(A - B).| & |.(O - A).| = 1 by Lm3;

 then

 A1: b = 1 & c = 1 & a = 1 by EUCLID_6: 43;

 (1 ^2 ) = (1 * 1) by SQUARE_1:def 1

 .= 1;

 then 1 = ((1 + 1) - (((2 * 1) * 1) * ( cos ( angle (B,O,A))))) by A1, EUCLID_6: 7;

 hence thesis by Lm1, Lm6;

 end;

 theorem :: EUCLID10:15



 Thm9: ( sin ( PI / 3)) = (( sqrt 3) / 2)

 proof



 A1: ((( sin ( PI / 3)) ^2 ) + (( cos ( PI / 3)) ^2 )) = 1 by SIN_COS: 29;



 A2: (( cos ( PI / 3)) ^2 ) = (( cos ( PI / 3)) * ( cos ( PI / 3))) by SQUARE_1:def 1

 .= (1 / 4) by Thm8;

 ( sin ( PI / 3)) >= 0

 proof



 A3: (( PI / 2) - ( PI / 3)) in ]. 0 , ( PI / 2).[

 proof

 set n = (( PI / 2) - ( PI / 3));

 ( PI / 6) < ( PI / 2) by COMPTRIG: 5, XREAL_1: 76;

 hence thesis by COMPTRIG: 5, XXREAL_1: 4;

 end;

 ( sin ( PI / 3)) = ( cos (( PI / 2) - ( PI / 3))) by SIN_COS: 79;

 hence thesis by A3, SIN_COS: 81;

 end;

 then ( sin ( PI / 3)) = ( sqrt (3 / 4)) by A1, A2, SQUARE_1: 22;

 hence thesis by SQUARE_1: 20, SQUARE_1: 30;

 end;

 theorem :: EUCLID10:16



 Thm10: ( tan ( PI / 3)) = ( sqrt 3)

 proof

 ( tan ( PI / 3)) = ((( sqrt 3) / 2) / (1 / 2)) by Thm8, Thm9, SIN_COS4:def 1

 .= ( sqrt 3);

 hence thesis;

 end;

 theorem :: EUCLID10:17



 Thm11: ( sin ( PI / 6)) = (1 / 2)

 proof

 ( sin ( PI / 6)) = ( sin (( PI / 2) - ( PI / 3)))

 .= (1 / 2) by Thm8, SIN_COS: 79;

 hence thesis;

 end;

 theorem :: EUCLID10:18



 Thm12: ( cos ( PI / 6)) = (( sqrt 3) / 2)

 proof

 ( cos ( PI / 6)) = ( cos (( PI / 2) - ( PI / 3)))

 .= (( sqrt 3) / 2) by Thm9, SIN_COS: 79;

 hence thesis;

 end;

 theorem :: EUCLID10:19



 Thm13: ( tan ( PI / 6)) = (( sqrt 3) / 3)

 proof

 ( tan ( PI / 6)) = ((1 / 2) / (( sqrt 3) / 2)) by Thm11, Thm12, SIN_COS4:def 1

 .= (1 / ( sqrt 3)) by XCMPLX_1: 55;

 hence thesis by SQUARE_1: 33;

 end;

 theorem :: EUCLID10:20

 ( sin ( - ( PI / 6))) = ( - (1 / 2)) & ( cos ( - ( PI / 6))) = (( sqrt 3) / 2) & ( tan ( - ( PI / 6))) = ( - (( sqrt 3) / 3)) & ( sin ( - ( PI / 3))) = ( - (( sqrt 3) / 2)) & ( cos ( - ( PI / 3))) = (1 / 2) & ( tan ( - ( PI / 3))) = ( - ( sqrt 3)) by SIN_COS: 31, SIN_COS4: 1, Thm8, Thm9, Thm11, Thm12, Thm10, Thm13;

 theorem :: EUCLID10:21

 ( arcsin (1 / 2)) = ( PI / 6) & ( arcsin (( sqrt 3) / 2)) = ( PI / 3)

 proof

 ( PI / 6) < ( PI / 2) & ( PI / 3) < ( PI / 2) & ( - ( PI / 2)) <= ( PI / 6) & ( - ( PI / 2)) <= ( PI / 3) by XREAL_1: 76, COMPTRIG: 5;

 hence thesis by Thm9, Thm11, SIN_COS6: 69;

 end;

 theorem :: EUCLID10:22



 Thm14: ( sin ((2 * PI ) / 3)) = (( sqrt 3) / 2)

 proof

 ( sin ((2 * PI ) / 3)) = ( sin (((2 * PI ) / 3) - 0 ))

 .= ( sin (( PI / 3) + 0 )) by Thm5

 .= ( sin ( PI / 3));

 hence thesis by Thm9;

 end;

 theorem :: EUCLID10:23



 Thm15: ( cos ((2 * PI ) / 3)) = ( - (1 / 2))

 proof

 ( cos ((2 * PI ) / 3)) = ( cos (((2 * PI ) / 3) - 0 ))

 .= ( - ( cos (( PI / 3) + 0 ))) by Thm6

 .= ( - ( cos ( PI / 3)));

 hence thesis by Thm8;

 end;

 begin

 theorem :: EUCLID10:24



 Thm16: for x be Real holds (( sin ( - x)) ^2 ) = (( sin x) ^2 )

 proof

 let x be Real;

 (( sin ( - x)) ^2 ) = (( sin ( - x)) * ( sin ( - x))) by SQUARE_1:def 1

 .= (( - ( sin x)) * ( sin ( - x))) by SIN_COS: 31

 .= (( - ( sin x)) * ( - ( sin x))) by SIN_COS: 31

 .= (( sin x) * ( sin x));

 hence thesis by SQUARE_1:def 1;

 end;

 theorem :: EUCLID10:25



 Thm17: for x,y,z be Real st ((x + y) + z) = PI holds (((( sin x) ^2 ) + (( sin y) ^2 )) - (((2 * ( sin x)) * ( sin y)) * ( cos z))) = (( sin z) ^2 )

 proof

 let x,y,z be Real such that

 A1: ((x + y) + z) = PI ;

 ( sin ((x + y) - PI )) = ( - ( sin (x + y))) by COMPLEX2: 5;

 then ( - ( sin ((x + y) - PI ))) = ( sin (x + y));

 then

 A2: (( sin ( - ((x + y) - PI ))) ^2 ) = (( sin (x + y)) ^2 ) by SIN_COS: 31;



 A3: ((( cos y) ^2 ) + (( sin y) ^2 )) = 1 by SIN_COS: 29;



 A4: ((( cos x) ^2 ) + (( sin x) ^2 )) = 1 by SIN_COS: 29;



 A5: (( sin (x + y)) ^2 ) = (((( sin x) * ( cos y)) + (( cos x) * ( sin y))) ^2 ) by SIN_COS: 75

 .= ((((( sin x) * ( cos y)) ^2 ) + ((2 * (( sin x) * ( cos y))) * (( cos x) * ( sin y)))) + ((( cos x) * ( sin y)) ^2 )) by SQUARE_1: 4

 .= ((((( sin x) * ( cos y)) * (( sin x) * ( cos y))) + ((((2 * ( sin x)) * ( cos y)) * ( cos x)) * ( sin y))) + ((( cos x) * ( sin y)) ^2 )) by SQUARE_1:def 1

 .= ((((( sin x) * ( cos y)) * (( sin x) * ( cos y))) + ((((2 * ( sin x)) * ( cos y)) * ( cos x)) * ( sin y))) + ((( cos x) * ( sin y)) * (( cos x) * ( sin y)))) by SQUARE_1:def 1

 .= ((((( sin x) * ( sin x)) * (( cos y) * ( cos y))) + ((((2 * ( sin x)) * ( cos y)) * ( cos x)) * ( sin y))) + (((( cos x) * ( cos x)) * ( sin y)) * ( sin y)))

 .= ((((( sin x) ^2 ) * (( cos y) * ( cos y))) + ((((2 * ( sin x)) * ( cos y)) * ( cos x)) * ( sin y))) + (((( cos x) * ( cos x)) * ( sin y)) * ( sin y))) by SQUARE_1:def 1

 .= ((((( sin x) ^2 ) * (( cos y) ^2 )) + ((((2 * ( sin x)) * ( cos y)) * ( cos x)) * ( sin y))) + (((( cos x) * ( cos x)) * ( sin y)) * ( sin y))) by SQUARE_1:def 1

 .= ((((( sin x) ^2 ) * (( cos y) ^2 )) + ((((2 * ( sin x)) * ( cos y)) * ( cos x)) * ( sin y))) + (((( cos x) ^2 ) * ( sin y)) * ( sin y))) by SQUARE_1:def 1

 .= ((((( sin x) ^2 ) * (( cos y) ^2 )) + ((((2 * ( sin x)) * ( cos y)) * ( cos x)) * ( sin y))) + ((( cos x) ^2 ) * (( sin y) * ( sin y))))

 .= ((((( sin x) ^2 ) * (( cos y) ^2 )) + ((((2 * ( sin x)) * ( cos y)) * ( cos x)) * ( sin y))) + ((( cos x) ^2 ) * (( sin y) ^2 ))) by SQUARE_1:def 1;

 (((( sin x) ^2 ) + (( sin y) ^2 )) - (((2 * ( sin x)) * ( sin y)) * ( cos z))) = (((( sin x) ^2 ) + (( sin y) ^2 )) - (((2 * ( sin x)) * ( sin y)) * ( cos ( - ((x + y) - PI ))))) by A1

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) - (((2 * ( sin x)) * ( sin y)) * ( cos ((x + y) - PI )))) by SIN_COS: 31

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) - (((2 * ( sin x)) * ( sin y)) * ( - ( cos (x + y))))) by COMPLEX2: 5

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin y)) * ( cos (x + y))))

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin y)) * ((( cos x) * ( cos y)) - (( sin x) * ( sin y))))) by SIN_COS: 75

 .= ((((( sin x) ^2 ) + (( sin y) ^2 )) + ((((2 * ( sin x)) * ( sin y)) * ( cos x)) * ( cos y))) - (((2 * (( sin x) * ( sin x))) * ( sin y)) * ( sin y)))

 .= ((((( sin x) ^2 ) + (( sin y) ^2 )) + ((((2 * ( sin x)) * ( sin y)) * ( cos x)) * ( cos y))) - (((2 * (( sin x) ^2 )) * ( sin y)) * ( sin y))) by SQUARE_1:def 1

 .= ((((( sin x) ^2 ) + (( sin y) ^2 )) + ((((2 * ( sin x)) * ( sin y)) * ( cos x)) * ( cos y))) - ((2 * (( sin x) ^2 )) * (( sin y) * ( sin y))))

 .= ((((( sin x) ^2 ) + (( sin y) ^2 )) + ((((2 * ( sin x)) * ( sin y)) * ( cos x)) * ( cos y))) - ((2 * (( sin x) ^2 )) * (( sin y) ^2 ))) by SQUARE_1:def 1

 .= (((((( sin x) ^2 ) * (1 - (( sin y) ^2 ))) + (( sin y) ^2 )) + ((((2 * ( sin x)) * ( sin y)) * ( cos x)) * ( cos y))) - ((( sin x) ^2 ) * (( sin y) ^2 )))

 .= ((((( sin x) ^2 ) * (( cos y) ^2 )) + ((( sin y) ^2 ) * (1 - (( sin x) ^2 )))) + ((((2 * ( sin x)) * ( sin y)) * ( cos x)) * ( cos y))) by A3

 .= ((((( sin x) ^2 ) * (( cos y) ^2 )) + ((( sin y) ^2 ) * (( cos x) ^2 ))) + ((((2 * ( sin x)) * ( sin y)) * ( cos x)) * ( cos y))) by A4;

 hence thesis by A1, A2, A5;

 end;

 theorem :: EUCLID10:26

 for x,y,z be Real st ((x - y) + z) = PI holds (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin y)) * ( cos z))) = (( sin z) ^2 )

 proof

 let x,y,z be Real;

 assume ((x - y) + z) = PI ;

 then

 A1: ((x + ( - y)) + z) = PI ;

 (((( sin x) ^2 ) + (( sin ( - y)) ^2 )) - (((2 * ( sin x)) * ( sin ( - y))) * ( cos z))) = (((( sin x) ^2 ) + (( sin ( - y)) ^2 )) - (((2 * ( sin x)) * ( - ( sin y))) * ( cos z))) by SIN_COS: 31

 .= (((( sin x) ^2 ) + (( sin ( - y)) ^2 )) + (((2 * ( sin x)) * ( sin y)) * ( cos z)))

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin y)) * ( cos z))) by Thm16;

 hence thesis by A1, Thm17;

 end;

 theorem :: EUCLID10:27

 for x,y,z be Real st ((x - (( - (2 * PI )) + y)) + z) = PI holds (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin y)) * ( cos z))) = (( sin z) ^2 )

 proof

 let x,y,z be Real;

 assume ((x - (( - (2 * PI )) + y)) + z) = PI ;

 then

 A1: ((x + ( - (( - (2 * PI )) + y))) + z) = PI ;

 (((( sin x) ^2 ) + (( sin ( - (( - (2 * PI )) + y))) ^2 )) - (((2 * ( sin x)) * ( sin ( - (( - (2 * PI )) + y)))) * ( cos z))) = (((( sin x) ^2 ) + (( sin ( - (( - (2 * PI )) + y))) ^2 )) - (((2 * ( sin x)) * ( - ( sin (( - (2 * PI )) + y)))) * ( cos z))) by SIN_COS: 31

 .= (((( sin x) ^2 ) + (( sin ( - (( - (2 * PI )) + y))) ^2 )) + (((2 * ( sin x)) * ( sin (( - (2 * PI )) + y))) * ( cos z)))

 .= (((( sin x) ^2 ) + (( sin (( - (2 * PI )) + y)) ^2 )) + (((2 * ( sin x)) * ( sin (( - (2 * PI )) + y))) * ( cos z))) by Thm16

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin (( - (2 * PI )) + y))) * ( cos z))) by Thm2

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin y)) * ( cos z))) by Thm2;

 hence thesis by A1, Thm17;

 end;

 theorem :: EUCLID10:28

 for x,y,z be Real st ((( PI - x) - ( PI - y)) + z) = PI holds (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin y)) * ( cos z))) = (( sin z) ^2 )

 proof

 let x,y,z be Real;

 assume ((( PI - x) - ( PI - y)) + z) = PI ;

 then

 A1: ((( PI - x) + ( - ( PI - y))) + z) = PI ;

 (((( sin ( PI - x)) ^2 ) + (( sin ( - ( PI - y))) ^2 )) - (((2 * ( sin ( PI - x))) * ( sin ( - ( PI - y)))) * ( cos z))) = (((( sin ( PI - x)) ^2 ) + (( sin ( - ( PI - y))) ^2 )) - (((2 * ( sin ( PI - x))) * ( - ( sin ( PI - y)))) * ( cos z))) by SIN_COS: 31

 .= (((( sin ( PI - x)) ^2 ) + (( sin ( - ( PI - y))) ^2 )) + (((2 * ( sin ( PI - x))) * ( sin ( PI - y))) * ( cos z)))

 .= (((( sin ( PI - x)) ^2 ) + (( sin ( PI - y)) ^2 )) + (((2 * ( sin ( PI - x))) * ( sin ( PI - y))) * ( cos z))) by Thm16

 .= (((( sin x) ^2 ) + (( sin ( PI - y)) ^2 )) + (((2 * ( sin ( PI - x))) * ( sin ( PI - y))) * ( cos z))) by Thm1

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin ( PI - x))) * ( sin ( PI - y))) * ( cos z))) by Thm1

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin ( PI - y))) * ( cos z))) by Thm1

 .= (((( sin x) ^2 ) + (( sin y) ^2 )) + (((2 * ( sin x)) * ( sin y)) * ( cos z))) by Thm1;

 hence thesis by A1, Thm17;

 end;

 theorem :: EUCLID10:29



 Thm18: for a be Real holds ( sin (3 * a)) = (((4 * ( sin a)) * ( sin (( PI / 3) + a))) * ( sin (( PI / 3) - a)))

 proof

 let a be Real;



 A1: ((( sqrt 3) / 2) ^2 ) = ((( sqrt 3) / 2) * (( sqrt 3) / 2)) by SQUARE_1:def 1

 .= (((( sqrt 3) * ( sqrt 3)) / 2) / 2)

 .= ((( sqrt (3 * 3)) / 2) / 2) by SQUARE_1: 29

 .= ((( sqrt (3 ^2 )) / 2) / 2) by SQUARE_1:def 1

 .= ((3 / 2) / 2) by SQUARE_1: 22

 .= (3 / 4);

 ( sin (3 * a)) = (( - (4 * (( sin a) |^ 3))) + (3 * ( sin a))) by SIN_COS5: 16

 .= ((((4 * ( sin a)) * 3) / 4) - (4 * (( sin a) |^ (2 + 1))))

 .= ((((4 * ( sin a)) * 3) / 4) - (4 * ((( sin a) |^ 2) * ( sin a)))) by NEWTON: 6

 .= ((4 * ( sin a)) * (((( sqrt 3) / 2) ^2 ) - (( sin a) |^ 2))) by A1

 .= ((4 * ( sin a)) * ((( sin ( PI / 3)) ^2 ) - (( sin a) ^2 ))) by Thm9, NEWTON: 81

 .= ((4 * ( sin a)) * ((( sin ( PI / 3)) - ( sin a)) * (( sin ( PI / 3)) + ( sin a)))) by SQUARE_1: 8

 .= (((4 * ( sin a)) * (( sin ( PI / 3)) + ( sin a))) * (( sin ( PI / 3)) - ( sin a)))

 .= (((4 * ( sin a)) * (2 * (( cos ((( PI / 3) - a) / 2)) * ( sin ((( PI / 3) + a) / 2))))) * (( sin ( PI / 3)) - ( sin a))) by SIN_COS4: 15

 .= (((4 * ( sin a)) * (2 * (( cos ((( PI / 3) - a) / 2)) * ( sin ((( PI / 3) + a) / 2))))) * (2 * (( cos ((( PI / 3) + a) / 2)) * ( sin ((( PI / 3) - a) / 2))))) by SIN_COS4: 16

 .= (((4 * ( sin a)) * ((2 * ( sin ((( PI / 3) - a) / 2))) * ( cos ((( PI / 3) - a) / 2)))) * ((2 * ( sin ((( PI / 3) + a) / 2))) * ( cos ((( PI / 3) + a) / 2))))

 .= (((4 * ( sin a)) * ( sin (2 * ((( PI / 3) - a) / 2)))) * ((2 * ( sin ((( PI / 3) + a) / 2))) * ( cos ((( PI / 3) + a) / 2)))) by SIN_COS5: 5

 .= (((4 * ( sin a)) * ( sin (2 * ((( PI / 3) - a) / 2)))) * ( sin (2 * ((( PI / 3) + a) / 2)))) by SIN_COS5: 5

 .= (((4 * ( sin a)) * ( sin (( PI / 3) - a))) * ( sin (( PI / 3) + a)));

 hence thesis;

 end;

 begin



 Lm7: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds ( angle (A,B,C)) <> 0

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume

 A1: (A,B,C) is_a_triangle ;

 then

 A2: (A,B,C) are_mutually_distinct by EUCLID_6: 20;

 now

 assume ( angle (A,B,C)) = 0 ;

 then ( angle (B,C,A)) = PI or ( angle (B,A,C)) = PI by A2, MENELAUS: 8;

 then C in ( LSeg (B,A)) or A in ( LSeg (B,C)) by EUCLID_6: 11;

 hence contradiction by A1, TOPREAL9: 67;

 end;

 hence thesis;

 end;

 theorem :: EUCLID10:30



 Thm19: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds ( angle (A,B,C)) is non zero & ( angle (B,C,A)) is non zero & ( angle (C,A,B)) is non zero & ( angle (A,C,B)) is non zero & ( angle (C,B,A)) is non zero & ( angle (B,A,C)) is non zero

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume

 A1: (A,B,C) is_a_triangle ;

 then (B,C,A) is_a_triangle & (C,A,B) is_a_triangle & (B,A,C) is_a_triangle & (A,C,B) is_a_triangle & (C,B,A) is_a_triangle by MENELAUS: 15;

 hence thesis by A1, Lm7;

 end;



 Lm9: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds ( angle (A,B,C)) = ((2 * PI ) - ( angle (C,B,A))) & ( angle (C,B,A)) = ((2 * PI ) - ( angle (A,B,C)))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume (A,B,C) is_a_triangle ;

 then ( angle (A,B,C)) <> 0 by Thm19;

 hence ( angle (A,B,C)) = ((2 * PI ) - ( angle (C,B,A))) by EUCLID_3: 38;

 hence thesis;

 end;

 theorem :: EUCLID10:31



 Thm20: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds ( angle (A,B,C)) = ((2 * PI ) - ( angle (C,B,A))) & ( angle (B,C,A)) = ((2 * PI ) - ( angle (A,C,B))) & ( angle (C,A,B)) = ((2 * PI ) - ( angle (B,A,C))) & ( angle (B,A,C)) = ((2 * PI ) - ( angle (C,A,B))) & ( angle (A,C,B)) = ((2 * PI ) - ( angle (B,C,A))) & ( angle (C,B,A)) = ((2 * PI ) - ( angle (A,B,C)))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume (A,B,C) is_a_triangle ;

 then (B,C,A) is_a_triangle & (C,A,B) is_a_triangle & (B,A,C) is_a_triangle & (A,C,B) is_a_triangle & (C,B,A) is_a_triangle by MENELAUS: 15;

 hence thesis by Lm9;

 end;

 theorem :: EUCLID10:32

 for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle & |((B - A), (C - A))| = 0 holds ( |.(C - B).| * ( sin ( angle (C,B,A)))) = |.(A - C).| or ( |.(C - B).| * ( - ( sin ( angle (C,B,A))))) = |.(A - C).|

 proof

 let A,B,C be Point of ( TOP-REAL 2) such that

 A1: (A,B,C) is_a_triangle and

 A2: |((B - A), (C - A))| = 0 ;



 A3: (A,B,C) are_mutually_distinct by A1, EUCLID_6: 20;

 then

 A4: ( |.(C - B).| * ( sin ( angle (C,B,A)))) = ( |.(C - A).| * ( sin ( angle (B,A,C)))) by EUCLID_6: 6;

 ( sin ( angle (B,A,C))) = 1 or ( sin ( angle (B,A,C))) = ( - 1) by A2, A3, SIN_COS: 77, EUCLID_3: 45;

 hence thesis by A4, EUCLID_6: 43;

 end;

 theorem :: EUCLID10:33

 for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle & ( angle (B,A,C)) = ( PI / 2) holds (( angle (C,B,A)) + ( angle (A,C,B))) = ( PI / 2)

 proof

 let A,B,C be Point of ( TOP-REAL 2) such that

 A1: (A,B,C) is_a_triangle and

 A2: ( angle (B,A,C)) = ( PI / 2);



 A3: (A,B,C) are_mutually_distinct by A1, EUCLID_6: 20;

 ((( angle (B,A,C)) + ( angle (A,C,B))) + ( angle (C,B,A))) = PI by A2, COMPTRIG: 5, A3, EUCLID_3: 47;

 hence thesis by A2;

 end;

 theorem :: EUCLID10:34



 Thm21: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle & ( angle (B,A,C)) = ( PI / 2) holds ( |.(C - B).| * ( sin ( angle (C,B,A)))) = |.(A - C).| & ( |.(C - B).| * ( sin ( angle (A,C,B)))) = |.(A - B).| & ( |.(C - B).| * ( cos ( angle (C,B,A)))) = |.(A - B).| & ( |.(C - B).| * ( cos ( angle (A,C,B)))) = |.(A - C).|

 proof

 let A,B,C be Point of ( TOP-REAL 2) such that

 A1: (A,B,C) is_a_triangle and

 A2: ( angle (B,A,C)) = ( PI / 2);



 A3: (A,B,C) are_mutually_distinct by A1, EUCLID_6: 20;

 then

 A4: ( |.(C - B).| * ( sin ( angle (C,B,A)))) = ( |.(C - A).| * ( sin ( angle (B,A,C)))) by EUCLID_6: 6;



 A5: ( |.(B - A).| * ( sin ( angle (B,A,C)))) = ( |.(B - C).| * ( sin ( angle (A,C,B)))) by A3, EUCLID_6: 6;

 thus

 A6: ( |.(C - B).| * ( sin ( angle (C,B,A)))) = |.(A - C).| by A2, A4, SIN_COS: 77, EUCLID_6: 43;

 ( |.(A - B).| * ( sin ( angle (B,A,C)))) = ( |.(B - C).| * ( sin ( angle (A,C,B)))) by A5, EUCLID_6: 43;

 hence

 A7: ( |.(C - B).| * ( sin ( angle (A,C,B)))) = |.(A - B).| by A2, SIN_COS: 77, EUCLID_6: 43;

 ((( angle (B,A,C)) + ( angle (A,C,B))) + ( angle (C,B,A))) = PI by A2, A3, COMPTRIG: 5, EUCLID_3: 47;

 then ( sin ( angle (A,C,B))) = ( sin (( PI / 2) - ( angle (C,B,A)))) by A2;

 hence ( |.(C - B).| * ( cos ( angle (C,B,A)))) = |.(A - B).| by A7, SIN_COS: 79;

 ((( angle (B,A,C)) + ( angle (A,C,B))) + ( angle (C,B,A))) = PI by A2, A3, COMPTRIG: 5, EUCLID_3: 47;

 then ( sin ( angle (C,B,A))) = ( sin (( PI / 2) - ( angle (A,C,B)))) by A2;

 hence ( |.(C - B).| * ( cos ( angle (A,C,B)))) = |.(A - C).| by A6, SIN_COS: 79;

 end;

 theorem :: EUCLID10:35

 for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle & ( angle (B,A,C)) = ( PI / 2) holds ( tan ( angle (A,C,B))) = ( |.(A - B).| / |.(A - C).|) & ( tan ( angle (C,B,A))) = ( |.(A - C).| / |.(A - B).|)

 proof

 let A,B,C be Point of ( TOP-REAL 2) such that

 A1: (A,B,C) is_a_triangle and

 A2: ( angle (B,A,C)) = ( PI / 2);



 A3: (A,B,C) are_mutually_distinct by A1, EUCLID_6: 20;

 ( |.(C - B).| * ( sin ( angle (A,C,B)))) = |.(A - B).| & ( |.(C - B).| * ( cos ( angle (A,C,B)))) = |.(A - C).| by A1, A2, Thm21;

 then ((( |.(C - B).| / |.(C - B).|) * ( sin ( angle (A,C,B)))) / ( cos ( angle (A,C,B)))) = ( |.(A - B).| / |.(A - C).|) by XCMPLX_1: 83;

 then

 A4: ((1 * ( sin ( angle (A,C,B)))) / ( cos ( angle (A,C,B)))) = ( |.(A - B).| / |.(A - C).|) by A3, EUCLID_6: 42, XCMPLX_1: 60;

 hence ( tan ( angle (A,C,B))) = ( |.(A - B).| / |.(A - C).|) by SIN_COS4:def 1;

 ((( angle (B,A,C)) + ( angle (A,C,B))) + ( angle (C,B,A))) = PI by A2, A3, COMPTRIG: 5, EUCLID_3: 47;



 then ( tan ( angle (C,B,A))) = (( sin (( PI / 2) - ( angle (A,C,B)))) / ( cos (( PI / 2) - ( angle (A,C,B))))) by A2, SIN_COS4:def 1

 .= (( cos ( angle (A,C,B))) / ( cos (( PI / 2) - ( angle (A,C,B))))) by SIN_COS: 79

 .= (( cos ( angle (A,C,B))) / ( sin ( angle (A,C,B)))) by SIN_COS: 79

 .= (1 / (( sin ( angle (A,C,B))) / ( cos ( angle (A,C,B))))) by XCMPLX_1: 57

 .= ( |.(A - C).| / |.(A - B).|) by A4, XCMPLX_1: 57;

 hence thesis;

 end;

 begin

 registration

 let a,b be Real, r be negative Real;

 cluster ( circle (a,b,r)) -> empty;

 coherence

 proof

 ( circle (a,b,r)) = ( Sphere ( |[a, b]|,r)) by TOPREAL9: 52;

 hence thesis;

 end;

 end

 theorem :: EUCLID10:36



 Thm23: for a,b be Real holds ( circle (a,b, 0 )) = { |[a, b]|}

 proof

 let a,b be Real;

 now

 hereby

 let t be object;

 assume t in { p where p be Point of ( TOP-REAL 2) : |.(p - |[a, b]|).| = 0 };

 then

 consider p0 be Point of ( TOP-REAL 2) such that

 A1: t = p0 and

 A2: |.(p0 - |[a, b]|).| = 0 ;

 p0 = |[a, b]| by A2, EUCLID_6: 42;

 hence t in { |[a, b]|} by A1, TARSKI:def 1;

 end;

 let t be object;

 assume

 A3: t in { |[a, b]|};

 then

 A4: t = |[a, b]| by TARSKI:def 1;

 reconsider p0 = t as Point of ( TOP-REAL 2) by A3, TARSKI:def 1;

 |.(p0 - |[a, b]|).| = 0 by A4, EUCLID_6: 42;

 hence t in { p where p be Point of ( TOP-REAL 2) : |.(p - |[a, b]|).| = 0 };

 end;

 then { p where p be Point of ( TOP-REAL 2) : |.(p - |[a, b]|).| = 0 } c= { |[a, b]|} & { |[a, b]|} c= { p where p be Point of ( TOP-REAL 2) : |.(p - |[a, b]|).| = 0 };

 hence thesis by JGRAPH_6:def 5;

 end;

 registration

 let a,b be Real;

 cluster ( circle (a,b, 0 )) -> trivial;

 coherence

 proof

 ( circle (a,b, 0 )) = { |[a, b]|} by Thm23;

 hence thesis;

 end;

 end

 theorem :: EUCLID10:37



 Thm24: for A,B,C be Point of ( TOP-REAL 2), a,b,r be Real st (A,B,C) is_a_triangle & A in ( circle (a,b,r)) & B in ( circle (a,b,r)) holds r is positive

 proof

 let A,B,C be Point of ( TOP-REAL 2), a,b,r be Real such that

 A1: (A,B,C) is_a_triangle and

 A2: A in ( circle (a,b,r)) & B in ( circle (a,b,r));



 A3: (A,B,C) are_mutually_distinct by A1, EUCLID_6: 20;

 assume not r is positive;

 per cases ;

 suppose r < 0 ;

 hence contradiction by A2;

 end;

 suppose r = 0 ;

 then A in { |[a, b]|} & B in { |[a, b]|} by A2, Thm23;

 then A = |[a, b]| & B = |[a, b]| by TARSKI:def 1;

 hence contradiction by A3;

 end;

 end;

 theorem :: EUCLID10:38



 Thm25: for A be Point of ( TOP-REAL 2), a,b be Real, r be positive Real st A in ( circle (a,b,r)) holds A <> |[a, b]|

 proof

 let A be Point of ( TOP-REAL 2), a,b be Real, r be positive Real such that

 A1: A in ( circle (a,b,r));

 ( circle (a,b,r)) = { p where p be Point of ( TOP-REAL 2) : |.(p - |[a, b]|).| = r } by JGRAPH_6:def 5;

 then

 consider p0 be Point of ( TOP-REAL 2) such that

 A2: A = p0 and

 A3: |.(p0 - |[a, b]|).| = r by A1;

 thus thesis by A2, A3, EUCLID_6: 42;

 end;

 theorem :: EUCLID10:39

 for A,B,C be Point of ( TOP-REAL 2), a,b,r be Real st (A,B,C) is_a_triangle & ( angle (C,B,A)) in ]. 0 , PI .[ & ( angle (B,A,C)) in ]. 0 , PI .[ & A in ( circle (a,b,r)) & B in ( circle (a,b,r)) & C in ( circle (a,b,r)) & |[a, b]| in ( LSeg (A,C)) holds ( angle (C,B,A)) = ( PI / 2)

 proof

 let A,B,C be Point of ( TOP-REAL 2), a,b,r be Real such that

 A1: (A,B,C) is_a_triangle and

 A2: ( angle (C,B,A)) in ]. 0 , PI .[ and

 A3: ( angle (B,A,C)) in ]. 0 , PI .[ and

 A4: A in ( circle (a,b,r)) & B in ( circle (a,b,r)) & C in ( circle (a,b,r)) and

 A5: |[a, b]| in ( LSeg (A,C));



 A6: (A,B,C) are_mutually_distinct by A1, EUCLID_6: 20;

 set O = |[a, b]|;



 A7: ( angle (C,B,A)) > 0 & ( angle (C,B,A)) < PI by A2, XXREAL_1: 4;



 A8: ( angle (B,A,C)) > 0 & ( angle (B,A,C)) < PI by A3, XXREAL_1: 4;



 A9: ( circle (a,b,r)) = { p where p be Point of ( TOP-REAL 2) : |.(p - |[a, b]|).| = r } by JGRAPH_6:def 5;

 consider JA be Point of ( TOP-REAL 2) such that

 A10: A = JA and

 A11: |.(JA - |[a, b]|).| = r by A4, A9;

 consider JB be Point of ( TOP-REAL 2) such that

 A12: B = JB and

 A13: |.(JB - |[a, b]|).| = r by A4, A9;

 consider JC be Point of ( TOP-REAL 2) such that

 A14: C = JC and

 A15: |.(JC - |[a, b]|).| = r by A4, A9;

 r is positive by A1, A4, Thm24;

 then

 A16: O <> A & O <> C by A4, Thm25;



 A17: ( angle (C,B,A)) < PI by A2, XXREAL_1: 4;



 A18: |.(B - O).| = |.(O - C).| & B <> C by A12, A13, A14, A15, A6, EUCLID_6: 43;



 A19: ( angle (C,B,O)) < PI

 proof

 assume ( angle (C,B,O)) >= PI ;

 then ( angle (O,C,B)) >= PI by A18, EUCLID_6: 16;

 then

 A20: ( angle (A,C,B)) >= PI by A5, A16, EUCLID_6: 9;

 ((( angle (C,B,A)) + ( angle (B,A,C))) + ( angle (A,C,B))) = PI by A17, A6, EUCLID_3: 47;

 then

 A21: (( angle (C,B,A)) + ( angle (B,A,C))) = ( PI - ( angle (A,C,B)));

 ( angle (B,A,C)) <= 0

 proof

 assume

 A22: ( angle (B,A,C)) > 0 ;

 ( angle (C,B,A)) > 0 by A2, XXREAL_1: 4;

 hence contradiction by A21, A20, A22, XREAL_1: 47;

 end;

 hence contradiction by A3, XXREAL_1: 4;

 end;



 A23: (A,O,B) is_a_triangle & (C,O,B) is_a_triangle

 proof



 A23a: r is positive by A1, A4, Thm24;

 then

 A24: O <> B & O <> A & O <> C by A4, Thm25;

 not A in ( Line (O,B))

 proof

 assume

 A25: A in ( Line (O,B));

 B in ( Line (O,B)) by RLTOPSP1: 72;

 then ( Line (A,B)) = ( Line (O,B)) by A6, A25, RLTOPSP1: 75;

 then O in ( Line (A,B)) & A in ( Line (A,B)) by RLTOPSP1: 72;

 then

 A26: ( Line (O,A)) = ( Line (A,B)) by A4, A23a, Thm25, RLTOPSP1: 75;

 O in ( Line (A,C)) & A in ( Line (A,C)) by A5, MENELAUS: 12, RLTOPSP1: 72;

 then ( Line (O,A)) = ( Line (A,C)) by A4, A23a, Thm25, RLTOPSP1: 75;

 then A in ( Line (A,B)) & B in ( Line (A,B)) & C in ( Line (A,B)) by A26, RLTOPSP1: 72;

 hence contradiction by A1, RLTOPSP1:def 16;

 end;

 hence (A,O,B) is_a_triangle by A24, MENELAUS: 13;

 not (C,O,B) are_collinear

 proof

 assume

 A28: (C,O,B) are_collinear ;

 then C in ( Line (O,B)) & B in ( Line (O,B)) by A24, MENELAUS: 13, RLTOPSP1: 72;

 then

 A29: ( Line (C,B)) = ( Line (O,B)) by A6, RLTOPSP1: 75;

 C in ( Line (O,B)) & O in ( Line (O,B)) & O <> C by A28, A24, MENELAUS: 13, RLTOPSP1: 72;

 then

 A30: ( Line (C,O)) = ( Line (O,B)) by RLTOPSP1: 75;



 A31: O in ( Line (A,C)) & A in ( Line (A,C)) & C in ( Line (C,A)) by A5, MENELAUS: 12, RLTOPSP1: 72;

 then ( Line (C,O)) = ( Line (A,C)) by A4, A23a, Thm25, RLTOPSP1: 75;

 hence contradiction by A30, A31, A29, A1, A6, MENELAUS: 13;

 end;

 hence (C,O,B) is_a_triangle ;

 end;

 then

 A32: (A,O,B) are_mutually_distinct & (C,O,B) are_mutually_distinct by EUCLID_6: 20;

 then ( angle (B,A,O)) < PI by A8, A5, EUCLID_6: 10;

 then

 A33: ((( angle (B,A,O)) + ( angle (A,O,B))) + ( angle (O,B,A))) = PI by A32, EUCLID_3: 47;

 |.(O - A).| = |.(B - O).| by A10, A11, A12, A13, EUCLID_6: 43;

 then

 A34: ( angle (O,A,B)) = ( angle (A,B,O)) by A6, EUCLID_6: 16;

 |.(O - B).| = |.(C - O).| by A12, A13, A14, A15, EUCLID_6: 43;

 then

 A35: ( angle (O,B,C)) = ( angle (B,C,O)) by A6, EUCLID_6: 16;



 A36: (((( angle (C,B,O)) + ( angle (O,C,B))) + ( angle (O,B,A))) + ( angle (B,A,O))) = PI or (((( angle (C,B,O)) + ( angle (O,C,B))) + ( angle (O,B,A))) + ( angle (B,A,O))) = ( - PI )

 proof



 A37: (( angle (A,O,B)) + ( angle (B,O,C))) = PI or (( angle (A,O,B)) + ( angle (B,O,C))) = (3 * PI ) by A32, A5, EUCLID_6: 13;

 ((( angle (C,B,O)) + ( angle (B,O,C))) + ( angle (O,C,B))) = PI by A19, A32, EUCLID_3: 47;

 hence thesis by A33, A37;

 end;

 ( angle (O,C,B)) = ( angle (C,B,O)) & ( angle (B,A,O)) = ( angle (O,B,A))

 proof

 ((2 * PI ) - ( angle (C,B,O))) = ( angle (O,B,C)) & ((2 * PI ) - ( angle (O,C,B))) = ( angle (B,C,O)) by A23, Thm20;

 hence ( angle (O,C,B)) = ( angle (C,B,O)) by A35;

 ((2 * PI ) - ( angle (O,B,A))) = ( angle (A,B,O)) & ((2 * PI ) - ( angle (O,A,B))) = ( angle (B,A,O)) by A23, Thm20;

 hence thesis by A34;

 end;

 then (( angle (C,B,O)) + ( angle (O,B,A))) = ( PI / 2) or (( angle (C,B,O)) + ( angle (O,B,A))) = ( - ( PI / 2)) by A36;

 then ( angle (C,B,A)) = ( PI / 2) or (( angle (C,B,A)) + (2 * PI )) = ( PI / 2) or ( angle (C,B,A)) = ( - ( PI / 2)) or (( angle (C,B,A)) + (2 * PI )) = ( - ( PI / 2)) by EUCLID_6: 4;

 then ( angle (C,B,A)) = ( PI / 2) or ( angle (C,B,A)) = ( - ((3 * PI ) / 2)) or ( angle (C,B,A)) = ( - ( PI / 2)) or ( angle (C,B,A)) = ( - ((5 * PI ) / 2));

 hence thesis by A7;

 end;

 theorem :: EUCLID10:40



 Thm26: for A,B,C be Point of ( TOP-REAL 2), r be positive Real st ( angle (A,B,C)) is non zero holds ( sin (r * ( angle (C,B,A)))) = ((( sin ((r * 2) * PI )) * ( cos (r * ( angle (A,B,C))))) - (( cos ((r * 2) * PI )) * ( sin (r * ( angle (A,B,C))))))

 proof

 let A,B,C be Point of ( TOP-REAL 2), r be positive Real;

 assume ( angle (A,B,C)) is non zero;

 then ( angle (C,B,A)) = ((2 * PI ) - ( angle (A,B,C))) by EUCLID_3: 37;

 then (r * ( angle (C,B,A))) = (((r * 2) * PI ) - (r * ( angle (A,B,C))));

 hence thesis by SIN_COS: 82;

 end;

 theorem :: EUCLID10:41

 for A,B,C be Point of ( TOP-REAL 2) st ( angle (A,B,C)) is non zero holds ( sin (( angle (C,B,A)) / 3)) = (((( sqrt 3) / 2) * ( cos (( angle (A,B,C)) / 3))) + ((1 / 2) * ( sin (( angle (A,B,C)) / 3))))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume ( angle (A,B,C)) is non zero;



 then ( sin ((1 / 3) * ( angle (C,B,A)))) = ((( sin ((2 * PI ) / 3)) * ( cos ((1 / 3) * ( angle (A,B,C))))) - (( cos (((1 / 3) * 2) * PI )) * ( sin ((1 / 3) * ( angle (A,B,C)))))) by Thm26

 .= (((( sqrt 3) / 2) * ( cos (( angle (A,B,C)) / 3))) + ((1 / 2) * ( sin (( angle (A,B,C)) / 3)))) by Thm14, Thm15;

 hence thesis;

 end;

 begin

 theorem :: EUCLID10:42



 Thm27: for A,B,C be Point of ( TOP-REAL 2) holds ( the_area_of_polygon3 (A,B,C)) = ( the_area_of_polygon3 (B,C,A)) & ( the_area_of_polygon3 (A,B,C)) = ( the_area_of_polygon3 (C,A,B))

 proof

 let A,B,C be Point of ( TOP-REAL 2);



 A1: ( the_area_of_polygon3 (A,B,C)) = ((((((A `1 ) * (B `2 )) - ((B `1 ) * (A `2 ))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * (A `2 )) - ((A `1 ) * (C `2 )))) / 2) by EUCLID_6:def 1;

 ( the_area_of_polygon3 (B,C,A)) = ((((((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 ))) + (((C `1 ) * (A `2 )) - ((A `1 ) * (C `2 )))) + (((A `1 ) * (B `2 )) - ((B `1 ) * (A `2 )))) / 2) by EUCLID_6:def 1;

 hence ( the_area_of_polygon3 (A,B,C)) = ( the_area_of_polygon3 (B,C,A)) by A1;

 ( the_area_of_polygon3 (C,A,B)) = ((((((C `1 ) * (A `2 )) - ((A `1 ) * (C `2 ))) + (((A `1 ) * (B `2 )) - ((B `1 ) * (A `2 )))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) / 2) by EUCLID_6:def 1;

 hence thesis by A1;

 end;

 theorem :: EUCLID10:43



 Thm28: for A,B,C be Point of ( TOP-REAL 2) holds ( the_area_of_polygon3 (A,B,C)) = ( - ( the_area_of_polygon3 (B,A,C)))

 proof

 let A,B,C be Point of ( TOP-REAL 2);



 A1: ( the_area_of_polygon3 (A,B,C)) = ((((((A `1 ) * (B `2 )) - ((B `1 ) * (A `2 ))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * (A `2 )) - ((A `1 ) * (C `2 )))) / 2) by EUCLID_6:def 1;

 ( the_area_of_polygon3 (B,A,C)) = ((((((B `1 ) * (A `2 )) - ((A `1 ) * (B `2 ))) + (((A `1 ) * (C `2 )) - ((C `1 ) * (A `2 )))) + (((C `1 ) * (B `2 )) - ((B `1 ) * (C `2 )))) / 2) by EUCLID_6:def 1;

 hence thesis by A1;

 end;

 definition

 let A,B,C be Point of ( TOP-REAL 2);

 :: EUCLID10:def1

 func the_diameter_of_the_circumcircle (A,B,C) -> Real equals (((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / ( the_area_of_polygon3 (A,B,C)));

 correctness ;

 end

 theorem :: EUCLID10:44



 Thm29: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds ( the_diameter_of_the_circumcircle (A,B,C)) = ( |.(C - A).| / ( sin ( angle (C,B,A))))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume (A,B,C) is_a_triangle ;

 then

 A2: (A,B,C) are_mutually_distinct by EUCLID_6: 20;

 ( the_diameter_of_the_circumcircle (A,B,C)) = (((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / ((( |.(A - B).| * |.(C - B).|) * ( sin ( angle (C,B,A)))) / 2)) by EUCLID_6: 5

 .= (((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / ((1 / 2) * (( |.(A - B).| * |.(C - B).|) * ( sin ( angle (C,B,A))))))

 .= ((((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (1 / 2)) / ( |.(A - B).| * ( |.(C - B).| * ( sin ( angle (C,B,A)))))) by XCMPLX_1: 78

 .= (((((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (1 / 2)) / |.(A - B).|) / ( |.(C - B).| * ( sin ( angle (C,B,A))))) by XCMPLX_1: 78

 .= (((( |.(A - B).| * ( |.(B - C).| * |.(C - A).|)) / |.(A - B).|) / |.(C - B).|) / ( sin ( angle (C,B,A)))) by XCMPLX_1: 78

 .= ((( |.(B - C).| * |.(C - A).|) / |.(C - B).|) / ( sin ( angle (C,B,A)))) by XCMPLX_1: 89, A2, EUCLID_6: 42

 .= ((( |.(B - C).| * |.(C - A).|) / |.(B - C).|) / ( sin ( angle (C,B,A)))) by EUCLID_6: 43

 .= ( |.(C - A).| / ( sin ( angle (C,B,A)))) by XCMPLX_1: 89, A2, EUCLID_6: 42;

 hence thesis;

 end;

 theorem :: EUCLID10:45

 for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds ( the_diameter_of_the_circumcircle (A,B,C)) = ( - ( |.(C - A).| / ( sin ( angle (A,B,C)))))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume (A,B,C) is_a_triangle ;



 then ( the_diameter_of_the_circumcircle (A,B,C)) = ( |.(C - A).| / ( sin ( angle (C,B,A)))) by Thm29

 .= ( |.(C - A).| / ( - ( sin ( angle (A,B,C))))) by EUCLID_6: 2

 .= ( - ( |.(C - A).| / ( sin ( angle (A,B,C))))) by XCMPLX_1: 188;

 hence thesis;

 end;

 theorem :: EUCLID10:46

 for A,B,C be Point of ( TOP-REAL 2) holds ( the_diameter_of_the_circumcircle (A,B,C)) = ( the_diameter_of_the_circumcircle (B,C,A)) by Thm27;

 theorem :: EUCLID10:47



 Thm31: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds ( the_diameter_of_the_circumcircle (A,B,C)) = ( - ( the_diameter_of_the_circumcircle (B,A,C)))

 proof

 let A,B,C be Point of ( TOP-REAL 2);



 A3: |.(B - A).| = |.(A - B).| & |.(A - C).| = |.(C - A).| & |.(C - B).| = |.(B - C).| by EUCLID_6: 43;

 ( the_diameter_of_the_circumcircle (B,A,C)) = (((( |.(A - B).| * |.(C - A).|) * |.(B - C).|) / 2) / ( - ( the_area_of_polygon3 (A,B,C)))) by A3, Thm28

 .= ( - (((( |.(A - B).| * |.(C - A).|) * |.(B - C).|) / 2) / ( the_area_of_polygon3 (A,B,C)))) by XCMPLX_1: 188;

 hence thesis;

 end;

 theorem :: EUCLID10:48



 Thm32: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds ( the_diameter_of_the_circumcircle (A,B,C)) = ( - ( the_diameter_of_the_circumcircle (A,C,B)))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume (A,B,C) is_a_triangle ;

 then

 A2: (A,C,B) is_a_triangle & (B,C,A) is_a_triangle by MENELAUS: 15;

 ( the_diameter_of_the_circumcircle (A,B,C)) = ( the_diameter_of_the_circumcircle (B,C,A)) by Thm27

 .= ( - ( the_diameter_of_the_circumcircle (C,B,A))) by A2, Thm31;

 hence thesis by Thm27;

 end;

 theorem :: EUCLID10:49



 Thm33: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds ( the_diameter_of_the_circumcircle (A,B,C)) = ( - ( the_diameter_of_the_circumcircle (C,B,A)))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume (A,B,C) is_a_triangle ;

 then ( the_diameter_of_the_circumcircle (A,B,C)) = ( - ( the_diameter_of_the_circumcircle (A,C,B))) by Thm32;

 hence thesis by Thm27;

 end;

 begin



 Lm10: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds |.(A - B).| = (( the_diameter_of_the_circumcircle (A,B,C)) * ( sin ( angle (A,C,B))))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume (A,B,C) is_a_triangle ;

 then

 A2: ( the_area_of_polygon3 (A,B,C)) <> 0 by MENELAUS: 9;

 set k = ((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) / ( the_area_of_polygon3 (B,C,A)));



 A3: ( the_area_of_polygon3 (B,C,A)) = ((( |.(B - C).| * |.(A - C).|) * ( sin ( angle (A,C,B)))) / 2) by EUCLID_6: 5;

 ( the_area_of_polygon3 (B,C,A)) <> 0 by A2, Thm27;

 then

 A4: |.(A - B).| = (( |.(A - B).| * ( the_area_of_polygon3 (B,C,A))) / ( the_area_of_polygon3 (B,C,A))) by XCMPLX_1: 89;



 A5: |.(A - B).| = ((((( |.(A - B).| * |.(B - C).|) * |.(A - C).|) * ( sin ( angle (A,C,B)))) / 2) / ( the_area_of_polygon3 (B,C,A))) by A4, A3;

 set abc = (( |.(A - B).| * |.(B - C).|) * |.(C - A).|);

 set S = ( the_area_of_polygon3 (B,C,A));

 set an = ( sin ( angle (A,C,B)));



 A6: (((abc * an) / 2) / S) = ((((abc * an) * 1) / 2) * (1 / S)) by XCMPLX_1: 99

 .= ((((abc * (1 / S)) * 1) / 2) * an)

 .= ((k / 2) * an) by XCMPLX_1: 99;

 (k / 2) = (((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) * (1 / ( the_area_of_polygon3 (B,C,A)))) / 2) by XCMPLX_1: 99

 .= (((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) * (1 / ( the_area_of_polygon3 (B,C,A))))

 .= (((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) * (1 / ( the_area_of_polygon3 (A,B,C)))) by Thm27

 .= (((( |.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / ( the_area_of_polygon3 (A,B,C))) by XCMPLX_1: 99;

 hence thesis by A6, A5, EUCLID_6: 43;

 end;

 theorem :: EUCLID10:50



 Thm34: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds |.(A - B).| = (( the_diameter_of_the_circumcircle (A,B,C)) * ( sin ( angle (A,C,B)))) & |.(B - C).| = (( the_diameter_of_the_circumcircle (A,B,C)) * ( sin ( angle (B,A,C)))) & |.(C - A).| = (( the_diameter_of_the_circumcircle (A,B,C)) * ( sin ( angle (C,B,A))))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume

 A1: (A,B,C) is_a_triangle ;

 then

 A2: (B,C,A) is_a_triangle & (C,A,B) is_a_triangle by MENELAUS: 15;



 A3: |.(B - C).| = (( the_diameter_of_the_circumcircle (B,C,A)) * ( sin ( angle (B,A,C)))) by A2, Lm10;

 thus |.(A - B).| = (( the_diameter_of_the_circumcircle (A,B,C)) * ( sin ( angle (A,C,B)))) by A1, Lm10;

 thus |.(B - C).| = (( the_diameter_of_the_circumcircle (A,B,C)) * ( sin ( angle (B,A,C)))) by A3, Thm27;

 |.(C - A).| = (( the_diameter_of_the_circumcircle (C,A,B)) * ( sin ( angle (C,B,A)))) by A2, Lm10;

 hence |.(C - A).| = (( the_diameter_of_the_circumcircle (A,B,C)) * ( sin ( angle (C,B,A)))) by Thm27;

 end;

 theorem :: EUCLID10:51

 for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle holds |.(A - B).| = ((((( 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))))

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume

 A1: (A,B,C) is_a_triangle ;

 |.(A - B).| = (( the_diameter_of_the_circumcircle (A,B,C)) * ( sin (3 * (( angle (A,C,B)) / 3)))) by A1, Lm10;

 then |.(A - B).| = (( 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))))) by Thm18;

 hence thesis;

 end;

 theorem :: EUCLID10:52

 for A,B,C,P be Point of ( TOP-REAL 2) st (A,B,P) are_mutually_distinct & ( angle (P,B,A)) = (( angle (C,B,A)) / 3) & ( angle (B,A,P)) = (( angle (B,A,C)) / 3) & ( angle (A,P,B)) < PI holds ( |.(A - P).| * ( sin ( PI - ((( angle (C,B,A)) / 3) + (( angle (B,A,C)) / 3))))) = ( |.(A - B).| * ( sin (( angle (C,B,A)) / 3)))

 proof

 let A,B,C,P be Point of ( TOP-REAL 2);

 assume that

 A1: (A,B,P) are_mutually_distinct and

 A2: ( angle (P,B,A)) = (( angle (C,B,A)) / 3) and

 A3: ( angle (B,A,P)) = (( angle (B,A,C)) / 3) and

 A4: ( angle (A,P,B)) < PI ;

 ((( angle (A,P,B)) + ( angle (P,B,A))) + ( angle (B,A,P))) = PI by A1, A4, EUCLID_3: 47;

 hence thesis by A1, A2, A3, EUCLID_6: 6;

 end;



 Lm11: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle & ( angle (C,B,A)) < PI holds ((( angle (C,B,A)) + ( angle (B,A,C))) + ( angle (A,C,B))) = PI & ((( angle (C,A,B)) + ( angle (A,B,C))) + ( angle (B,C,A))) = (5 * PI )

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume that

 A1: (A,B,C) is_a_triangle and

 A2: ( angle (C,B,A)) < PI ;



 A3: (A,B,C) are_mutually_distinct by A1, EUCLID_6: 20;

 hence ((( angle (C,B,A)) + ( angle (B,A,C))) + ( angle (A,C,B))) = PI by A2, EUCLID_3: 47;

 ( angle (C,B,A)) = ((2 * PI ) - ( angle (A,B,C))) & ( angle (B,A,C)) = ((2 * PI ) - ( angle (C,A,B))) & ( angle (A,C,B)) = ((2 * PI ) - ( angle (B,C,A))) by A1, Thm20;



 then ((( angle (C,A,B)) + ( angle (A,B,C))) + ( angle (B,C,A))) = ((6 * PI ) - ((( angle (B,A,C)) + ( angle (C,B,A))) + ( angle (A,C,B))))

 .= ((6 * PI ) - PI ) by A2, A3, EUCLID_3: 47

 .= (5 * PI );

 hence thesis;

 end;



 Lm12: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle & ( angle (C,B,A)) < PI holds (((( angle (C,B,A)) / 3) + (( angle (B,A,C)) / 3)) + (( angle (A,C,B)) / 3)) = ( PI / 3)

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume that

 A1: (A,B,C) is_a_triangle and

 A2: ( angle (C,B,A)) < PI ;

 ((( angle (C,B,A)) + ( angle (B,A,C))) + ( angle (A,C,B))) = PI by A1, A2, Lm11;

 hence thesis;

 end;

 theorem :: EUCLID10:53



 Thm35: for A,B,C,P be Point of ( TOP-REAL 2) st (A,B,P) are_mutually_distinct & ( angle (P,B,A)) = (( angle (C,B,A)) / 3) & ( angle (B,A,P)) = (( angle (B,A,C)) / 3) & ( angle (A,P,B)) < PI & (((( angle (C,B,A)) / 3) + (( angle (B,A,C)) / 3)) + (( angle (A,C,B)) / 3)) = ( PI / 3) holds ( |.(A - P).| * ( sin (((2 * PI ) / 3) + (( angle (A,C,B)) / 3)))) = ( |.(A - B).| * ( sin (( angle (C,B,A)) / 3)))

 proof

 let A,B,C,P be Point of ( TOP-REAL 2);

 assume that

 A1: (A,B,P) are_mutually_distinct and

 A2: ( angle (P,B,A)) = (( angle (C,B,A)) / 3) and

 A3: ( angle (B,A,P)) = (( angle (B,A,C)) / 3) and

 A4: ( angle (A,P,B)) < PI and

 A5: (((( angle (C,B,A)) / 3) + (( angle (B,A,C)) / 3)) + (( angle (A,C,B)) / 3)) = ( PI / 3);

 ((( angle (A,P,B)) + ( angle (P,B,A))) + ( angle (B,A,P))) = PI by A1, A4, EUCLID_3: 47;

 hence thesis by A1, A2, A3, A5, EUCLID_6: 6;

 end;

 theorem :: EUCLID10:54

 for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle & ( angle (C,A,B)) < PI holds ((( angle (C,B,A)) + ( angle (B,A,C))) + ( angle (A,C,B))) = (5 * PI ) & ((( angle (C,A,B)) + ( angle (A,B,C))) + ( angle (B,C,A))) = PI

 proof

 let A,B,C be Point of ( TOP-REAL 2);

 assume that

 A1: (A,B,C) is_a_triangle and

 A2: ( angle (C,A,B)) < PI ;

 (B,A,C) is_a_triangle by A1, MENELAUS: 15;

 hence thesis by A2, Lm11;

 end;

 theorem :: EUCLID10:55

 for A,B,C,P be Point of ( TOP-REAL 2) st (A,B,C) is_a_triangle & ( angle (C,B,A)) < PI & (A,B,P) are_mutually_distinct & ( angle (P,B,A)) = (( angle (C,B,A)) / 3) & ( angle (B,A,P)) = (( angle (B,A,C)) / 3) & ( angle (A,P,B)) < PI holds ( |.(A - P).| * ( sin (( PI / 3) - (( angle (A,C,B)) / 3)))) = ( |.(A - B).| * ( sin (( angle (C,B,A)) / 3)))

 proof

 let A,B,C,P be Point of ( TOP-REAL 2);

 assume that

 A1: (A,B,C) is_a_triangle and

 A2: ( angle (C,B,A)) < PI and

 A3: (A,B,P) are_mutually_distinct and

 A4: ( angle (P,B,A)) = (( angle (C,B,A)) / 3) and

 A5: ( angle (B,A,P)) = (( angle (B,A,C)) / 3) and

 A6: ( angle (A,P,B)) < PI ;



 A7: (((( angle (C,B,A)) / 3) + (( angle (B,A,C)) / 3)) + (( angle (A,C,B)) / 3)) = ( PI / 3) by A1, A2, Lm12;



 A8: ((( angle (A,P,B)) + ( angle (P,B,A))) + ( angle (B,A,P))) = PI by A3, A6, EUCLID_3: 47;

 ( |.(A - P).| * ( sin ( PI - ((( angle (C,B,A)) / 3) + (( angle (B,A,C)) / 3))))) = ( |.(A - B).| * ( sin (( angle (C,B,A)) / 3))) by A3, A4, EUCLID_6: 6, A8, A5;

 hence thesis by A7, Thm1;

 end;

 theorem :: EUCLID10:56

 for A,B,C,P be Point of ( TOP-REAL 2) st (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 holds |.(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))))

 proof

 let A,B,C,P be Point of ( TOP-REAL 2);

 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 ;



 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 thesis;

 end;

 begin

 theorem :: EUCLID10:57



 Thm37: for A,B,C be Point of ( TOP-REAL 2) st (A,B,C) are_mutually_distinct & C in ( LSeg (A,B)) holds |.(A - B).| = ( |.(A - C).| + |.(C - B).|)

 proof

 let A,B,C be Point of ( TOP-REAL 2) such that

 A1: (A,B,C) are_mutually_distinct and

 A2: C in ( LSeg (A,B));

 ( |.(B - A).| ^2 ) = ((( |.(A - C).| ^2 ) + ( |.(B - C).| ^2 )) - (((2 * |.(A - C).|) * |.(B - C).|) * ( cos ( angle (A,C,B))))) by EUCLID_6: 7

 .= ((( |.(A - C).| ^2 ) + ( |.(B - C).| ^2 )) - (((2 * |.(A - C).|) * |.(B - C).|) * ( - 1))) by A1, A2, SIN_COS: 77, EUCLID_6: 8

 .= ((( |.(A - C).| ^2 ) + ((2 * |.(A - C).|) * |.(B - C).|)) + ( |.(B - C).| ^2 ))

 .= (( |.(A - C).| + |.(B - C).|) ^2 ) by SQUARE_1: 4;

 then

 A3: |.(B - A).| = ( |.(A - C).| + |.(B - C).|) or |.(B - A).| = ( - ( |.(A - C).| + |.(B - C).|)) by SQUARE_1: 40;

 |.(B - A).| >= 0 & |.(A - C).| >= 0 & |.(B - C).| >= 0 & not |.(B - A).| = 0 & not |.(A - C).| = 0 & not |.(B - C).| = 0 by A1, EUCLID_6: 42;

 then |.(A - B).| = ( |.(A - C).| + |.(B - C).|) by A3, EUCLID_6: 43;

 hence thesis by EUCLID_6: 43;

 end;

 theorem :: EUCLID10:58



 Thm38: for A,B be Point of ( TOP-REAL 2), a,b be Real, r be positive Real st (A,B, |[a, b]|) are_mutually_distinct & A in ( circle (a,b,r)) & B in ( circle (a,b,r)) & |[a, b]| in ( LSeg (A,B)) holds |.(A - B).| = (2 * r)

 proof

 let A,B be Point of ( TOP-REAL 2), a,b be Real, r be positive Real such that

 A1: (A,B, |[a, b]|) are_mutually_distinct and

 A2: A in ( circle (a,b,r)) & B in ( circle (a,b,r)) and

 A3: |[a, b]| in ( LSeg (A,B));



 A4: ( circle (a,b,r)) = { p where p be Point of ( TOP-REAL 2) : |.(p - |[a, b]|).| = r } by JGRAPH_6:def 5;

 consider JA be Point of ( TOP-REAL 2) such that

 A5: A = JA and

 A6: |.(JA - |[a, b]|).| = r by A2, A4;

 consider JB be Point of ( TOP-REAL 2) such that

 A7: B = JB and

 A8: |.(JB - |[a, b]|).| = r by A2, A4;

 |.(A - B).| = ( |.(A - |[a, b]|).| + |.( |[a, b]| - B).|) by A1, A3, Thm37

 .= (r + r) by A5, A6, A7, A8, EUCLID_6: 43;

 hence thesis;

 end;

 theorem :: EUCLID10:59

 for a,b be Real, r be positive Real, C be Subset of ( Euclid 2) st C = ( circle (a,b,r)) holds ( diameter C) = (2 * r)

 proof

 let a,b be Real, r be positive Real, C be Subset of ( Euclid 2) such that

 A1: C = ( circle (a,b,r));



 A2: ( circle (a,b,r)) = { p where p be Point of ( TOP-REAL 2) : |.(p - |[a, b]|).| = r } by JGRAPH_6:def 5;



 A3: for x,y be Point of ( Euclid 2) st x in C & y in C holds ( dist (x,y)) <= (2 * r)

 proof

 let x,y be Point of ( Euclid 2) such that

 A4: x in C and

 A5: y in C;

 consider JA be Point of ( TOP-REAL 2) such that

 A6: x = JA and

 A7: |.(JA - |[a, b]|).| = r by A1, A4, A2;

 consider JB be Point of ( TOP-REAL 2) such that

 A8: y = JB and

 A9: |.(JB - |[a, b]|).| = r by A1, A5, A2;

 reconsider KA = JA, KB = JB as Element of ( REAL 2) by EUCLID: 22;

 reconsider O = |[a, b]| as Element of ( REAL 2) by EUCLID: 22;

 reconsider O2 = |[a, b]| as Point of ( Euclid 2) by EUCLID: 67;



 A10: ( dist (x,y)) <= (( dist (x,O2)) + ( dist (y,O2))) by METRIC_1: 4;

 ( dist (y,O2)) = |.(KB - O).| by A8, SPPOL_1: 5;

 then ( dist (x,y)) <= ( |.(KA - O).| + |.(KB - O).|) by A10, A6, SPPOL_1: 5;

 hence thesis by A7, A9;

 end;



 A12: C is bounded by A1, JORDAN2C: 11;

 for s be Real st (for x,y be Point of ( Euclid 2) st x in C & y in C holds ( dist (x,y)) <= s) holds (2 * r) <= s

 proof

 let s be Real;

 assume

 A13: for x,y be Point of ( Euclid 2) st x in C & y in C holds ( dist (x,y)) <= s;

 assume

 A14: s < (2 * r);

 set A1 = |[(a + r), b]|;

 set B1 = |[(a - r), b]|;



 A15: (A1 - |[a, b]|) = |[((a + r) - a), (b - b)]| by EUCLID: 62

 .= |[r, 0 ]|;



 A16: (B1 - |[a, b]|) = |[((a - r) - a), (b - b)]| by EUCLID: 62

 .= |[( - r), 0 ]|;



 A17: ((r ^2 ) + ( 0 ^2 )) = ((r ^2 ) + ( 0 * 0 )) by SQUARE_1:def 1

 .= (r ^2 );

 ( Re (r + ( 0 * ))) = r & ( Im (r + ( 0 * ))) = 0 by COMPLEX1: 12;



 then |.( cpx2euc (r + ( 0 * ))).| = ( sqrt (r ^2 )) by A17, EUCLID_3: 24

 .= r by SQUARE_1: 22;

 then

 A18: |.(A1 - |[a, b]|).| = r by A15, EUCLID_3: 5;

 then

 A19: A1 in ( circle (a,b,r)) by A2;



 A20: A1 in C by A18, A1, A2;



 A21: ((( - r) ^2 ) + ( 0 ^2 )) = ((( - r) ^2 ) + ( 0 * 0 )) by SQUARE_1:def 1

 .= (r ^2 ) by SQUARE_1: 3;

 ( Re (( - r) + ( 0 * ))) = ( - r) & ( Im (( - r) + ( 0 * ))) = 0 by COMPLEX1: 12;



 then |.( cpx2euc (( - r) + ( 0 * ))).| = ( sqrt (r ^2 )) by A21, EUCLID_3: 24

 .= r by SQUARE_1: 22;

 then

 A22: |. |[( - r), 0 ]|.| = r by EUCLID_3: 5;

 then

 A23: B1 in ( circle (a,b,r)) by A2, A16;



 A24: B1 in C by A1, A2, A22, A16;



 A25: |[a, b]| in ( LSeg (A1,B1))

 proof

 ( |[(a + r), b]| + |[(a - r), b]|) = |[((a + r) + (a - r)), (b + b)]| by EUCLID: 56;



 then ((1 / 2) * (A1 + B1)) = |[((1 / 2) * (2 * a)), ((1 / 2) * (2 * b))]| by EUCLID: 58

 .= |[a, b]|;

 hence thesis by RLTOPSP1: 69;

 end;



 A26: A1 <> B1

 proof

 assume A1 = B1;

 then (a + r) = (a - r) & b = b by SPPOL_2: 1;

 then r = 0 ;

 hence contradiction;

 end;



 A27: A1 <> |[a, b]|

 proof

 assume A1 = |[a, b]|;

 then (a + r) = a & b = b by SPPOL_2: 1;

 then r = 0 ;

 hence contradiction;

 end;

 (A1,B1, |[a, b]|) are_mutually_distinct

 proof

 B1 <> |[a, b]|

 proof

 assume B1 = |[a, b]|;

 then (a - r) = a & b = b by SPPOL_2: 1;

 then ( - r) = 0 ;

 hence contradiction;

 end;

 hence thesis by A26, A27;

 end;

 then

 A28: |.(A1 - B1).| = (2 * r) by A19, A23, A25, Thm38;

 reconsider a1 = A1, b1 = B1 as Point of ( Euclid 2) by EUCLID: 67;

 reconsider A2 = A1, B2 = B1 as Element of ( REAL 2) by EUCLID: 22;

 ( Euclid 2) = MetrStruct (# ( REAL 2), ( Pitag_dist 2) #) by EUCLID:def 7;



 then ( dist (a1,b1)) = (( Pitag_dist 2) . (A1,B1)) by METRIC_1:def 1

 .= |.(A2 - B2).| by EUCLID:def 6

 .= (2 * r) by A28;

 hence contradiction by A14, A20, A24, A13;

 end;

 hence thesis by A3, A12, A1, TBSP_1:def 8;

 end;