sin_cos6.miz



    begin

    reserve r,r1,r2,s,x for Real,

i for Integer;

    theorem :: SIN_COS6:1

    

     Th1: 0 <= r & r < s implies [\(r / s)/] = 0

    proof

      assume

       A1: 0 <= r & r < s;

      then (r / s) < (s / s) by XREAL_1: 74;

      then ((r / s) - 1) < ((s / s) - 1) by XREAL_1: 9;

      then ((r / s) - 1) < (1 - 1) by A1, XCMPLX_1: 60;

      hence thesis by A1, INT_1:def 6;

    end;

    theorem :: SIN_COS6:2

    

     Th2: for f be Function, X,Y be set st (f | X) is one-to-one & Y c= X holds (f | Y) is one-to-one

    proof

      let f be Function, X,Y be set such that

       A1: (f | X) is one-to-one and

       A2: Y c= X;

      let x,y be object;

      

       A3: ( dom (f | Y)) = (( dom f) /\ Y) by RELAT_1: 61;

      assume

       A4: x in ( dom (f | Y));

      then

       A5: x in Y by A3, XBOOLE_0:def 4;

      x in ( dom f) by A3, A4, XBOOLE_0:def 4;

      then x in (( dom f) /\ X) by A2, A5, XBOOLE_0:def 4;

      then

       A6: x in ( dom (f | X)) by RELAT_1: 61;

      assume

       A7: y in ( dom (f | Y));

      then

       A8: y in Y by A3, XBOOLE_0:def 4;

      y in ( dom f) by A3, A7, XBOOLE_0:def 4;

      then y in (( dom f) /\ X) by A2, A8, XBOOLE_0:def 4;

      then

       A9: y in ( dom (f | X)) by RELAT_1: 61;

      assume

       A10: ((f | Y) . x) = ((f | Y) . y);

      ((f | X) . x) = (f . x) by A2, A5, FUNCT_1: 49

      .= ((f | Y) . x) by A5, FUNCT_1: 49

      .= (f . y) by A8, A10, FUNCT_1: 49

      .= ((f | X) . y) by A2, A8, FUNCT_1: 49;

      hence thesis by A1, A6, A9;

    end;

    begin

    theorem :: SIN_COS6:3

    

     Th3: ( - 1) <= ( sin r)

    proof

      ( sin . r) in [.( - 1), 1.] by COMPTRIG: 27;

      then ( sin r) in [.( - 1), 1.] by SIN_COS:def 17;

      hence thesis by XXREAL_1: 1;

    end;

    theorem :: SIN_COS6:4

    

     Th4: ( sin r) <= 1

    proof

      ( sin . r) in [.( - 1), 1.] by COMPTRIG: 27;

      then ( sin r) in [.( - 1), 1.] by SIN_COS:def 17;

      hence thesis by XXREAL_1: 1;

    end;

    theorem :: SIN_COS6:5

    

     Th5: ( - 1) <= ( cos r)

    proof

      ( cos . r) in [.( - 1), 1.] by COMPTRIG: 27;

      then ( cos r) in [.( - 1), 1.] by SIN_COS:def 19;

      hence thesis by XXREAL_1: 1;

    end;

    theorem :: SIN_COS6:6

    

     Th6: ( cos r) <= 1

    proof

      ( cos . r) in [.( - 1), 1.] by COMPTRIG: 27;

      then ( cos r) in [.( - 1), 1.] by SIN_COS:def 19;

      hence thesis by XXREAL_1: 1;

    end;

    deffunc T( Integer) = ((2 * PI ) * $1);

    

     Lm1: [.(( - ( PI / 2)) + T(0)), (( PI / 2) + T(0)).] = [.( - ( PI / 2)), ( PI / 2).];

    

     Lm2: [.(( PI / 2) + T(0)), (((3 / 2) * PI ) + T(0)).] = [.( PI / 2), ((3 / 2) * PI ).];

    

     Lm3: [. T(0), ( PI + T(0)).] = [. 0 , PI .];

    

     Lm4: [.( PI + T(0)), ((2 * PI ) + T(0)).] = [. PI , (2 * PI ).];

    

     Lm5: ((r ^2 ) + (s ^2 )) = 1 implies ( - 1) <= r & r <= 1

    proof

      (s ^2 ) >= 0 by XREAL_1: 63;

      then ( - (s ^2 )) <= ( - 0 );

      then ((r ^2 ) - ((r ^2 ) + (s ^2 ))) <= 0 ;

      hence thesis by SQUARE_1: 43;

    end;

    registration

      cluster PI -> positive;

      coherence

      proof

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

        hence PI > 0 by XXREAL_1: 4;

      end;

    end

    

     Lm6: ( PI / 2) < ( PI / 1) by XREAL_1: 76;

    

     Lm7: (1 * PI ) < ((3 / 2) * PI ) by XREAL_1: 68;

    

     Lm8: ( 0 + T()) < (( PI / 2) + T()) by XREAL_1: 6;

    

     Lm9: ((3 / 2) * PI ) < (2 * PI ) by XREAL_1: 68;

    

     Lm10: (1 * PI ) < (2 * PI ) by XREAL_1: 68;

    theorem :: SIN_COS6:7

    

     Th7: ( sin ( - ( PI / 2))) = ( - 1) & ( sin . ( - ( PI / 2))) = ( - 1)

    proof

      ( sin . ( - ( PI / 2))) = ( sin . (( - ( PI / 2)) + (2 * PI ))) by SIN_COS: 78

      .= ( - 1) by SIN_COS: 76;

      hence thesis by SIN_COS:def 17;

    end;

    theorem :: SIN_COS6:8

    

     Th8: ( sin . r) = ( sin . (r + ((2 * PI ) * i)))

    proof

      

      thus ( sin . r) = ( sin r) by SIN_COS:def 17

      .= ( sin (r + ((2 * PI ) * i))) by COMPLEX2: 8

      .= ( sin . (r + ((2 * PI ) * i))) by SIN_COS:def 17;

    end;

    theorem :: SIN_COS6:9

    

     Th9: ( cos ( - ( PI / 2))) = 0 & ( cos . ( - ( PI / 2))) = 0

    proof

      ( cos . ( - ( PI / 2))) = ( cos . (( - ( PI / 2)) + (2 * PI ))) by SIN_COS: 78

      .= 0 by SIN_COS: 76;

      hence thesis by SIN_COS:def 19;

    end;

    theorem :: SIN_COS6:10

    

     Th10: ( cos . r) = ( cos . (r + ((2 * PI ) * i)))

    proof

      

      thus ( cos . r) = ( cos r) by SIN_COS:def 19

      .= ( cos (r + ((2 * PI ) * i))) by COMPLEX2: 9

      .= ( cos . (r + ((2 * PI ) * i))) by SIN_COS:def 19;

    end;

    theorem :: SIN_COS6:11

    

     Th11: ((2 * PI ) * i) < r & r < ( PI + ((2 * PI ) * i)) implies ( sin r) > 0

    proof

      assume T(i) < r & r < ( PI + T(i));

      then ( T(i) - T(i)) < (r - T(i)) & (r - T(i)) < (( PI + T(i)) - T(i)) by XREAL_1: 9;

      then (r - T(i)) in ]. 0 , PI .[ by XXREAL_1: 4;

      then ( sin . (r + T(-))) > 0 by COMPTRIG: 7;

      then ( sin . r) > 0 by Th8;

      hence thesis by SIN_COS:def 17;

    end;

    theorem :: SIN_COS6:12

    

     Th12: ( PI + ((2 * PI ) * i)) < r & r < ((2 * PI ) + ((2 * PI ) * i)) implies ( sin r) < 0

    proof

      assume ( PI + T(i)) < r & r < ((2 * PI ) + T(i));

      then (( PI + T(i)) - T(i)) < (r - T(i)) & (r - T(i)) < (((2 * PI ) + T(i)) - T(i)) by XREAL_1: 9;

      then (r - T(i)) in ]. PI , (2 * PI ).[ by XXREAL_1: 4;

      then ( sin . (r + T(-))) < 0 by COMPTRIG: 9;

      then ( sin . r) < 0 by Th8;

      hence thesis by SIN_COS:def 17;

    end;

    theorem :: SIN_COS6:13

    

     Th13: (( - ( PI / 2)) + ((2 * PI ) * i)) < r & r < (( PI / 2) + ((2 * PI ) * i)) implies ( cos r) > 0

    proof

      assume that

       A1: (( - ( PI / 2)) + T(i)) < r and

       A2: r < (( PI / 2) + T(i));

      (r + ( PI / 2)) < ((( PI / 2) + T(i)) + ( PI / 2)) by A2, XREAL_1: 6;

      then

       A3: (r + ( PI / 2)) < ( PI + T(i));

      

       A4: ( sin (r + ( PI / 2))) = ( cos r) by SIN_COS: 79;

      ((( - ( PI / 2)) + T(i)) + ( PI / 2)) < (r + ( PI / 2)) by A1, XREAL_1: 6;

      hence thesis by A3, A4, Th11;

    end;

    theorem :: SIN_COS6:14

    

     Th14: (( PI / 2) + ((2 * PI ) * i)) < r & r < (((3 / 2) * PI ) + ((2 * PI ) * i)) implies ( cos r) < 0

    proof

      assume that

       A1: (( PI / 2) + T(i)) < r and

       A2: r < (((3 / 2) * PI ) + T(i));

      ((( PI / 2) + T(i)) + ( PI / 2)) < (r + ( PI / 2)) by A1, XREAL_1: 6;

      then

       A3: ( PI + T(i)) < (r + ( PI / 2));

      (r + ( PI / 2)) < ((((3 / 2) * PI ) + T(i)) + ( PI / 2)) by A2, XREAL_1: 6;

      then

       A4: (r + ( PI / 2)) < ((2 * PI ) + T(i));

      ( sin (r + ( PI / 2))) = ( cos r) by SIN_COS: 79;

      hence thesis by A3, A4, Th12;

    end;

    theorem :: SIN_COS6:15

    

     Th15: (((3 / 2) * PI ) + ((2 * PI ) * i)) < r & r < ((2 * PI ) + ((2 * PI ) * i)) implies ( cos r) > 0

    proof

      assume that

       A1: (((3 / 2) * PI ) + T(i)) < r and

       A2: r < ((2 * PI ) + T(i));

      ((((3 / 2) * PI ) + T(i)) - PI ) < (r - PI ) by A1, XREAL_1: 9;

      then

       A3: (( PI / 2) + T(i)) < (r - PI );

      ( PI + T(i)) < (((3 / 2) * PI ) + T(i)) & (r - PI ) < (((2 * PI ) + T(i)) - PI ) by A2, COMPTRIG: 5, XREAL_1: 6, XREAL_1: 9;

      then

       A4: (r - PI ) < (((3 / 2) * PI ) + T(i)) by XXREAL_0: 2;

      ( cos (r - PI )) = ( cos ( - ( PI - r)))

      .= ( cos ( PI + ( - r))) by SIN_COS: 31

      .= ( - ( cos ( - r))) by SIN_COS: 79

      .= ( - ( cos r)) by SIN_COS: 31;

      hence thesis by A3, A4, Th14;

    end;

    theorem :: SIN_COS6:16

    ((2 * PI ) * i) <= r & r <= ( PI + ((2 * PI ) * i)) implies ( sin r) >= 0

    proof

      assume

       A1: ((2 * PI ) * i) <= r & r <= ( PI + ((2 * PI ) * i));

      per cases by A1, XXREAL_0: 1;

        suppose ((2 * PI ) * i) < r & r < ( PI + ((2 * PI ) * i));

        hence thesis by Th11;

      end;

        suppose

         A2: ((2 * PI ) * i) = r;

        ( sin ( 0 + ((2 * PI ) * i))) = ( sin 0 ) by COMPLEX2: 8;

        hence thesis by A2, SIN_COS: 31;

      end;

        suppose r = ( PI + ((2 * PI ) * i));

        hence thesis by COMPLEX2: 8, SIN_COS: 77;

      end;

    end;

    theorem :: SIN_COS6:17

    ( PI + ((2 * PI ) * i)) <= r & r <= ((2 * PI ) + ((2 * PI ) * i)) implies ( sin r) <= 0

    proof

      assume ( PI + ((2 * PI ) * i)) <= r & r <= ((2 * PI ) + ((2 * PI ) * i));

      then ( PI + ((2 * PI ) * i)) < r & r < ((2 * PI ) + ((2 * PI ) * i)) or ( PI + ((2 * PI ) * i)) = r or r = ((2 * PI ) + ((2 * PI ) * i)) by XXREAL_0: 1;

      hence thesis by Th12, COMPLEX2: 8, SIN_COS: 77;

    end;

    theorem :: SIN_COS6:18

    (( - ( PI / 2)) + ((2 * PI ) * i)) <= r & r <= (( PI / 2) + ((2 * PI ) * i)) implies ( cos r) >= 0

    proof

      assume (( - ( PI / 2)) + ((2 * PI ) * i)) <= r & r <= (( PI / 2) + ((2 * PI ) * i));

      then (( - ( PI / 2)) + ((2 * PI ) * i)) < r & r < (( PI / 2) + ((2 * PI ) * i)) or (( - ( PI / 2)) + ((2 * PI ) * i)) = r or r = (( PI / 2) + ((2 * PI ) * i)) by XXREAL_0: 1;

      hence thesis by Th9, Th13, COMPLEX2: 9, SIN_COS: 77;

    end;

    theorem :: SIN_COS6:19

    (( PI / 2) + ((2 * PI ) * i)) <= r & r <= (((3 / 2) * PI ) + ((2 * PI ) * i)) implies ( cos r) <= 0

    proof

      assume (( PI / 2) + ((2 * PI ) * i)) <= r & r <= (((3 / 2) * PI ) + ((2 * PI ) * i));

      then (( PI / 2) + ((2 * PI ) * i)) < r & r < (((3 / 2) * PI ) + ((2 * PI ) * i)) or (( PI / 2) + ((2 * PI ) * i)) = r or r = (((3 / 2) * PI ) + ((2 * PI ) * i)) by XXREAL_0: 1;

      hence thesis by Th14, COMPLEX2: 9, SIN_COS: 77;

    end;

    theorem :: SIN_COS6:20

    (((3 / 2) * PI ) + ((2 * PI ) * i)) <= r & r <= ((2 * PI ) + ((2 * PI ) * i)) implies ( cos r) >= 0

    proof

      assume

       A1: (((3 / 2) * PI ) + ((2 * PI ) * i)) <= r & r <= ((2 * PI ) + ((2 * PI ) * i));

      per cases by A1, XXREAL_0: 1;

        suppose (((3 / 2) * PI ) + ((2 * PI ) * i)) < r & r < ((2 * PI ) + ((2 * PI ) * i));

        hence thesis by Th15;

      end;

        suppose (((3 / 2) * PI ) + ((2 * PI ) * i)) = r;

        hence thesis by COMPLEX2: 9, SIN_COS: 77;

      end;

        suppose r = ((2 * PI ) + ((2 * PI ) * i));

        hence thesis by COMPLEX2: 9, SIN_COS: 77;

      end;

    end;

    theorem :: SIN_COS6:21

    

     Th21: ((2 * PI ) * i) <= r & r < ((2 * PI ) + ((2 * PI ) * i)) & ( sin r) = 0 implies r = ((2 * PI ) * i) or r = ( PI + ((2 * PI ) * i))

    proof

      assume

       A1: T(i) <= r & r < ((2 * PI ) + T(i));

      assume

       A2: ( sin r) = 0 ;

      then

       A3: r <= ( PI + T(i)) or ((2 * PI ) + T(i)) <= r by Th12;

      r <= T(i) or r >= ( PI + T(i)) by A2, Th11;

      hence thesis by A1, A3, XXREAL_0: 1;

    end;

    theorem :: SIN_COS6:22

    

     Th22: ((2 * PI ) * i) <= r & r < ((2 * PI ) + ((2 * PI ) * i)) & ( cos r) = 0 implies r = (( PI / 2) + ((2 * PI ) * i)) or r = (((3 / 2) * PI ) + ((2 * PI ) * i))

    proof

      assume that

       A1: T(i) <= r and

       A2: r < ((2 * PI ) + T(i));

      

       A3: (( - ( PI / 2)) + T(i)) < ( 0 + T(i)) by XREAL_1: 6;

      assume

       A4: ( cos r) = 0 ;

      then

       A5: (( PI / 2) + T(i)) >= r or r >= (((3 / 2) * PI ) + T(i)) by Th14;

      (( - ( PI / 2)) + T(i)) >= r or r >= (( PI / 2) + T(i)) by A4, Th13;

      then r = (( PI / 2) + T(i)) or r = (((3 / 2) * PI ) + T(i)) or r > (((3 / 2) * PI ) + T(i)) by A1, A5, A3, XXREAL_0: 1, XXREAL_0: 2;

      hence thesis by A2, A4, Th15;

    end;

    theorem :: SIN_COS6:23

    

     Th23: ( sin r) = ( - 1) implies r = (((3 / 2) * PI ) + ((2 * PI ) * [\(r / (2 * PI ))/]))

    proof

      set i = [\(r / (2 * PI ))/];

      consider w be Real such that

       A1: w = (((2 * PI ) * ( - i)) + r) and

       A2: 0 <= w & w < (2 * PI ) by COMPLEX2: 1;

      assume

       A3: ( sin r) = ( - 1);

      then ((( cos r) * ( cos r)) + (( - 1) * ( - 1))) = 1 by SIN_COS: 29;

      then

       A4: ( cos r) = 0 ;

      ( 0 + T(i)) <= (w + T(i)) & (w + T(i)) < ((2 * PI ) + T(i)) by A2, XREAL_1: 6;

      then r = (( PI / 2) + T(i)) or r = (((3 / 2) * PI ) + T(i)) by A1, A4, Th22;

      hence thesis by A3, COMPLEX2: 8, SIN_COS: 77;

    end;

    theorem :: SIN_COS6:24

    

     Th24: ( sin r) = 1 implies r = (( PI / 2) + ((2 * PI ) * [\(r / (2 * PI ))/]))

    proof

      set i = [\(r / (2 * PI ))/];

      consider w be Real such that

       A1: w = (((2 * PI ) * ( - i)) + r) and

       A2: 0 <= w & w < (2 * PI ) by COMPLEX2: 1;

      assume

       A3: ( sin r) = 1;

      then ((( cos r) * ( cos r)) + (1 * 1)) = 1 by SIN_COS: 29;

      then

       A4: ( cos r) = 0 ;

      ( 0 + T(i)) <= (w + T(i)) & (w + T(i)) < ((2 * PI ) + T(i)) by A2, XREAL_1: 6;

      then r = (( PI / 2) + T(i)) or r = (((3 / 2) * PI ) + T(i)) by A1, A4, Th22;

      hence thesis by A3, COMPLEX2: 8, SIN_COS: 77;

    end;

    theorem :: SIN_COS6:25

    

     Th25: ( cos r) = ( - 1) implies r = ( PI + ((2 * PI ) * [\(r / (2 * PI ))/]))

    proof

      set i = [\(r / (2 * PI ))/];

      consider w be Real such that

       A1: w = (((2 * PI ) * ( - i)) + r) and

       A2: 0 <= w & w < (2 * PI ) by COMPLEX2: 1;

      assume

       A3: ( cos r) = ( - 1);

      then ((( sin r) * ( sin r)) + (( - 1) * ( - 1))) = 1 by SIN_COS: 29;

      then

       A4: ( sin r) = 0 ;

      ( 0 + T(i)) <= (w + T(i)) & (w + T(i)) < ((2 * PI ) + T(i)) by A2, XREAL_1: 6;

      then r = ( 0 + T(i)) or r = ( PI + T(i)) by A1, A4, Th21;

      hence thesis by A3, COMPLEX2: 9, SIN_COS: 31;

    end;

    theorem :: SIN_COS6:26

    

     Th26: ( cos r) = 1 implies r = ((2 * PI ) * [\(r / (2 * PI ))/])

    proof

      set i = [\(r / (2 * PI ))/];

      consider w be Real such that

       A1: w = (((2 * PI ) * ( - i)) + r) and

       A2: 0 <= w & w < (2 * PI ) by COMPLEX2: 1;

      assume

       A3: ( cos r) = 1;

      then ((( sin r) * ( sin r)) + (1 * 1)) = 1 by SIN_COS: 29;

      then

       A4: ( sin r) = 0 ;

      ( 0 + T(i)) <= (w + T(i)) & (w + T(i)) < ((2 * PI ) + T(i)) by A2, XREAL_1: 6;

      then r = ( 0 + T(i)) or r = ( PI + T(i)) by A1, A4, Th21;

      hence thesis by A3, COMPLEX2: 9, SIN_COS: 77;

    end;

    theorem :: SIN_COS6:27

    

     Th27: 0 <= r & r <= (2 * PI ) & ( sin r) = ( - 1) implies r = ((3 / 2) * PI )

    proof

      assume that

       A1: 0 <= r and

       A2: r <= (2 * PI ) and

       A3: ( sin r) = ( - 1);

      

       A4: r = (2 * PI ) or r < (2 * PI ) by A2, XXREAL_0: 1;

      

      thus r = (((3 / 2) * PI ) + ((2 * PI ) * [\(r / (2 * PI ))/])) by A3, Th23

      .= (((3 / 2) * PI ) + ((2 * PI ) * 0 )) by A1, A3, A4, Th1, SIN_COS: 77

      .= ((3 / 2) * PI );

    end;

    theorem :: SIN_COS6:28

    

     Th28: 0 <= r & r <= (2 * PI ) & ( sin r) = 1 implies r = ( PI / 2)

    proof

      assume that

       A1: 0 <= r and

       A2: r <= (2 * PI ) and

       A3: ( sin r) = 1;

      

       A4: r = (2 * PI ) or r < (2 * PI ) by A2, XXREAL_0: 1;

      

      thus r = (( PI / 2) + ((2 * PI ) * [\(r / (2 * PI ))/])) by A3, Th24

      .= (( PI / 2) + ((2 * PI ) * 0 )) by A1, A3, A4, Th1, SIN_COS: 77

      .= ( PI / 2);

    end;

    theorem :: SIN_COS6:29

    

     Th29: 0 <= r & r <= (2 * PI ) & ( cos r) = ( - 1) implies r = PI

    proof

      assume that

       A1: 0 <= r and

       A2: r <= (2 * PI ) and

       A3: ( cos r) = ( - 1);

      

       A4: r = (2 * PI ) or r < (2 * PI ) by A2, XXREAL_0: 1;

      

      thus r = ( PI + ((2 * PI ) * [\(r / (2 * PI ))/])) by A3, Th25

      .= ( PI + ((2 * PI ) * 0 )) by A1, A3, A4, Th1, SIN_COS: 77

      .= PI ;

    end;

    theorem :: SIN_COS6:30

    

     Th30: 0 <= r & r < ( PI / 2) implies ( sin r) < 1

    proof

      assume that

       A1: 0 <= r and

       A2: r < ( PI / 2) and

       A3: ( sin r) >= 1;

      

       A4: ( sin r) <= 1 by Th4;

      ((1 / 2) * PI ) <= (2 * PI ) by XREAL_1: 64;

      then r < (2 * PI ) by A2, XXREAL_0: 2;

      hence thesis by A1, A2, A3, A4, Th28, XXREAL_0: 1;

    end;

    theorem :: SIN_COS6:31

    

     Th31: 0 <= r & r < ((3 / 2) * PI ) implies ( sin r) > ( - 1)

    proof

      assume that

       A1: 0 <= r and

       A2: r < ((3 / 2) * PI ) and

       A3: ( sin r) <= ( - 1);

      

       A4: ( sin r) >= ( - 1) by Th3;

      r <= (2 * PI ) by A2, Lm9, XXREAL_0: 2;

      hence thesis by A1, A2, A3, A4, Th27, XXREAL_0: 1;

    end;

    theorem :: SIN_COS6:32

    

     Th32: ((3 / 2) * PI ) < r & r <= (2 * PI ) implies ( sin r) > ( - 1)

    proof

      assume

       A1: ((3 / 2) * PI ) < r & r <= (2 * PI ) & ( sin r) <= ( - 1);

      ( sin r) >= ( - 1) by Th3;

      hence thesis by A1, Th27, XXREAL_0: 1;

    end;

    theorem :: SIN_COS6:33

    

     Th33: ( PI / 2) < r & r <= (2 * PI ) implies ( sin r) < 1

    proof

      assume

       A1: ( PI / 2) < r & r <= (2 * PI ) & ( sin r) >= 1;

      ( sin r) <= 1 by Th4;

      hence thesis by A1, Th28, XXREAL_0: 1;

    end;

    theorem :: SIN_COS6:34

    

     Th34: 0 < r & r < (2 * PI ) implies ( cos r) < 1

    proof

      assume 0 < r & r < (2 * PI );

      then

       A1: ( cos r) <> 1 by COMPTRIG: 61;

      ( cos r) <= 1 by Th6;

      hence thesis by A1, XXREAL_0: 1;

    end;

    theorem :: SIN_COS6:35

    

     Th35: 0 <= r & r < PI implies ( cos r) > ( - 1)

    proof

      assume that

       A1: 0 <= r and

       A2: r < PI ;

      

       A3: ( cos r) >= ( - 1) by Th5;

      r <= (2 * PI ) by A2, Lm10, XXREAL_0: 2;

      hence thesis by A1, A2, A3, Th29, XXREAL_0: 1;

    end;

    theorem :: SIN_COS6:36

    

     Th36: PI < r & r <= (2 * PI ) implies ( cos r) > ( - 1)

    proof

      assume

       A1: PI < r & r <= (2 * PI );

      ( cos r) >= ( - 1) by Th5;

      hence thesis by A1, Th29, XXREAL_0: 1;

    end;

    theorem :: SIN_COS6:37

    ((2 * PI ) * i) <= r & r < (( PI / 2) + ((2 * PI ) * i)) implies ( sin r) < 1

    proof

      assume that

       A1: T(i) <= r & r < (( PI / 2) + T(i)) and

       A2: ( sin r) >= 1;

      

       A3: ( T(i) - T(i)) <= (r - T(i)) & (r - T(i)) < ((( PI / 2) + T(i)) - T(i)) by A1, XREAL_1: 9;

      

       A4: ( sin r) <= 1 by Th4;

      ( sin (r - T(i))) = ( sin (r + T(-)))

      .= ( sin r) by COMPLEX2: 8

      .= 1 by A2, A4, XXREAL_0: 1;

      hence thesis by A3, Th30;

    end;

    theorem :: SIN_COS6:38

    ((2 * PI ) * i) <= r & r < (((3 / 2) * PI ) + ((2 * PI ) * i)) implies ( sin r) > ( - 1)

    proof

      assume that

       A1: T(i) <= r & r < (((3 / 2) * PI ) + T(i)) and

       A2: ( sin r) <= ( - 1);

      

       A3: ( T(i) - T(i)) <= (r - T(i)) & (r - T(i)) < ((((3 / 2) * PI ) + T(i)) - T(i)) by A1, XREAL_1: 9;

      

       A4: ( sin r) >= ( - 1) by Th3;

      ( sin (r - T(i))) = ( sin (r + T(-)))

      .= ( sin r) by COMPLEX2: 8

      .= ( - 1) by A2, A4, XXREAL_0: 1;

      hence thesis by A3, Th31;

    end;

    theorem :: SIN_COS6:39

    (((3 / 2) * PI ) + ((2 * PI ) * i)) < r & r <= ((2 * PI ) + ((2 * PI ) * i)) implies ( sin r) > ( - 1)

    proof

      assume that

       A1: (((3 / 2) * PI ) + T(i)) < r & r <= ((2 * PI ) + T(i)) and

       A2: ( sin r) <= ( - 1);

      

       A3: ((((3 / 2) * PI ) + T(i)) - T(i)) < (r - T(i)) & (r - T(i)) <= (((2 * PI ) + T(i)) - T(i)) by A1, XREAL_1: 9;

      

       A4: ( sin r) >= ( - 1) by Th3;

      ( sin (r - T(i))) = ( sin (r + T(-)))

      .= ( sin r) by COMPLEX2: 8

      .= ( - 1) by A2, A4, XXREAL_0: 1;

      hence thesis by A3, Th32;

    end;

    theorem :: SIN_COS6:40

    (( PI / 2) + ((2 * PI ) * i)) < r & r <= ((2 * PI ) + ((2 * PI ) * i)) implies ( sin r) < 1

    proof

      assume that

       A1: (( PI / 2) + T(i)) < r & r <= ((2 * PI ) + T(i)) and

       A2: ( sin r) >= 1;

      

       A3: ((( PI / 2) + T(i)) - T(i)) < (r - T(i)) & (r - T(i)) <= (((2 * PI ) + T(i)) - T(i)) by A1, XREAL_1: 9;

      

       A4: ( sin r) <= 1 by Th4;

      ( sin (r - T(i))) = ( sin (r + T(-)))

      .= ( sin r) by COMPLEX2: 8

      .= 1 by A2, A4, XXREAL_0: 1;

      hence thesis by A3, Th33;

    end;

    theorem :: SIN_COS6:41

    ((2 * PI ) * i) < r & r < ((2 * PI ) + ((2 * PI ) * i)) implies ( cos r) < 1

    proof

      assume that

       A1: T(i) < r & r < ((2 * PI ) + T(i)) and

       A2: ( cos r) >= 1;

      

       A3: ( T(i) - T(i)) < (r - T(i)) & (r - T(i)) < (((2 * PI ) + T(i)) - T(i)) by A1, XREAL_1: 9;

      

       A4: ( cos r) <= 1 by Th6;

      ( cos (r - T(i))) = ( cos (r + T(-)))

      .= ( cos r) by COMPLEX2: 9

      .= 1 by A2, A4, XXREAL_0: 1;

      hence thesis by A3, Th34;

    end;

    theorem :: SIN_COS6:42

    ((2 * PI ) * i) <= r & r < ( PI + ((2 * PI ) * i)) implies ( cos r) > ( - 1)

    proof

      assume that

       A1: T(i) <= r & r < ( PI + T(i)) and

       A2: ( cos r) <= ( - 1);

      

       A3: ( T(i) - T(i)) <= (r - T(i)) & (r - T(i)) < (( PI + T(i)) - T(i)) by A1, XREAL_1: 9;

      

       A4: ( cos r) >= ( - 1) by Th5;

      ( cos (r - T(i))) = ( cos (r + T(-)))

      .= ( cos r) by COMPLEX2: 9

      .= ( - 1) by A2, A4, XXREAL_0: 1;

      hence thesis by A3, Th35;

    end;

    theorem :: SIN_COS6:43

    ( PI + ((2 * PI ) * i)) < r & r <= ((2 * PI ) + ((2 * PI ) * i)) implies ( cos r) > ( - 1)

    proof

      assume that

       A1: ( PI + T(i)) < r & r <= ((2 * PI ) + T(i)) and

       A2: ( cos r) <= ( - 1);

      

       A3: (( PI + T(i)) - T(i)) < (r - T(i)) & (r - T(i)) <= (((2 * PI ) + T(i)) - T(i)) by A1, XREAL_1: 9;

      

       A4: ( cos r) >= ( - 1) by Th5;

      ( cos (r - T(i))) = ( cos (r + T(-)))

      .= ( cos r) by COMPLEX2: 9

      .= ( - 1) by A2, A4, XXREAL_0: 1;

      hence thesis by A3, Th36;

    end;

    theorem :: SIN_COS6:44

    ( cos ((2 * PI ) * r)) = 1 implies r in INT

    proof

      reconsider d = 2 as positive Real;

      assume

       A1: ( cos ((2 * PI ) * r)) = 1;

      assume not r in INT ;

      then not r is integer by INT_1:def 2;

      then

      reconsider t = ( frac r) as positive Real by INT_1: 46;

      set s = [\r/];

      

       A2: r = (s + t) & ((d * PI ) * t) < ((d * PI ) * 1) by INT_1: 42, INT_1: 43, XREAL_1: 68;

      ( cos ((2 * PI ) * (s + t))) = ( cos (((2 * PI ) * s) + ((2 * PI ) * t)))

      .= ( cos ((2 * PI ) * t)) by COMPLEX2: 9;

      hence contradiction by A1, A2, Th34;

    end;

    theorem :: SIN_COS6:45

    

     Th45: ( sin .: [.( - ( PI / 2)), ( PI / 2).]) = [.( - 1), 1.] by COMPTRIG: 30, RELAT_1: 115;

    theorem :: SIN_COS6:46

    

     Th46: ( sin .: ].( - ( PI / 2)), ( PI / 2).[) = ].( - 1), 1.[

    proof

      ( sin | ].( - ( PI / 2)), ( PI / 2).[) c= ( sin | [.( - ( PI / 2)), ( PI / 2).]) by RELAT_1: 75, XXREAL_1: 25;

      then

       A1: ( rng ( sin | ].( - ( PI / 2)), ( PI / 2).[)) c= ( rng ( sin | [.( - ( PI / 2)), ( PI / 2).])) by RELAT_1: 11;

      

       A2: ( rng ( sin | ].( - ( PI / 2)), ( PI / 2).[)) = ( sin .: ].( - ( PI / 2)), ( PI / 2).[) by RELAT_1: 115;

      thus ( sin .: ].( - ( PI / 2)), ( PI / 2).[) c= ].( - 1), 1.[

      proof

        let x be object;

        assume

         A3: x in ( sin .: ].( - ( PI / 2)), ( PI / 2).[);

        then

        consider a be object such that

         A4: a in ( dom sin ) and

         A5: a in ].( - ( PI / 2)), ( PI / 2).[ and

         A6: ( sin . a) = x by FUNCT_1:def 6;

        reconsider a, x as Real by A4, A6;

        set i = [\(a / (2 * PI ))/];

        

         A7: ( T(i) / ((2 * PI ) * 1)) = (i / 1) by XCMPLX_1: 91;

        

         A8: ( sin . a) = ( sin a) by SIN_COS:def 17;

         A9:

        now

          assume x = 1;

          then

           A10: a = (( PI / 2) + T(i)) by A6, A8, Th24;

          then (( PI / 2) + T(i)) < ( PI / 2) by A5, XXREAL_1: 4;

          then ((( PI / 2) + T(i)) - ( PI / 2)) < (( PI / 2) - ( PI / 2)) by XREAL_1: 9;

          then i < 0 ;

          then

           A11: i <= ( - 1) by INT_1: 8;

          ( - ( PI / 2)) < (( PI / 2) + T(i)) by A5, A10, XXREAL_1: 4;

          then (( - ( PI / 2)) - ( PI / 2)) < ((( PI / 2) + T(i)) - ( PI / 2)) by XREAL_1: 9;

          then ((( - 1) * PI ) / (2 * PI )) < i by A7, XREAL_1: 74;

          then (( - 1) / 2) < i by XCMPLX_1: 91;

          hence contradiction by A11, XXREAL_0: 2;

        end;

         A12:

        now

          assume x = ( - 1);

          then

           A13: a = (((3 / 2) * PI ) + T(i)) by A6, A8, Th23;

          then ( - ( PI / 2)) < (((3 / 2) * PI ) + T(i)) by A5, XXREAL_1: 4;

          then (( - ( PI / 2)) - ((3 / 2) * PI )) < ((((3 / 2) * PI ) + T(i)) - ((3 / 2) * PI )) by XREAL_1: 9;

          then (( - (2 * PI )) / (2 * PI )) < i by A7, XREAL_1: 74;

          then ( - ((2 * PI ) / (2 * PI ))) < i by XCMPLX_1: 187;

          then ( - 1) < i by XCMPLX_1: 60;

          then

           A14: (( - 1) + 1) <= i by INT_1: 7;

          (((3 / 2) * PI ) + T(i)) < ( PI / 2) by A5, A13, XXREAL_1: 4;

          then ((((3 / 2) * PI ) + T(i)) - ((3 / 2) * PI )) < (( PI / 2) - ((3 / 2) * PI )) by XREAL_1: 9;

          then i < (( - PI ) / (2 * PI )) by A7, XREAL_1: 74;

          hence contradiction by A14, XCMPLX_1: 91;

        end;

        x <= 1 by A1, A2, A3, COMPTRIG: 30, XXREAL_1: 1;

        then

         A15: x < 1 by A9, XXREAL_0: 1;

        ( - 1) <= x by A1, A2, A3, COMPTRIG: 30, XXREAL_1: 1;

        then ( - 1) < x by A12, XXREAL_0: 1;

        hence thesis by A15, XXREAL_1: 4;

      end;

      let a be object;

      assume

       A16: a in ].( - 1), 1.[;

      then

      reconsider a as Real;

      ( - 1) < a & a < 1 by A16, XXREAL_1: 4;

      then a in ( rng ( sin | [.( - ( PI / 2)), ( PI / 2).])) by COMPTRIG: 30, XXREAL_1: 1;

      then

      consider x be object such that

       A17: x in ( dom ( sin | [.( - ( PI / 2)), ( PI / 2).])) and

       A18: (( sin | [.( - ( PI / 2)), ( PI / 2).]) . x) = a by FUNCT_1:def 3;

      reconsider x as Real by A17;

      

       A19: ( sin . x) = a by A17, A18, FUNCT_1: 47;

      ( dom ( sin | [.( - ( PI / 2)), ( PI / 2).])) = [.( - ( PI / 2)), ( PI / 2).] by RELAT_1: 62, SIN_COS: 24;

      then ( - ( PI / 2)) <= x & x <= ( PI / 2) by A17, XXREAL_1: 1;

      then ( - ( PI / 2)) < x & x < ( PI / 2) or ( - ( PI / 2)) = x or ( PI / 2) = x by XXREAL_0: 1;

      then x in ].( - ( PI / 2)), ( PI / 2).[ by A16, A19, Th7, SIN_COS: 76, XXREAL_1: 4;

      hence thesis by A19, FUNCT_1:def 6, SIN_COS: 24;

    end;

    theorem :: SIN_COS6:47

    ( sin .: [.( PI / 2), ((3 / 2) * PI ).]) = [.( - 1), 1.] by COMPTRIG: 31, RELAT_1: 115;

    theorem :: SIN_COS6:48

    ( sin .: ].( PI / 2), ((3 / 2) * PI ).[) = ].( - 1), 1.[

    proof

      ( sin | ].( PI / 2), ((3 / 2) * PI ).[) c= ( sin | [.( PI / 2), ((3 / 2) * PI ).]) by RELAT_1: 75, XXREAL_1: 25;

      then

       A1: ( rng ( sin | ].( PI / 2), ((3 / 2) * PI ).[)) c= ( rng ( sin | [.( PI / 2), ((3 / 2) * PI ).])) by RELAT_1: 11;

      

       A2: ( rng ( sin | ].( PI / 2), ((3 / 2) * PI ).[)) = ( sin .: ].( PI / 2), ((3 / 2) * PI ).[) by RELAT_1: 115;

      thus ( sin .: ].( PI / 2), ((3 / 2) * PI ).[) c= ].( - 1), 1.[

      proof

        let x be object;

        assume

         A3: x in ( sin .: ].( PI / 2), ((3 / 2) * PI ).[);

        then

        consider a be object such that

         A4: a in ( dom sin ) and

         A5: a in ].( PI / 2), ((3 / 2) * PI ).[ and

         A6: ( sin . a) = x by FUNCT_1:def 6;

        reconsider a, x as Real by A4, A6;

        set i = [\(a / (2 * PI ))/];

        

         A7: ( T(i) / ((2 * PI ) * 1)) = (i / 1) by XCMPLX_1: 91;

        

         A8: ( sin . a) = ( sin a) by SIN_COS:def 17;

         A9:

        now

          assume x = 1;

          then

           A10: a = (( PI / 2) + T(i)) by A6, A8, Th24;

          then ( PI / 2) < (( PI / 2) + T(i)) by A5, XXREAL_1: 4;

          then (( PI / 2) - ( PI / 2)) < ((( PI / 2) + T(i)) - ( PI / 2)) by XREAL_1: 9;

          then 0 < i;

          then

           A11: ( 0 + 1) <= i by INT_1: 7;

          (( PI / 2) + T(i)) < ((3 / 2) * PI ) by A5, A10, XXREAL_1: 4;

          then ((( PI / 2) + T(i)) - ( PI / 2)) < (((3 / 2) * PI ) - ( PI / 2)) by XREAL_1: 9;

          then i < ((1 * PI ) / (2 * PI )) by A7, XREAL_1: 74;

          then i < (1 / 2) by XCMPLX_1: 91;

          hence contradiction by A11, XXREAL_0: 2;

        end;

         A12:

        now

          assume x = ( - 1);

          then

           A13: a = (((3 / 2) * PI ) + T(i)) by A6, A8, Th23;

          then (((3 / 2) * PI ) + T(i)) < ((3 / 2) * PI ) by A5, XXREAL_1: 4;

          then ((((3 / 2) * PI ) + T(i)) - ((3 / 2) * PI )) < (((3 / 2) * PI ) - ((3 / 2) * PI )) by XREAL_1: 9;

          then i < 0 ;

          then

           A14: i <= ( - 1) by INT_1: 8;

          ( PI / 2) < (((3 / 2) * PI ) + T(i)) by A5, A13, XXREAL_1: 4;

          then (( PI / 2) - ((3 / 2) * PI )) < ((((3 / 2) * PI ) + T(i)) - ((3 / 2) * PI )) by XREAL_1: 9;

          then ((( - 1) * PI ) / (2 * PI )) < i by A7, XREAL_1: 74;

          then (( - 1) / 2) < i by XCMPLX_1: 91;

          hence contradiction by A14, XXREAL_0: 2;

        end;

        x <= 1 by A1, A2, A3, COMPTRIG: 31, XXREAL_1: 1;

        then

         A15: x < 1 by A9, XXREAL_0: 1;

        ( - 1) <= x by A1, A2, A3, COMPTRIG: 31, XXREAL_1: 1;

        then ( - 1) < x by A12, XXREAL_0: 1;

        hence thesis by A15, XXREAL_1: 4;

      end;

      let a be object;

      assume

       A16: a in ].( - 1), 1.[;

      then

      reconsider a as Real;

      ( - 1) < a & a < 1 by A16, XXREAL_1: 4;

      then a in ( rng ( sin | [.( PI / 2), ((3 / 2) * PI ).])) by COMPTRIG: 31, XXREAL_1: 1;

      then

      consider x be object such that

       A17: x in ( dom ( sin | [.( PI / 2), ((3 / 2) * PI ).])) and

       A18: (( sin | [.( PI / 2), ((3 / 2) * PI ).]) . x) = a by FUNCT_1:def 3;

      reconsider x as Real by A17;

      

       A19: ( sin . x) = a by A17, A18, FUNCT_1: 47;

      ( dom ( sin | [.( PI / 2), ((3 / 2) * PI ).])) = [.( PI / 2), ((3 / 2) * PI ).] by RELAT_1: 62, SIN_COS: 24;

      then ( PI / 2) <= x & x <= ((3 / 2) * PI ) by A17, XXREAL_1: 1;

      then ( PI / 2) < x & x < ((3 / 2) * PI ) or ( PI / 2) = x or ((3 / 2) * PI ) = x by XXREAL_0: 1;

      then x in ].( PI / 2), ((3 / 2) * PI ).[ by A16, A19, SIN_COS: 76, XXREAL_1: 4;

      hence thesis by A19, FUNCT_1:def 6, SIN_COS: 24;

    end;

    theorem :: SIN_COS6:49

    

     Th49: ( cos .: [. 0 , PI .]) = [.( - 1), 1.] by COMPTRIG: 32, RELAT_1: 115;

    theorem :: SIN_COS6:50

    

     Th50: ( cos .: ]. 0 , PI .[) = ].( - 1), 1.[

    proof

      ( cos | ]. 0 , PI .[) c= ( cos | [. 0 , PI .]) by RELAT_1: 75, XXREAL_1: 25;

      then

       A1: ( rng ( cos | ]. 0 , PI .[)) c= ( rng ( cos | [. 0 , PI .])) by RELAT_1: 11;

      

       A2: ( rng ( cos | ]. 0 , PI .[)) = ( cos .: ]. 0 , PI .[) by RELAT_1: 115;

      thus ( cos .: ]. 0 , PI .[) c= ].( - 1), 1.[

      proof

        let x be object;

        assume

         A3: x in ( cos .: ]. 0 , PI .[);

        then

        consider a be object such that

         A4: a in ( dom cos ) and

         A5: a in ]. 0 , PI .[ and

         A6: ( cos . a) = x by FUNCT_1:def 6;

        reconsider a, x as Real by A4, A6;

        set i = [\(a / (2 * PI ))/];

        

         A7: ( T(i) / ((2 * PI ) * 1)) = (i / 1) by XCMPLX_1: 91;

        

         A8: ( cos . a) = ( cos a) by SIN_COS:def 19;

         A9:

        now

          assume x = 1;

          then

           A10: a = T(i) by A6, A8, Th26;

          then T(i) < PI by A5, XXREAL_1: 4;

          then i < ((1 * PI ) / (2 * PI )) by A7, XREAL_1: 74;

          then

           A11: i < (1 / 2) by XCMPLX_1: 91;

           0 < i by A5, A10, XXREAL_1: 4;

          then ( 0 + 1) <= i by INT_1: 7;

          hence contradiction by A11, XXREAL_0: 2;

        end;

         A12:

        now

          assume x = ( - 1);

          then

           A13: a = ( PI + T(i)) by A6, A8, Th25;

          then 0 < ( PI + T(i)) by A5, XXREAL_1: 4;

          then ( 0 - PI ) < (( PI + T(i)) - PI ) by XREAL_1: 9;

          then (( - PI ) / (2 * PI )) < ( T(i) / (2 * PI )) by XREAL_1: 74;

          then ( - ((1 * PI ) / (2 * PI ))) < i by A7, XCMPLX_1: 187;

          then

           A14: ( - (1 / 2)) < i by XCMPLX_1: 91;

          ( PI + T(i)) < PI by A5, A13, XXREAL_1: 4;

          then (( PI + T(i)) - PI ) < ( PI - PI ) by XREAL_1: 9;

          then i < 0 ;

          then i <= ( - 1) by INT_1: 8;

          hence contradiction by A14, XXREAL_0: 2;

        end;

        x <= 1 by A1, A2, A3, COMPTRIG: 32, XXREAL_1: 1;

        then

         A15: x < 1 by A9, XXREAL_0: 1;

        ( - 1) <= x by A1, A2, A3, COMPTRIG: 32, XXREAL_1: 1;

        then ( - 1) < x by A12, XXREAL_0: 1;

        hence thesis by A15, XXREAL_1: 4;

      end;

      let a be object;

      assume

       A16: a in ].( - 1), 1.[;

      then

      reconsider a as Real;

      ( - 1) < a & a < 1 by A16, XXREAL_1: 4;

      then a in ( rng ( cos | [. 0 , PI .])) by COMPTRIG: 32, XXREAL_1: 1;

      then

      consider x be object such that

       A17: x in ( dom ( cos | [. 0 , PI .])) and

       A18: (( cos | [. 0 , PI .]) . x) = a by FUNCT_1:def 3;

      reconsider x as Real by A17;

      

       A19: ( cos . x) = a by A17, A18, FUNCT_1: 47;

      

       A20: ( dom ( cos | [. 0 , PI .])) = [. 0 , PI .] by RELAT_1: 62, SIN_COS: 24;

      then x <= PI by A17, XXREAL_1: 1;

      then 0 < x & x < PI or 0 = x or PI = x by A17, A20, XXREAL_0: 1, XXREAL_1: 1;

      then x in ]. 0 , PI .[ by A16, A19, SIN_COS: 30, SIN_COS: 76, XXREAL_1: 4;

      hence thesis by A19, FUNCT_1:def 6, SIN_COS: 24;

    end;

    theorem :: SIN_COS6:51

    ( cos .: [. PI , (2 * PI ).]) = [.( - 1), 1.] by COMPTRIG: 33, RELAT_1: 115;

    theorem :: SIN_COS6:52

    ( cos .: ]. PI , (2 * PI ).[) = ].( - 1), 1.[

    proof

      ( cos | ]. PI , (2 * PI ).[) c= ( cos | [. PI , (2 * PI ).]) by RELAT_1: 75, XXREAL_1: 25;

      then

       A1: ( rng ( cos | ]. PI , (2 * PI ).[)) c= ( rng ( cos | [. PI , (2 * PI ).])) by RELAT_1: 11;

      

       A2: ( rng ( cos | ]. PI , (2 * PI ).[)) = ( cos .: ]. PI , (2 * PI ).[) by RELAT_1: 115;

      thus ( cos .: ]. PI , (2 * PI ).[) c= ].( - 1), 1.[

      proof

        let x be object;

        assume

         A3: x in ( cos .: ]. PI , (2 * PI ).[);

        then

        consider a be object such that

         A4: a in ( dom cos ) and

         A5: a in ]. PI , (2 * PI ).[ and

         A6: ( cos . a) = x by FUNCT_1:def 6;

        reconsider a, x as Real by A4, A6;

        set i = [\(a / (2 * PI ))/];

        

         A7: ( T(i) / ((2 * PI ) * 1)) = (i / 1) by XCMPLX_1: 91;

        

         A8: ( cos . a) = ( cos a) by SIN_COS:def 19;

         A9:

        now

          assume x = 1;

          then

           A10: a = T(i) by A6, A8, Th26;

          then T(i) < (2 * PI ) by A5, XXREAL_1: 4;

          then i < ((2 * PI ) / (2 * PI )) by A7, XREAL_1: 74;

          then

           A11: i < (1 + 0 ) by XCMPLX_1: 60;

           PI < T(i) by A5, A10, XXREAL_1: 4;

          hence contradiction by A7, A11, INT_1: 7;

        end;

         A12:

        now

          assume x = ( - 1);

          then

           A13: a = ( PI + T(i)) by A6, A8, Th25;

          then PI < ( PI + T(i)) by A5, XXREAL_1: 4;

          then ( PI - PI ) < (( PI + T(i)) - PI ) by XREAL_1: 9;

          then ( 0 / (2 * PI )) < i;

          then

           A14: ( 0 + 1) <= i by INT_1: 7;

          ( PI + T(i)) < (2 * PI ) by A5, A13, XXREAL_1: 4;

          then (( PI + T(i)) - PI ) < ((2 * PI ) - PI ) by XREAL_1: 9;

          then i < ((1 * PI ) / (2 * PI )) by A7, XREAL_1: 74;

          then i <= (1 / 2) by XCMPLX_1: 91;

          hence contradiction by A14, XXREAL_0: 2;

        end;

        x <= 1 by A1, A2, A3, COMPTRIG: 33, XXREAL_1: 1;

        then

         A15: x < 1 by A9, XXREAL_0: 1;

        ( - 1) <= x by A1, A2, A3, COMPTRIG: 33, XXREAL_1: 1;

        then ( - 1) < x by A12, XXREAL_0: 1;

        hence thesis by A15, XXREAL_1: 4;

      end;

      let a be object;

      assume

       A16: a in ].( - 1), 1.[;

      then

      reconsider a as Real;

      ( - 1) < a & a < 1 by A16, XXREAL_1: 4;

      then a in ( rng ( cos | [. PI , (2 * PI ).])) by COMPTRIG: 33, XXREAL_1: 1;

      then

      consider x be object such that

       A17: x in ( dom ( cos | [. PI , (2 * PI ).])) and

       A18: (( cos | [. PI , (2 * PI ).]) . x) = a by FUNCT_1:def 3;

      reconsider x as Real by A17;

      

       A19: ( cos . x) = a by A17, A18, FUNCT_1: 47;

      ( dom ( cos | [. PI , (2 * PI ).])) = [. PI , (2 * PI ).] by RELAT_1: 62, SIN_COS: 24;

      then PI <= x & x <= (2 * PI ) by A17, XXREAL_1: 1;

      then PI < x & x < (2 * PI ) or PI = x or (2 * PI ) = x by XXREAL_0: 1;

      then x in ]. PI , (2 * PI ).[ by A16, A19, SIN_COS: 76, XXREAL_1: 4;

      hence thesis by A19, FUNCT_1:def 6, SIN_COS: 24;

    end;

     Lm11:

    now

      let i, r;

      let p1,p2 be Real;

      assume

       A1: r in [.(p1 + T(i)), (p2 + T(i)).];

      then r <= (p2 + T(i)) by XXREAL_1: 1;

      then

       A2: (r + (2 * PI )) <= ((p2 + T(i)) + (2 * PI )) by XREAL_1: 6;

      (p1 + T(i)) <= r by A1, XXREAL_1: 1;

      then ((p1 + T(i)) + (2 * PI )) <= (r + (2 * PI )) by XREAL_1: 6;

      hence (r + (2 * PI )) in [.(p1 + T(+)), (p2 + T(+)).] by A2, XXREAL_1: 1;

    end;

     Lm12:

    now

      let i, r;

      let p1,p2 be Real;

      assume r in ( [.(p1 + T(i)), (p2 + T(i)).] /\ REAL );

      then r in [.(p1 + T(i)), (p2 + T(i)).] by XBOOLE_0:def 4;

      then (r + (2 * PI )) in [.(p1 + T(+)), (p2 + T(+)).] by Lm11;

      hence (r + (2 * PI )) in ( [.(p1 + T(+)), (p2 + T(+)).] /\ REAL ) by XBOOLE_0:def 4;

    end;

     Lm13:

    now

      let i, r;

      let p1,p2 be Real;

      assume

       A1: r in [.(p1 + T(i)), (p2 + T(i)).];

      then r <= (p2 + T(i)) by XXREAL_1: 1;

      then

       A2: (r - (2 * PI )) <= ((p2 + T(i)) - (2 * PI )) by XREAL_1: 9;

      (p1 + T(i)) <= r by A1, XXREAL_1: 1;

      then ((p1 + T(i)) - (2 * PI )) <= (r - (2 * PI )) by XREAL_1: 9;

      hence (r - (2 * PI )) in [.(p1 + T(-)), (p2 + T(-)).] by A2, XXREAL_1: 1;

    end;

     Lm14:

    now

      let i, r;

      let p1,p2 be Real;

      assume r in ( [.(p1 + T(i)), (p2 + T(i)).] /\ REAL );

      then r in [.(p1 + T(i)), (p2 + T(i)).] by XBOOLE_0:def 4;

      then (r - (2 * PI )) in [.(p1 + T(-)), (p2 + T(-)).] by Lm13;

      hence (r - (2 * PI )) in ( [.(p1 + T(-)), (p2 + T(-)).] /\ REAL ) by XBOOLE_0:def 4;

    end;

    theorem :: SIN_COS6:53

    

     Th53: ( sin | [.(( - ( PI / 2)) + ((2 * PI ) * i)), (( PI / 2) + ((2 * PI ) * i)).]) is increasing

    proof

      defpred P[ Integer] means ( sin | [.(( - ( PI / 2)) + T($1)), (( PI / 2) + T($1)).]) is increasing;

      

       A1: for i holds P[i] implies P[(i - 1)] & P[(i + 1)]

      proof

        let i such that

         A2: P[i];

        set Z = [.(( - ( PI / 2)) + T(+)), (( PI / 2) + T(+)).];

        thus P[(i - 1)]

        proof

          set Y = [.(( - ( PI / 2)) + T(-)), (( PI / 2) + T(-)).];

          now

            let r1, r2;

            assume r1 in (Y /\ ( dom sin )) & r2 in (Y /\ ( dom sin ));

            then

             A3: (r1 + (2 * PI )) in (Z /\ ( dom sin )) & (r2 + (2 * PI )) in (Z /\ ( dom sin )) by Lm12, SIN_COS: 24;

            assume r1 < r2;

            then (r1 + (2 * PI )) < (r2 + (2 * PI )) by XREAL_1: 6;

            then ( sin . (r1 + (2 * PI ))) < ( sin . (r2 + ((2 * PI ) * 1))) by A2, A3, RFUNCT_2: 20;

            then ( sin . (r1 + ((2 * PI ) * 1))) < ( sin . r2) by Th8;

            hence ( sin . r1) < ( sin . r2) by Th8;

          end;

          hence thesis by RFUNCT_2: 20;

        end;

        set Y = [.(( - ( PI / 2)) + T(+)), (( PI / 2) + T(+)).];

        

         A4: Z = [.(( - ( PI / 2)) + T(-)), (( PI / 2) + T(-)).];

        now

          let r1, r2;

          assume r1 in (Y /\ ( dom sin )) & r2 in (Y /\ ( dom sin ));

          then

           A5: (r1 - (2 * PI )) in (Z /\ ( dom sin )) & (r2 - (2 * PI )) in (Z /\ ( dom sin )) by A4, Lm14, SIN_COS: 24;

          assume r1 < r2;

          then (r1 - (2 * PI )) < (r2 - (2 * PI )) by XREAL_1: 9;

          then ( sin . (r1 - (2 * PI ))) < ( sin . (r2 + ((2 * PI ) * ( - 1)))) by A2, A5, RFUNCT_2: 20;

          then ( sin . (r1 + ((2 * PI ) * ( - 1)))) < ( sin . r2) by Th8;

          hence ( sin . r1) < ( sin . r2) by Th8;

        end;

        hence thesis by RFUNCT_2: 20;

      end;

      

       A6: P[ 0 ] by COMPTRIG: 23;

      for i holds P[i] from INT_1:sch 4( A6, A1);

      hence thesis;

    end;

    theorem :: SIN_COS6:54

    

     Th54: ( sin | [.(( PI / 2) + ((2 * PI ) * i)), (((3 / 2) * PI ) + ((2 * PI ) * i)).]) is decreasing

    proof

      defpred P[ Integer] means ( sin | [.(( PI / 2) + T($1)), (((3 / 2) * PI ) + T($1)).]) is decreasing;

      

       A1: for i holds P[i] implies P[(i - 1)] & P[(i + 1)]

      proof

        let i such that

         A2: P[i];

        set Z = [.(( PI / 2) + T(+)), (((3 / 2) * PI ) + T(+)).];

        thus P[(i - 1)]

        proof

          set Y = [.(( PI / 2) + T(-)), (((3 / 2) * PI ) + T(-)).];

          now

            let r1, r2;

            assume r1 in (Y /\ ( dom sin )) & r2 in (Y /\ ( dom sin ));

            then

             A3: (r1 + (2 * PI )) in (Z /\ ( dom sin )) & (r2 + (2 * PI )) in (Z /\ ( dom sin )) by Lm12, SIN_COS: 24;

            assume r1 < r2;

            then (r1 + (2 * PI )) < (r2 + (2 * PI )) by XREAL_1: 6;

            then ( sin . (r1 + (2 * PI ))) > ( sin . (r2 + ((2 * PI ) * 1))) by A2, A3, RFUNCT_2: 21;

            then ( sin . (r1 + ((2 * PI ) * 1))) > ( sin . r2) by Th8;

            hence ( sin . r1) > ( sin . r2) by Th8;

          end;

          hence thesis by RFUNCT_2: 21;

        end;

        set Y = [.(( PI / 2) + T(+)), (((3 / 2) * PI ) + T(+)).];

        

         A4: Z = [.(( PI / 2) + T(-)), (((3 / 2) * PI ) + T(-)).];

        now

          let r1, r2;

          assume r1 in (Y /\ ( dom sin )) & r2 in (Y /\ ( dom sin ));

          then

           A5: (r1 - (2 * PI )) in (Z /\ ( dom sin )) & (r2 - (2 * PI )) in (Z /\ ( dom sin )) by A4, Lm14, SIN_COS: 24;

          assume r1 < r2;

          then (r1 - (2 * PI )) < (r2 - (2 * PI )) by XREAL_1: 9;

          then ( sin . (r1 - (2 * PI ))) > ( sin . (r2 + ((2 * PI ) * ( - 1)))) by A2, A5, RFUNCT_2: 21;

          then ( sin . (r1 + ((2 * PI ) * ( - 1)))) > ( sin . r2) by Th8;

          hence ( sin . r1) > ( sin . r2) by Th8;

        end;

        hence thesis by RFUNCT_2: 21;

      end;

      

       A6: P[ 0 ] by COMPTRIG: 24;

      for i holds P[i] from INT_1:sch 4( A6, A1);

      hence thesis;

    end;

    theorem :: SIN_COS6:55

    

     Th55: ( cos | [.((2 * PI ) * i), ( PI + ((2 * PI ) * i)).]) is decreasing

    proof

      defpred P[ Integer] means ( cos | [. T($1), ( PI + T($1)).]) is decreasing;

      

       A1: for i holds P[i] implies P[(i - 1)] & P[(i + 1)]

      proof

        let i such that

         A2: P[i];

        set Z = [.( 0 + T(+)), ( PI + T(+)).];

        thus P[(i - 1)]

        proof

          set Y = [. T(-), ( PI + T(-)).];

          

           A3: Y = [.( 0 + T(-)), ( PI + T(-)).];

          now

            let r1, r2;

            assume r1 in (Y /\ ( dom cos )) & r2 in (Y /\ ( dom cos ));

            then

             A4: (r1 + (2 * PI )) in (Z /\ ( dom cos )) & (r2 + (2 * PI )) in (Z /\ ( dom cos )) by A3, Lm12, SIN_COS: 24;

            assume r1 < r2;

            then (r1 + (2 * PI )) < (r2 + (2 * PI )) by XREAL_1: 6;

            then ( cos . (r1 + (2 * PI ))) > ( cos . (r2 + ((2 * PI ) * 1))) by A2, A4, RFUNCT_2: 21;

            then ( cos . (r1 + ((2 * PI ) * 1))) > ( cos . r2) by Th10;

            hence ( cos . r1) > ( cos . r2) by Th10;

          end;

          hence thesis by RFUNCT_2: 21;

        end;

        set Y = [. T(+), ( PI + T(+)).];

        

         A5: Y = [.( 0 + T(+)), ( PI + T(+)).] & Z = [. T(-), ( PI + T(-)).];

        now

          let r1, r2;

          assume r1 in (Y /\ ( dom cos )) & r2 in (Y /\ ( dom cos ));

          then

           A6: (r1 - (2 * PI )) in (Z /\ ( dom cos )) & (r2 - (2 * PI )) in (Z /\ ( dom cos )) by A5, Lm14, SIN_COS: 24;

          assume r1 < r2;

          then (r1 - (2 * PI )) < (r2 - (2 * PI )) by XREAL_1: 9;

          then ( cos . (r1 - (2 * PI ))) > ( cos . (r2 + ((2 * PI ) * ( - 1)))) by A2, A6, RFUNCT_2: 21;

          then ( cos . (r1 + ((2 * PI ) * ( - 1)))) > ( cos . r2) by Th10;

          hence ( cos . r1) > ( cos . r2) by Th10;

        end;

        hence thesis by RFUNCT_2: 21;

      end;

      

       A7: P[ 0 ] by COMPTRIG: 25;

      for i holds P[i] from INT_1:sch 4( A7, A1);

      hence thesis;

    end;

    theorem :: SIN_COS6:56

    

     Th56: ( cos | [.( PI + ((2 * PI ) * i)), ((2 * PI ) + ((2 * PI ) * i)).]) is increasing

    proof

      defpred P[ Integer] means ( cos | [.( PI + T($1)), ((2 * PI ) + T($1)).]) is increasing;

      

       A1: for i holds P[i] implies P[(i - 1)] & P[(i + 1)]

      proof

        let i such that

         A2: P[i];

        set Z = [.( PI + T(+)), ((2 * PI ) + T(+)).];

        thus P[(i - 1)]

        proof

          set Y = [.( PI + T(-)), ((2 * PI ) + T(-)).];

          now

            let r1, r2;

            assume r1 in (Y /\ ( dom cos )) & r2 in (Y /\ ( dom cos ));

            then

             A3: (r1 + (2 * PI )) in (Z /\ ( dom cos )) & (r2 + (2 * PI )) in (Z /\ ( dom cos )) by Lm12, SIN_COS: 24;

            assume r1 < r2;

            then (r1 + (2 * PI )) < (r2 + (2 * PI )) by XREAL_1: 6;

            then ( cos . (r1 + (2 * PI ))) < ( cos . (r2 + ((2 * PI ) * 1))) by A2, A3, RFUNCT_2: 20;

            then ( cos . (r1 + ((2 * PI ) * 1))) < ( cos . r2) by Th10;

            hence ( cos . r1) < ( cos . r2) by Th10;

          end;

          hence thesis by RFUNCT_2: 20;

        end;

        set Y = [.( PI + T(+)), ((2 * PI ) + T(+)).];

        

         A4: Z = [.( PI + T(-)), ((2 * PI ) + T(-)).];

        now

          let r1, r2;

          assume r1 in (Y /\ ( dom cos )) & r2 in (Y /\ ( dom cos ));

          then

           A5: (r1 - (2 * PI )) in (Z /\ ( dom cos )) & (r2 - (2 * PI )) in (Z /\ ( dom cos )) by A4, Lm14, SIN_COS: 24;

          assume r1 < r2;

          then (r1 - (2 * PI )) < (r2 - (2 * PI )) by XREAL_1: 9;

          then ( cos . (r1 - (2 * PI ))) < ( cos . (r2 + ((2 * PI ) * ( - 1)))) by A2, A5, RFUNCT_2: 20;

          then ( cos . (r1 + ((2 * PI ) * ( - 1)))) < ( cos . r2) by Th10;

          hence ( cos . r1) < ( cos . r2) by Th10;

        end;

        hence thesis by RFUNCT_2: 20;

      end;

      

       A6: P[ 0 ] by COMPTRIG: 26;

      for i holds P[i] from INT_1:sch 4( A6, A1);

      hence thesis;

    end;

    theorem :: SIN_COS6:57

    

     Th57: ( sin | [.(( - ( PI / 2)) + ((2 * PI ) * i)), (( PI / 2) + ((2 * PI ) * i)).]) is one-to-one

    proof

      set Q = [.(( - ( PI / 2)) + ((2 * PI ) * i)), (( PI / 2) + ((2 * PI ) * i)).];

      ( sin | Q) is increasing by Th53;

      hence thesis by FCONT_3: 8;

    end;

    theorem :: SIN_COS6:58

    

     Th58: ( sin | [.(( PI / 2) + ((2 * PI ) * i)), (((3 / 2) * PI ) + ((2 * PI ) * i)).]) is one-to-one

    proof

      set Q = [.(( PI / 2) + ((2 * PI ) * i)), (((3 / 2) * PI ) + ((2 * PI ) * i)).];

      ( sin | Q) is decreasing by Th54;

      hence thesis by FCONT_3: 8;

    end;

    registration

      cluster ( sin | [.( - ( PI / 2)), ( PI / 2).]) -> one-to-one;

      coherence by Lm1, Th57;

      cluster ( sin | [.( PI / 2), ((3 / 2) * PI ).]) -> one-to-one;

      coherence by Lm2, Th58;

    end

    registration

      cluster ( sin | [.( - ( PI / 2)), 0 .]) -> one-to-one;

      coherence

      proof

        ( sin | [.( - ( PI / 2)), ( PI / 2).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 34;

      end;

      cluster ( sin | [. 0 , ( PI / 2).]) -> one-to-one;

      coherence

      proof

        ( sin | [.( - ( PI / 2)), ( PI / 2).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 34;

      end;

      cluster ( sin | [.( PI / 2), PI .]) -> one-to-one;

      coherence

      proof

        ( sin | [.( PI / 2), ((3 / 2) * PI ).]) is one-to-one;

        hence thesis by Lm7, Th2, XXREAL_1: 34;

      end;

      cluster ( sin | [. PI , ((3 / 2) * PI ).]) -> one-to-one;

      coherence

      proof

        ( sin | [.( PI / 2), ((3 / 2) * PI ).]) is one-to-one;

        hence thesis by Lm6, Th2, XXREAL_1: 34;

      end;

      cluster ( sin | [.((3 / 2) * PI ), (2 * PI ).]) -> one-to-one;

      coherence

      proof

        ( sin | [.(( - ( PI / 2)) + T()), (( PI / 2) + T()).]) is one-to-one by Th57;

        hence thesis by Lm8, Th2, XXREAL_1: 34;

      end;

    end

    registration

      cluster ( sin | ].( - ( PI / 2)), ( PI / 2).[) -> one-to-one;

      coherence

      proof

        ( sin | [.( - ( PI / 2)), ( PI / 2).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( sin | ].( PI / 2), ((3 / 2) * PI ).[) -> one-to-one;

      coherence

      proof

        ( sin | [.( PI / 2), ((3 / 2) * PI ).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( sin | ].( - ( PI / 2)), 0 .[) -> one-to-one;

      coherence

      proof

        ( sin | [.( - ( PI / 2)), 0 .]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( sin | ]. 0 , ( PI / 2).[) -> one-to-one;

      coherence

      proof

        ( sin | [. 0 , ( PI / 2).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( sin | ].( PI / 2), PI .[) -> one-to-one;

      coherence

      proof

        ( sin | [.( PI / 2), PI .]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( sin | ]. PI , ((3 / 2) * PI ).[) -> one-to-one;

      coherence

      proof

        ( sin | [. PI , ((3 / 2) * PI ).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( sin | ].((3 / 2) * PI ), (2 * PI ).[) -> one-to-one;

      coherence

      proof

        ( sin | [.((3 / 2) * PI ), (2 * PI ).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

    end

    theorem :: SIN_COS6:59

    

     Th59: ( cos | [.((2 * PI ) * i), ( PI + ((2 * PI ) * i)).]) is one-to-one

    proof

      set Q1 = [.((2 * PI ) * i), ( PI + ((2 * PI ) * i)).];

      ( cos | Q1) is decreasing by Th55;

      hence thesis by FCONT_3: 8;

    end;

    theorem :: SIN_COS6:60

    

     Th60: ( cos | [.( PI + ((2 * PI ) * i)), ((2 * PI ) + ((2 * PI ) * i)).]) is one-to-one

    proof

      set Q1 = [.( PI + ((2 * PI ) * i)), ((2 * PI ) + ((2 * PI ) * i)).];

      ( cos | Q1) is increasing by Th56;

      hence thesis by FCONT_3: 8;

    end;

    registration

      cluster ( cos | [. 0 , PI .]) -> one-to-one;

      coherence by Lm3, Th59;

      cluster ( cos | [. PI , (2 * PI ).]) -> one-to-one;

      coherence by Lm4, Th60;

    end

    registration

      cluster ( cos | [. 0 , ( PI / 2).]) -> one-to-one;

      coherence

      proof

        ( cos | [. 0 , PI .]) is one-to-one;

        hence thesis by Lm6, Th2, XXREAL_1: 34;

      end;

      cluster ( cos | [.( PI / 2), PI .]) -> one-to-one;

      coherence

      proof

        ( cos | [. 0 , PI .]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 34;

      end;

      cluster ( cos | [. PI , ((3 / 2) * PI ).]) -> one-to-one;

      coherence

      proof

        ( cos | [. PI , (2 * PI ).]) is one-to-one;

        hence thesis by Lm9, Th2, XXREAL_1: 34;

      end;

      cluster ( cos | [.((3 / 2) * PI ), (2 * PI ).]) -> one-to-one;

      coherence

      proof

        ( cos | [. PI , (2 * PI ).]) is one-to-one;

        hence thesis by Lm7, Th2, XXREAL_1: 34;

      end;

    end

    registration

      cluster ( cos | ]. 0 , PI .[) -> one-to-one;

      coherence

      proof

        ( cos | [. 0 , PI .]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( cos | ]. PI , (2 * PI ).[) -> one-to-one;

      coherence

      proof

        ( cos | [. PI , (2 * PI ).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( cos | ]. 0 , ( PI / 2).[) -> one-to-one;

      coherence

      proof

        ( cos | [. 0 , ( PI / 2).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( cos | ].( PI / 2), PI .[) -> one-to-one;

      coherence

      proof

        ( cos | [.( PI / 2), PI .]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( cos | ]. PI , ((3 / 2) * PI ).[) -> one-to-one;

      coherence

      proof

        ( cos | [. PI , ((3 / 2) * PI ).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

      cluster ( cos | ].((3 / 2) * PI ), (2 * PI ).[) -> one-to-one;

      coherence

      proof

        ( cos | [.((3 / 2) * PI ), (2 * PI ).]) is one-to-one;

        hence thesis by Th2, XXREAL_1: 25;

      end;

    end

    theorem :: SIN_COS6:61

    ((2 * PI ) * i) <= r & r < ((2 * PI ) + ((2 * PI ) * i)) & ((2 * PI ) * i) <= s & s < ((2 * PI ) + ((2 * PI ) * i)) & ( sin r) = ( sin s) & ( cos r) = ( cos s) implies r = s

    proof

      assume that

       A1: ((2 * PI ) * i) <= r and

       A2: r < ((2 * PI ) + ((2 * PI ) * i)) & ((2 * PI ) * i) <= s and

       A3: s < ((2 * PI ) + ((2 * PI ) * i)) and

       A4: ( sin r) = ( sin s) & ( cos r) = ( cos s);

      

       A5: ( cos (r - s)) = ((( cos r) * ( cos s)) + (( sin r) * ( sin s))) by COMPLEX2: 3

      .= 1 by A4, SIN_COS: 29;

      

       A6: ( sin (r - s)) = ((( sin r) * ( cos s)) - (( cos r) * ( sin s))) by COMPLEX2: 3

      .= 0 by A4;

      

       A7: ( cos (s - r)) = ((( cos r) * ( cos s)) + (( sin r) * ( sin s))) by COMPLEX2: 3

      .= 1 by A4, SIN_COS: 29;

      

       A8: ( sin (s - r)) = ((( sin s) * ( cos r)) - (( cos s) * ( sin r))) by COMPLEX2: 3

      .= 0 by A4;

      per cases by XXREAL_0: 1;

        suppose

         A9: r > s;

        (r + ((2 * PI ) * i)) < (((2 * PI ) + ((2 * PI ) * i)) + s) by A2, XREAL_1: 8;

        then ((r + ((2 * PI ) * i)) - ((2 * PI ) * i)) < ((((2 * PI ) + ((2 * PI ) * i)) + s) - ((2 * PI ) * i)) by XREAL_1: 9;

        then r < ((2 * PI ) + s);

        then

         A10: (r - s) < (2 * PI ) by XREAL_1: 19;

        r > (s + 0 ) by A9;

        then 0 <= (r - s) by XREAL_1: 20;

        then (r - s) = 0 or (r - s) = PI by A6, A10, COMPTRIG: 17;

        hence thesis by A5, SIN_COS: 77;

      end;

        suppose

         A11: r < s;

        (s + ((2 * PI ) * i)) < (((2 * PI ) + ((2 * PI ) * i)) + r) by A1, A3, XREAL_1: 8;

        then ((s + ((2 * PI ) * i)) - ((2 * PI ) * i)) < ((((2 * PI ) + ((2 * PI ) * i)) + r) - ((2 * PI ) * i)) by XREAL_1: 9;

        then s < ((2 * PI ) + r);

        then

         A12: (s - r) < (2 * PI ) by XREAL_1: 19;

        s > (r + 0 ) by A11;

        then 0 <= (s - r) by XREAL_1: 20;

        then (s - r) = 0 or (s - r) = PI by A8, A12, COMPTRIG: 17;

        hence thesis by A7, SIN_COS: 77;

      end;

        suppose r = s;

        hence thesis;

      end;

    end;

    begin

    definition

      :: SIN_COS6:def1

      func arcsin -> PartFunc of REAL , REAL equals (( sin | [.( - ( PI / 2)), ( PI / 2).]) " );

      coherence ;

    end

    definition

      let r be object;

      :: SIN_COS6:def2

      func arcsin r -> number equals ( arcsin . r);

      coherence ;

    end

    registration

      let r be object;

      cluster ( arcsin r) -> real;

      coherence ;

    end

    

     Lm15: ( arcsin qua Function " ) = ( sin | [.( - ( PI / 2)), ( PI / 2).]) by FUNCT_1: 43;

    theorem :: SIN_COS6:62

    

     Th62: ( rng arcsin ) = [.( - ( PI / 2)), ( PI / 2).]

    proof

      ( dom ( sin | [.( - ( PI / 2)), ( PI / 2).])) = [.( - ( PI / 2)), ( PI / 2).] by RELAT_1: 62, SIN_COS: 24;

      hence thesis by FUNCT_1: 33;

    end;

    registration

      cluster arcsin -> one-to-one;

      coherence ;

    end

    theorem :: SIN_COS6:63

    

     Th63: ( dom arcsin ) = [.( - 1), 1.] by COMPTRIG: 30, FUNCT_1: 33;

    theorem :: SIN_COS6:64

    

     Th64: (( sin | [.( - ( PI / 2)), ( PI / 2).]) qua Function * arcsin ) = ( id [.( - 1), 1.]) by COMPTRIG: 30, FUNCT_1: 39;

    theorem :: SIN_COS6:65

    ( arcsin * ( sin | [.( - ( PI / 2)), ( PI / 2).])) = ( id [.( - 1), 1.]) by COMPTRIG: 30, FUNCT_1: 39;

    theorem :: SIN_COS6:66

    

     Th66: (( sin | [.( - ( PI / 2)), ( PI / 2).]) * arcsin ) = ( id [.( - ( PI / 2)), ( PI / 2).]) by Lm15, Th62, FUNCT_1: 39;

    theorem :: SIN_COS6:67

    ( arcsin qua Function * ( sin | [.( - ( PI / 2)), ( PI / 2).])) = ( id [.( - ( PI / 2)), ( PI / 2).]) by Lm15, Th62, FUNCT_1: 39;

    theorem :: SIN_COS6:68

    

     Th68: ( - 1) <= r & r <= 1 implies ( sin ( arcsin r)) = r

    proof

      assume ( - 1) <= r & r <= 1;

      then

       A1: r in [.( - 1), 1.] by XXREAL_1: 1;

      then

       A2: ( arcsin . r) in [.( - ( PI / 2)), ( PI / 2).] by Th62, Th63, FUNCT_1:def 3;

      

      thus ( sin ( arcsin r)) = ( sin . ( arcsin . r)) by SIN_COS:def 17

      .= (( sin | [.( - ( PI / 2)), ( PI / 2).]) qua Function . ( arcsin . r)) by A2, FUNCT_1: 49

      .= (( id [.( - 1), 1.]) . r) by A1, Th63, Th64, FUNCT_1: 13

      .= r by A1, FUNCT_1: 18;

    end;

    theorem :: SIN_COS6:69

    

     Th69: ( - ( PI / 2)) <= r & r <= ( PI / 2) implies ( arcsin ( sin r)) = r

    proof

      

       A1: ( dom ( sin | [.( - ( PI / 2)), ( PI / 2).])) = [.( - ( PI / 2)), ( PI / 2).] by RELAT_1: 62, SIN_COS: 24;

      assume ( - ( PI / 2)) <= r & r <= ( PI / 2);

      then

       A2: r in [.( - ( PI / 2)), ( PI / 2).] by XXREAL_1: 1;

      

      thus ( arcsin ( sin r)) = ( arcsin . ( sin . r)) by SIN_COS:def 17

      .= ( arcsin . (( sin | [.( - ( PI / 2)), ( PI / 2).]) . r)) by A2, FUNCT_1: 49

      .= (( id [.( - ( PI / 2)), ( PI / 2).]) . r) by A2, A1, Th66, FUNCT_1: 13

      .= r by A2, FUNCT_1: 18;

    end;

    theorem :: SIN_COS6:70

    ( arcsin ( - 1)) = ( - ( PI / 2)) by Th7, Th69;

    theorem :: SIN_COS6:71

    ( arcsin 0 ) = 0 by Th69, SIN_COS: 31;

    theorem :: SIN_COS6:72

    ( arcsin 1) = ( PI / 2) by Th69, SIN_COS: 77;

    theorem :: SIN_COS6:73

    ( - 1) <= r & r <= 1 & ( arcsin r) = ( - ( PI / 2)) implies r = ( - 1) by Th7, Th68;

    theorem :: SIN_COS6:74

    ( - 1) <= r & r <= 1 & ( arcsin r) = 0 implies r = 0 by Th68, SIN_COS: 31;

    theorem :: SIN_COS6:75

    ( - 1) <= r & r <= 1 & ( arcsin r) = ( PI / 2) implies r = 1 by Th68, SIN_COS: 77;

    theorem :: SIN_COS6:76

    

     Th76: ( - 1) <= r & r <= 1 implies ( - ( PI / 2)) <= ( arcsin r) & ( arcsin r) <= ( PI / 2)

    proof

      assume ( - 1) <= r & r <= 1;

      then r in [.( - 1), 1.] by XXREAL_1: 1;

      then ( arcsin . r) in ( rng arcsin ) by Th63, FUNCT_1:def 3;

      hence thesis by Th62, XXREAL_1: 1;

    end;

    theorem :: SIN_COS6:77

    

     Th77: ( - 1) < r & r < 1 implies ( - ( PI / 2)) < ( arcsin r) & ( arcsin r) < ( PI / 2)

    proof

      assume

       A1: ( - 1) < r & r < 1;

      then ( - ( PI / 2)) <= ( arcsin r) & ( arcsin r) <= ( PI / 2) by Th76;

      then ( - ( PI / 2)) < ( arcsin r) & ( arcsin r) < ( PI / 2) or ( - ( PI / 2)) = ( arcsin r) or ( arcsin r) = ( PI / 2) by XXREAL_0: 1;

      hence thesis by A1, Th7, Th68, SIN_COS: 77;

    end;

    theorem :: SIN_COS6:78

    

     Th78: ( - 1) <= r & r <= 1 implies ( arcsin r) = ( - ( arcsin ( - r)))

    proof

      assume ( - 1) <= r & r <= 1;

      then

       A1: ( - ( - 1)) >= ( - r) & ( - r) >= ( - 1) by XREAL_1: 24;

      then ( arcsin ( - r)) <= ( PI / 2) by Th76;

      then

       A2: ( - ( PI / 2)) <= ( - ( arcsin ( - r))) by XREAL_1: 24;

      ( - ( PI / 2)) <= ( arcsin ( - r)) by A1, Th76;

      then

       A3: ( - ( arcsin ( - r))) <= ( - ( - ( PI / 2))) by XREAL_1: 24;

      r = ( 0 - (1 * ( - r)))

      .= ((( sin 0 ) * ( cos ( arcsin ( - r)))) - (( cos 0 ) * ( sin ( arcsin ( - r))))) by A1, Th68, SIN_COS: 31

      .= ( sin ( 0 - ( arcsin ( - r)))) by COMPLEX2: 3;

      hence thesis by A2, A3, Th69;

    end;

    theorem :: SIN_COS6:79

    

     Th79: 0 <= s & ((r ^2 ) + (s ^2 )) = 1 implies ( cos ( arcsin r)) = s

    proof

      set x = ( arcsin r);

      assume that

       A1: 0 <= s and

       A2: ((r ^2 ) + (s ^2 )) = 1;

      

       A3: ( - 1) <= r & r <= 1 by A2, Lm5;

      then ( - ( PI / 2)) <= x & x <= ( PI / 2) by Th76;

      then

       A4: x in [.( - ( PI / 2)), ( PI / 2).] by XXREAL_1: 1;

      ((( sin . x) ^2 ) + (( cos . x) ^2 )) = 1 by SIN_COS: 28;

      

      then (( cos . x) ^2 ) = (1 - (( sin . x) ^2 ))

      .= (1 - (( sin x) ^2 )) by SIN_COS:def 17

      .= (1 - (r ^2 )) by A3, Th68;

      then

       A5: ( cos . x) = s or ( cos . x) = ( - s) by A2, SQUARE_1: 40;

      ( - ( - ( - s))) < 0 or s = 0 by A1;

      hence thesis by A5, A4, COMPTRIG: 12, SIN_COS:def 19;

    end;

    theorem :: SIN_COS6:80

    s <= 0 & ((r ^2 ) + (s ^2 )) = 1 implies ( cos ( arcsin r)) = ( - s)

    proof

      set x = ( arcsin r);

      assume that

       A1: s <= 0 and

       A2: ((r ^2 ) + (s ^2 )) = 1;

      

       A3: ( - 1) <= r & r <= 1 by A2, Lm5;

      then ( - ( PI / 2)) <= x & x <= ( PI / 2) by Th76;

      then

       A4: x in [.( - ( PI / 2)), ( PI / 2).] by XXREAL_1: 1;

      ((( sin . x) ^2 ) + (( cos . x) ^2 )) = 1 by SIN_COS: 28;

      

      then (( cos . x) ^2 ) = (1 - (( sin . x) ^2 ))

      .= (1 - (( sin x) ^2 )) by SIN_COS:def 17

      .= (1 - (r ^2 )) by A3, Th68;

      then

       A5: ( cos . x) = s or ( cos . x) = ( - s) by A2, SQUARE_1: 40;

       0 > s or s = 0 by A1;

      hence thesis by A5, A4, COMPTRIG: 12, SIN_COS:def 19;

    end;

    theorem :: SIN_COS6:81

    

     Th81: ( - 1) <= r & r <= 1 implies ( cos ( arcsin r)) = ( sqrt (1 - (r ^2 )))

    proof

      set s = ( sqrt (1 - (r ^2 )));

      assume ( - 1) <= r & r <= 1;

      then ((r ^2 ) + 0 ) <= (1 ^2 ) by SQUARE_1: 49;

      then 0 <= (1 - (r ^2 )) by XREAL_1: 19;

      then 0 <= s & ((r ^2 ) + (s ^2 )) = ((r ^2 ) + (1 - (r ^2 ))) by SQUARE_1:def 2;

      hence thesis by Th79;

    end;

    theorem :: SIN_COS6:82

    ( arcsin | [.( - 1), 1.]) is increasing

    proof

      set f = ( sin | [.( - ( PI / 2)), ( PI / 2).]);

      (f .: [.( - ( PI / 2)), ( PI / 2).]) = [.( - 1), 1.] & (((f | [.( - ( PI / 2)), ( PI / 2).]) " ) | (f .: [.( - ( PI / 2)), ( PI / 2).])) is increasing by Th45, COMPTRIG: 23, FCONT_3: 9, RELAT_1: 129;

      hence thesis by RELAT_1: 72;

    end;

    theorem :: SIN_COS6:83

     arcsin is_differentiable_on ].( - 1), 1.[ & (( - 1) < r & r < 1 implies ( diff ( arcsin ,r)) = (1 / ( sqrt (1 - (r ^2 )))))

    proof

      set g = ( arcsin | ].( - 1), 1.[);

      set h = ( sin | [.( - ( PI / 2)), ( PI / 2).]);

      set f = ( sin | ].( - ( PI / 2)), ( PI / 2).[);

      

       A1: ( dom f) = ( ].( - ( PI / 2)), ( PI / 2).[ /\ REAL ) by RELAT_1: 61, SIN_COS: 24

      .= ].( - ( PI / 2)), ( PI / 2).[ by XBOOLE_1: 28;

      set x = ( arcsin . r);

      set s = ( sqrt (1 - (r ^2 )));

      

       A2: ].( - 1), 1.[ c= ( dom arcsin ) by Th63, XXREAL_1: 25;

      

       A3: sin is_differentiable_on ].( - ( PI / 2)), ( PI / 2).[ by FDIFF_1: 26, SIN_COS: 68;

      then

       A4: f is_differentiable_on ].( - ( PI / 2)), ( PI / 2).[ by FDIFF_2: 16;

       A5:

      now

        let x0 be Real such that

         A6: x0 in ].( - ( PI / 2)), ( PI / 2).[;

        ( diff (f,x0)) = ((f `| ].( - ( PI / 2)), ( PI / 2).[) . x0) by A4, A6, FDIFF_1:def 7

        .= (( sin `| ].( - ( PI / 2)), ( PI / 2).[) . x0) by A3, FDIFF_2: 16

        .= ( diff ( sin ,x0)) by A3, A6, FDIFF_1:def 7

        .= ( cos . x0) by SIN_COS: 68;

        hence 0 < ( diff (f,x0)) by A6, COMPTRIG: 11;

      end;

      

       A7: (f " ) = ((h | ].( - ( PI / 2)), ( PI / 2).[) " ) by RELAT_1: 74, XXREAL_1: 25

      .= ((h " ) | (h .: ].( - ( PI / 2)), ( PI / 2).[)) by RFUNCT_2: 17

      .= g by Th46, RELAT_1: 129, XXREAL_1: 25;

      then

       A8: (f | ].( - ( PI / 2)), ( PI / 2).[) = f & ( dom (f " )) = ].( - 1), 1.[ by Th63, RELAT_1: 62, RELAT_1: 72, XXREAL_1: 25;

      then

       A9: g is_differentiable_on ].( - 1), 1.[ by A7, A4, A1, A5, FDIFF_2: 48;

      then for x st x in ].( - 1), 1.[ holds g is_differentiable_in x by FDIFF_1: 9;

      hence

       A10: arcsin is_differentiable_on ].( - 1), 1.[ by A2, FDIFF_1:def 6;

      assume

       A11: ( - 1) < r & r < 1;

      then

       A12: r in ].( - 1), 1.[ by XXREAL_1: 4;

      then

       A13: (g . r) = x by FUNCT_1: 49;

      x = ( arcsin r);

      then ( - ( PI / 2)) < x & x < ( PI / 2) by A11, Th77;

      then

       A14: x in ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 4;

      

      then

       A15: ( diff (f,x)) = ((f `| ].( - ( PI / 2)), ( PI / 2).[) . x) by A4, FDIFF_1:def 7

      .= (( sin `| ].( - ( PI / 2)), ( PI / 2).[) . x) by A3, FDIFF_2: 16

      .= ( diff ( sin ,x)) by A3, A14, FDIFF_1:def 7

      .= ( cos . x) by SIN_COS: 68

      .= ( cos ( arcsin r)) by SIN_COS:def 19

      .= s by A11, Th81;

      

      thus ( diff ( arcsin ,r)) = (( arcsin `| ].( - 1), 1.[) . r) by A10, A12, FDIFF_1:def 7

      .= ((g `| ].( - 1), 1.[) . r) by A10, FDIFF_2: 16

      .= ( diff (g,r)) by A9, A12, FDIFF_1:def 7

      .= (1 / s) by A7, A8, A4, A1, A5, A12, A13, A15, FDIFF_2: 48;

    end;

    theorem :: SIN_COS6:84

    ( arcsin | [.( - 1), 1.]) is continuous

    proof

      set f = ( sin | [.( - ( PI / 2)), ( PI / 2).]);

      ( dom f) = [.( - ( PI / 2)), ( PI / 2).] by RELAT_1: 62, SIN_COS: 24;

      then (f | [.( - ( PI / 2)), ( PI / 2).]) = f & (((f | [.( - ( PI / 2)), ( PI / 2).]) " ) | (f .: [.( - ( PI / 2)), ( PI / 2).])) is continuous by COMPTRIG: 23, FCONT_1: 47, RELAT_1: 73;

      hence thesis by COMPTRIG: 30, RELAT_1: 115;

    end;

    begin

    definition

      :: SIN_COS6:def3

      func arccos -> PartFunc of REAL , REAL equals (( cos | [. 0 , PI .]) " );

      coherence ;

    end

    definition

      let r be object;

      :: SIN_COS6:def4

      func arccos r -> number equals ( arccos . r);

      coherence ;

    end

    registration

      let r be object;

      cluster ( arccos r) -> real;

      coherence ;

    end

    

     Lm16: ( arccos qua Function " ) = ( cos | [. 0 , PI .]) by FUNCT_1: 43;

    theorem :: SIN_COS6:85

    

     Th85: ( rng arccos ) = [. 0 , PI .]

    proof

      ( dom ( cos | [. 0 , PI .])) = [. 0 , PI .] by RELAT_1: 62, SIN_COS: 24;

      hence thesis by FUNCT_1: 33;

    end;

    registration

      cluster arccos -> one-to-one;

      coherence ;

    end

    theorem :: SIN_COS6:86

    

     Th86: ( dom arccos ) = [.( - 1), 1.] by COMPTRIG: 32, FUNCT_1: 33;

    theorem :: SIN_COS6:87

    

     Th87: (( cos | [. 0 , PI .]) qua Function * arccos ) = ( id [.( - 1), 1.]) by COMPTRIG: 32, FUNCT_1: 39;

    theorem :: SIN_COS6:88

    ( arccos * ( cos | [. 0 , PI .])) = ( id [.( - 1), 1.]) by COMPTRIG: 32, FUNCT_1: 39;

    theorem :: SIN_COS6:89

    

     Th89: (( cos | [. 0 , PI .]) * arccos ) = ( id [. 0 , PI .]) by Lm16, Th85, FUNCT_1: 39;

    theorem :: SIN_COS6:90

    ( arccos qua Function * ( cos | [. 0 , PI .])) = ( id [. 0 , PI .]) by Lm16, Th85, FUNCT_1: 39;

    theorem :: SIN_COS6:91

    

     Th91: ( - 1) <= r & r <= 1 implies ( cos ( arccos r)) = r

    proof

      assume ( - 1) <= r & r <= 1;

      then

       A1: r in [.( - 1), 1.] by XXREAL_1: 1;

      then

       A2: ( arccos . r) in [. 0 , PI .] by Th85, Th86, FUNCT_1:def 3;

      

      thus ( cos ( arccos r)) = ( cos . ( arccos . r)) by SIN_COS:def 19

      .= (( cos | [. 0 , PI .]) qua Function . ( arccos . r)) by A2, FUNCT_1: 49

      .= (( id [.( - 1), 1.]) . r) by A1, Th86, Th87, FUNCT_1: 13

      .= r by A1, FUNCT_1: 18;

    end;

    theorem :: SIN_COS6:92

    

     Th92: 0 <= r & r <= PI implies ( arccos ( cos r)) = r

    proof

      

       A1: ( dom ( cos | [. 0 , PI .])) = [. 0 , PI .] by RELAT_1: 62, SIN_COS: 24;

      assume 0 <= r & r <= PI ;

      then

       A2: r in [. 0 , PI .] by XXREAL_1: 1;

      

      thus ( arccos ( cos r)) = ( arccos . ( cos . r)) by SIN_COS:def 19

      .= ( arccos . (( cos | [. 0 , PI .]) . r)) by A2, FUNCT_1: 49

      .= (( id [. 0 , PI .]) . r) by A2, A1, Th89, FUNCT_1: 13

      .= r by A2, FUNCT_1: 18;

    end;

    theorem :: SIN_COS6:93

    ( arccos ( - 1)) = PI by Th92, SIN_COS: 77;

    theorem :: SIN_COS6:94

    ( arccos 0 ) = ( PI / 2) by Lm6, Th92, SIN_COS: 77;

    theorem :: SIN_COS6:95

    ( arccos 1) = 0 by Th92, SIN_COS: 31;

    theorem :: SIN_COS6:96

    ( - 1) <= r & r <= 1 & ( arccos r) = 0 implies r = 1 by Th91, SIN_COS: 31;

    theorem :: SIN_COS6:97

    ( - 1) <= r & r <= 1 & ( arccos r) = ( PI / 2) implies r = 0 by Th91, SIN_COS: 77;

    theorem :: SIN_COS6:98

    ( - 1) <= r & r <= 1 & ( arccos r) = PI implies r = ( - 1) by Th91, SIN_COS: 77;

    theorem :: SIN_COS6:99

    

     Th99: ( - 1) <= r & r <= 1 implies 0 <= ( arccos r) & ( arccos r) <= PI

    proof

      assume ( - 1) <= r & r <= 1;

      then r in [.( - 1), 1.] by XXREAL_1: 1;

      then ( arccos . r) in ( rng arccos ) by Th86, FUNCT_1:def 3;

      hence thesis by Th85, XXREAL_1: 1;

    end;

    theorem :: SIN_COS6:100

    

     Th100: ( - 1) < r & r < 1 implies 0 < ( arccos r) & ( arccos r) < PI

    proof

      assume

       A1: ( - 1) < r & r < 1;

      then ( arccos r) <= PI by Th99;

      then 0 < ( arccos r) & ( arccos r) < PI or 0 = ( arccos r) or ( arccos r) = PI by A1, Th99, XXREAL_0: 1;

      hence thesis by A1, Th91, SIN_COS: 31, SIN_COS: 77;

    end;

    theorem :: SIN_COS6:101

    

     Th101: ( - 1) <= r & r <= 1 implies ( arccos r) = ( PI - ( arccos ( - r)))

    proof

      assume ( - 1) <= r & r <= 1;

      then

       A1: ( - ( - 1)) >= ( - r) & ( - r) >= ( - 1) by XREAL_1: 24;

      then ( 0 + ( arccos ( - r))) <= PI by Th99;

      then

       A2: 0 <= ( PI - ( arccos ( - r))) by XREAL_1: 19;

       0 <= ( arccos ( - r)) by A1, Th99;

      then ( PI + 0 ) <= ( PI + ( arccos ( - r))) by XREAL_1: 6;

      then

       A3: ( PI - ( arccos ( - r))) <= PI by XREAL_1: 20;

      r = (( - 1) * ( - r))

      .= ((( cos PI ) * ( cos ( arccos ( - r)))) + (( sin PI ) * ( sin ( arccos ( - r))))) by A1, Th91, SIN_COS: 77

      .= ( cos ( PI - ( arccos ( - r)))) by COMPLEX2: 3;

      hence thesis by A2, A3, Th92;

    end;

    theorem :: SIN_COS6:102

    

     Th102: 0 <= s & ((r ^2 ) + (s ^2 )) = 1 implies ( sin ( arccos r)) = s

    proof

      set x = ( arccos r);

      assume that

       A1: 0 <= s and

       A2: ((r ^2 ) + (s ^2 )) = 1;

      

       A3: ( - 1) <= r & r <= 1 by A2, Lm5;

      then 0 <= x & x <= PI by Th99;

      then

       A4: x in [. 0 , PI .] by XXREAL_1: 1;

      ((( sin . x) ^2 ) + (( cos . x) ^2 )) = 1 by SIN_COS: 28;

      

      then (( sin . x) ^2 ) = (1 - (( cos . x) ^2 ))

      .= (1 - (( cos x) ^2 )) by SIN_COS:def 19

      .= (1 - (r ^2 )) by A3, Th91;

      then

       A5: ( sin . x) = s or ( sin . x) = ( - s) by A2, SQUARE_1: 40;

      ( - ( - ( - s))) < 0 or s = 0 by A1;

      hence thesis by A5, A4, COMPTRIG: 8, SIN_COS:def 17;

    end;

    theorem :: SIN_COS6:103

    s <= 0 & ((r ^2 ) + (s ^2 )) = 1 implies ( sin ( arccos r)) = ( - s)

    proof

      set x = ( arccos r);

      assume that

       A1: s <= 0 and

       A2: ((r ^2 ) + (s ^2 )) = 1;

      

       A3: ( - 1) <= r & r <= 1 by A2, Lm5;

      then 0 <= x & x <= PI by Th99;

      then

       A4: x in [. 0 , PI .] by XXREAL_1: 1;

      ((( sin . x) ^2 ) + (( cos . x) ^2 )) = 1 by SIN_COS: 28;

      

      then (( sin . x) ^2 ) = (1 - (( cos . x) ^2 ))

      .= (1 - (( cos x) ^2 )) by SIN_COS:def 19

      .= (1 - (r ^2 )) by A3, Th91;

      then

       A5: ( sin . x) = s or ( sin . x) = ( - s) by A2, SQUARE_1: 40;

       0 > s or s = 0 by A1;

      hence thesis by A5, A4, COMPTRIG: 8, SIN_COS:def 17;

    end;

    theorem :: SIN_COS6:104

    

     Th104: ( - 1) <= r & r <= 1 implies ( sin ( arccos r)) = ( sqrt (1 - (r ^2 )))

    proof

      set s = ( sqrt (1 - (r ^2 )));

      assume ( - 1) <= r & r <= 1;

      then ((r ^2 ) + 0 ) <= (1 ^2 ) by SQUARE_1: 49;

      then 0 <= (1 - (r ^2 )) by XREAL_1: 19;

      then 0 <= s & ((r ^2 ) + (s ^2 )) = ((r ^2 ) + (1 - (r ^2 ))) by SQUARE_1:def 2;

      hence thesis by Th102;

    end;

    theorem :: SIN_COS6:105

    ( arccos | [.( - 1), 1.]) is decreasing

    proof

      set f = ( cos | [. 0 , PI .]);

      (f .: [. 0 , PI .]) = [.( - 1), 1.] & (((f | [. 0 , PI .]) " ) | (f .: [. 0 , PI .])) is decreasing by Th49, COMPTRIG: 25, FCONT_3: 10, RELAT_1: 129;

      hence thesis by RELAT_1: 72;

    end;

    theorem :: SIN_COS6:106

     arccos is_differentiable_on ].( - 1), 1.[ & (( - 1) < r & r < 1 implies ( diff ( arccos ,r)) = ( - (1 / ( sqrt (1 - (r ^2 ))))))

    proof

      set g = ( arccos | ].( - 1), 1.[);

      set h = ( cos | [. 0 , PI .]);

      set f = ( cos | ]. 0 , PI .[);

      

       A1: ( dom f) = ( ]. 0 , PI .[ /\ REAL ) by RELAT_1: 61, SIN_COS: 24

      .= ]. 0 , PI .[ by XBOOLE_1: 28;

      set x = ( arccos . r);

      set s = ( sqrt (1 - (r ^2 )));

      

       A2: ].( - 1), 1.[ c= ( dom arccos ) by Th86, XXREAL_1: 25;

      

       A3: cos is_differentiable_on ]. 0 , PI .[ by FDIFF_1: 26, SIN_COS: 67;

      then

       A4: f is_differentiable_on ]. 0 , PI .[ by FDIFF_2: 16;

       A5:

      now

        let x0 be Real such that

         A6: x0 in ]. 0 , PI .[;

        

         A7: ( - ( - ( sin . x0))) > 0 by A6, COMPTRIG: 7;

        ( diff (f,x0)) = ((f `| ]. 0 , PI .[) . x0) by A4, A6, FDIFF_1:def 7

        .= (( cos `| ]. 0 , PI .[) . x0) by A3, FDIFF_2: 16

        .= ( diff ( cos ,x0)) by A3, A6, FDIFF_1:def 7

        .= ( - ( sin . x0)) by SIN_COS: 67;

        hence 0 > ( diff (f,x0)) by A7;

      end;

      

       A8: (f " ) = ((h | ]. 0 , PI .[) " ) by RELAT_1: 74, XXREAL_1: 25

      .= ((h " ) | (h .: ]. 0 , PI .[)) by RFUNCT_2: 17

      .= g by Th50, RELAT_1: 129, XXREAL_1: 25;

      then

       A9: (f | ]. 0 , PI .[) = f & ( dom (f " )) = ].( - 1), 1.[ by Th86, RELAT_1: 62, RELAT_1: 72, XXREAL_1: 25;

      then

       A10: g is_differentiable_on ].( - 1), 1.[ by A8, A4, A1, A5, FDIFF_2: 48;

      then for x st x in ].( - 1), 1.[ holds g is_differentiable_in x by FDIFF_1: 9;

      hence

       A11: arccos is_differentiable_on ].( - 1), 1.[ by A2, FDIFF_1:def 6;

      assume

       A12: ( - 1) < r & r < 1;

      then

       A13: r in ].( - 1), 1.[ by XXREAL_1: 4;

      then

       A14: (g . r) = x by FUNCT_1: 49;

      x = ( arccos r);

      then 0 < x & x < PI by A12, Th100;

      then

       A15: x in ]. 0 , PI .[ by XXREAL_1: 4;

      

      then

       A16: ( diff (f,x)) = ((f `| ]. 0 , PI .[) . x) by A4, FDIFF_1:def 7

      .= (( cos `| ]. 0 , PI .[) . x) by A3, FDIFF_2: 16

      .= ( diff ( cos ,x)) by A3, A15, FDIFF_1:def 7

      .= ( - ( sin . x)) by SIN_COS: 67

      .= ( - ( sin ( arccos r))) by SIN_COS:def 17

      .= ( - s) by A12, Th104;

      

      thus ( diff ( arccos ,r)) = (( arccos `| ].( - 1), 1.[) . r) by A11, A13, FDIFF_1:def 7

      .= ((g `| ].( - 1), 1.[) . r) by A11, FDIFF_2: 16

      .= ( diff (g,r)) by A10, A13, FDIFF_1:def 7

      .= (1 / ( - s)) by A8, A9, A4, A1, A5, A13, A14, A16, FDIFF_2: 48

      .= (( - 1) / s) by XCMPLX_1: 192

      .= ( - (1 / s)) by XCMPLX_1: 187;

    end;

    theorem :: SIN_COS6:107

    ( arccos | [.( - 1), 1.]) is continuous

    proof

      set f = ( cos | [. 0 , PI .]);

      ( dom f) = [. 0 , PI .] by RELAT_1: 62, SIN_COS: 24;

      then (f | [. 0 , PI .]) = f & (((f | [. 0 , PI .]) " ) | (f .: [. 0 , PI .])) is continuous by COMPTRIG: 25, FCONT_1: 47, RELAT_1: 73;

      hence thesis by COMPTRIG: 32, RELAT_1: 115;

    end;

    theorem :: SIN_COS6:108

    

     Th108: ( - 1) <= r & r <= 1 implies (( arcsin r) + ( arccos r)) = ( PI / 2)

    proof

      assume

       A1: ( - 1) <= r & r <= 1;

      then (( - ( PI / 2)) + ( PI / 2)) <= ( arccos r) by Th99;

      then ( - ( PI / 2)) <= (( arccos r) - ( PI / 2)) by XREAL_1: 19;

      then

       A2: ( - ( - ( PI / 2))) >= ( - (( arccos r) - ( PI / 2))) by XREAL_1: 24;

      ( arccos r) <= (( PI / 2) + ( PI / 2)) by A1, Th99;

      then (( arccos r) - ( PI / 2)) <= ( PI / 2) by XREAL_1: 20;

      then

       A3: ( - (( arccos r) - ( PI / 2))) >= ( - ( PI / 2)) by XREAL_1: 24;

      r = ((( sin ( PI / 2)) * ( cos ( arccos r))) - (( cos ( PI / 2)) * ( sin ( arccos r)))) by A1, Th91, SIN_COS: 77

      .= ( sin (( PI / 2) - ( arccos r))) by COMPLEX2: 3;

      then ( arcsin r) = (( PI / 2) - ( arccos r)) by A2, A3, Th69;

      hence thesis;

    end;

    theorem :: SIN_COS6:109

    ( - 1) <= r & r <= 1 implies (( arccos ( - r)) - ( arcsin r)) = ( PI / 2)

    proof

      assume

       A1: ( - 1) <= r & r <= 1;

      then

       A2: (( arcsin r) + ( arccos r)) = (( PI / 2) + 0 ) by Th108;

      ( - ( - 1)) >= ( - r) & ( - r) >= ( - 1) by A1, XREAL_1: 24;

      

      then ( arccos ( - r)) = ( PI - ( arccos ( - ( - r)))) by Th101

      .= (( arcsin r) + ( PI / 2)) by A2;

      hence thesis;

    end;

    theorem :: SIN_COS6:110

    ( - 1) <= r & r <= 1 implies (( arccos r) - ( arcsin ( - r))) = ( PI / 2)

    proof

      assume

       A1: ( - 1) <= r & r <= 1;

      then

       A2: (( arcsin r) + ( arccos r)) = (( PI / 2) + 0 ) by Th108;

      ( - ( - 1)) >= ( - r) & ( - r) >= ( - 1) by A1, XREAL_1: 24;

      

      then ( arcsin ( - r)) = ( - ( arcsin ( - ( - r)))) by Th78

      .= (( arccos r) - ( PI / 2)) by A2;

      hence thesis;

    end;