sin_cos9.miz



    begin

    reserve x,x0,r,s,h for Real,

n for Element of NAT ,

rr,y for set,

Z for open Subset of REAL ,

f,f1,f2 for PartFunc of REAL , REAL ;

    theorem :: SIN_COS9:1

    

     Th1: ].( - ( PI / 2)), ( PI / 2).[ c= ( dom tan )

    proof

      ( ].( - ( PI / 2)), ( PI / 2).[ /\ ( cos " { 0 })) = {}

      proof

        assume ( ].( - ( PI / 2)), ( PI / 2).[ /\ ( cos " { 0 })) <> {} ;

        then

        consider rr be object such that

         A1: rr in ( ].( - ( PI / 2)), ( PI / 2).[ /\ ( cos " { 0 })) by XBOOLE_0: 7;

        rr in ( cos " { 0 }) by A1, XBOOLE_0:def 4;

        then

         A2: ( cos . rr) in { 0 } by FUNCT_1:def 7;

        rr in ].( - ( PI / 2)), ( PI / 2).[ by A1, XBOOLE_0:def 4;

        then ( cos . rr) <> 0 by COMPTRIG: 11;

        hence contradiction by A2, TARSKI:def 1;

      end;

      then

       A3: ].( - ( PI / 2)), ( PI / 2).[ misses ( cos " { 0 }) by XBOOLE_0:def 7;

      ( ].( - ( PI / 2)), ( PI / 2).[ \ ( cos " { 0 })) c= (( dom cos ) \ ( cos " { 0 })) by SIN_COS: 24, XBOOLE_1: 33;

      then ].( - ( PI / 2)), ( PI / 2).[ c= (( dom cos ) \ ( cos " { 0 })) by A3, XBOOLE_1: 83;

      then ].( - ( PI / 2)), ( PI / 2).[ c= (( dom sin ) /\ (( dom cos ) \ ( cos " { 0 }))) by SIN_COS: 24, XBOOLE_1: 19;

      hence thesis by RFUNCT_1:def 1;

    end;

    theorem :: SIN_COS9:2

    

     Th2: ]. 0 , PI .[ c= ( dom cot )

    proof

      ( ]. 0 , PI .[ /\ ( sin " { 0 })) = {}

      proof

        assume ( ]. 0 , PI .[ /\ ( sin " { 0 })) <> {} ;

        then

        consider rr be object such that

         A1: rr in ( ]. 0 , PI .[ /\ ( sin " { 0 })) by XBOOLE_0: 7;

        rr in ( sin " { 0 }) by A1, XBOOLE_0:def 4;

        then

         A2: ( sin . rr) in { 0 } by FUNCT_1:def 7;

        rr in ]. 0 , PI .[ by A1, XBOOLE_0:def 4;

        then ( sin . rr) <> 0 by COMPTRIG: 7;

        hence contradiction by A2, TARSKI:def 1;

      end;

      then

       A3: ]. 0 , PI .[ misses ( sin " { 0 }) by XBOOLE_0:def 7;

      ( ]. 0 , PI .[ \ ( sin " { 0 })) c= (( dom sin ) \ ( sin " { 0 })) by SIN_COS: 24, XBOOLE_1: 33;

      then ]. 0 , PI .[ c= (( dom sin ) \ ( sin " { 0 })) by A3, XBOOLE_1: 83;

      then ]. 0 , PI .[ c= (( dom cos ) /\ (( dom sin ) \ ( sin " { 0 }))) by SIN_COS: 24, XBOOLE_1: 19;

      hence thesis by RFUNCT_1:def 1;

    end;

    

     Lm1: tan is_differentiable_on ].( - ( PI / 2)), ( PI / 2).[

    proof

      for x st x in ].( - ( PI / 2)), ( PI / 2).[ holds tan is_differentiable_in x

      proof

        let x;

        assume x in ].( - ( PI / 2)), ( PI / 2).[;

        then ( cos . x) <> 0 by COMPTRIG: 11;

        hence thesis by FDIFF_7: 46;

      end;

      hence thesis by Th1, FDIFF_1: 9;

    end;

    

     Lm2: cot is_differentiable_on ]. 0 , PI .[

    proof

      for x st x in ]. 0 , PI .[ holds cot is_differentiable_in x

      proof

        let x;

        assume x in ]. 0 , PI .[;

        then ( sin . x) <> 0 by COMPTRIG: 7;

        hence thesis by FDIFF_7: 47;

      end;

      hence thesis by Th2, FDIFF_1: 9;

    end;

    

     Lm3: for x st x in ].( - ( PI / 2)), ( PI / 2).[ holds ( diff ( tan ,x)) = (1 / (( cos . x) ^2 ))

    proof

      let x;

      assume x in ].( - ( PI / 2)), ( PI / 2).[;

      then ( cos . x) <> 0 by COMPTRIG: 11;

      hence thesis by FDIFF_7: 46;

    end;

    

     Lm4: for x st x in ]. 0 , PI .[ holds ( diff ( cot ,x)) = ( - (1 / (( sin . x) ^2 )))

    proof

      let x;

      assume x in ]. 0 , PI .[;

      then ( sin . x) <> 0 by COMPTRIG: 7;

      hence thesis by FDIFF_7: 47;

    end;

    theorem :: SIN_COS9:3

     tan is_differentiable_on ].( - ( PI / 2)), ( PI / 2).[ & for x st x in ].( - ( PI / 2)), ( PI / 2).[ holds ( diff ( tan ,x)) = (1 / (( cos . x) ^2 )) by Lm1, Lm3;

    theorem :: SIN_COS9:4

     cot is_differentiable_on ]. 0 , PI .[ & for x st x in ]. 0 , PI .[ holds ( diff ( cot ,x)) = ( - (1 / (( sin . x) ^2 ))) by Lm2, Lm4;

    theorem :: SIN_COS9:5

    ( tan | ].( - ( PI / 2)), ( PI / 2).[) is continuous by Lm1, FDIFF_1: 25;

    theorem :: SIN_COS9:6

    ( cot | ]. 0 , PI .[) is continuous by Lm2, FDIFF_1: 25;

    theorem :: SIN_COS9:7

    

     Th7: ( tan | ].( - ( PI / 2)), ( PI / 2).[) is increasing

    proof

      

       A1: for x st x in ].( - ( PI / 2)), ( PI / 2).[ holds ( diff ( tan ,x)) > 0

      proof

        let x;

        assume

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

        then 0 < ( cos . x) by COMPTRIG: 11;

        then (( cos . x) ^2 ) > 0 ;

        then (1 / (( cos . x) ^2 )) > ( 0 / (( cos . x) ^2 ));

        hence thesis by A2, Lm3;

      end;

       ].( - ( PI / 2)), ( PI / 2).[ c= ( dom tan ) by Lm1, FDIFF_1:def 6;

      hence thesis by A1, Lm1, ROLLE: 9;

    end;

    theorem :: SIN_COS9:8

    

     Th8: ( cot | ]. 0 , PI .[) is decreasing

    proof

      

       A1: for x st x in ]. 0 , PI .[ holds ( diff ( cot ,x)) < 0

      proof

        let x;

        assume

         A2: x in ]. 0 , PI .[;

        then 0 < ( sin . x) by COMPTRIG: 7;

        then (( sin . x) ^2 ) > 0 ;

        then (1 / (( sin . x) ^2 )) > ( 0 / (( sin . x) ^2 ));

        then ( - (1 / (( sin . x) ^2 ))) < ( - 0 );

        hence thesis by A2, Lm4;

      end;

       ]. 0 , PI .[ c= ( dom cot ) by Lm2, FDIFF_1:def 6;

      hence thesis by A1, Lm2, ROLLE: 10;

    end;

    theorem :: SIN_COS9:9

    ( tan | ].( - ( PI / 2)), ( PI / 2).[) is one-to-one by Th7, FCONT_3: 8;

    theorem :: SIN_COS9:10

    ( cot | ]. 0 , PI .[) is one-to-one by Th8, FCONT_3: 8;

    registration

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

      coherence by Th7, FCONT_3: 8;

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

      coherence by Th8, FCONT_3: 8;

    end

    definition

      :: SIN_COS9:def1

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

      coherence ;

      :: SIN_COS9:def2

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

      coherence ;

    end

    definition

      let r be Real;

      :: SIN_COS9:def3

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

      coherence ;

      :: SIN_COS9:def4

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

      coherence ;

    end

    registration

      let r be Real;

      cluster ( arctan r) -> real;

      coherence ;

      cluster ( arccot r) -> real;

      coherence ;

    end

    

     Lm5: ( arctan qua Function " ) = ( tan | ].( - ( PI / 2)), ( PI / 2).[) by FUNCT_1: 43;

    

     Lm6: ( arccot qua Function " ) = ( cot | ]. 0 , PI .[) by FUNCT_1: 43;

    theorem :: SIN_COS9:11

    

     Th11: ( rng arctan ) = ].( - ( PI / 2)), ( PI / 2).[

    proof

      ( dom ( tan | ].( - ( PI / 2)), ( PI / 2).[)) = ].( - ( PI / 2)), ( PI / 2).[ by Th1, RELAT_1: 62;

      hence thesis by FUNCT_1: 33;

    end;

    theorem :: SIN_COS9:12

    

     Th12: ( rng arccot ) = ]. 0 , PI .[

    proof

      ( dom ( cot | ]. 0 , PI .[)) = ]. 0 , PI .[ by Th2, RELAT_1: 62;

      hence thesis by FUNCT_1: 33;

    end;

    registration

      cluster arctan -> one-to-one;

      coherence ;

      cluster arccot -> one-to-one;

      coherence ;

    end

    

     Lm7: ( - ( PI / 4)) in ].( - ( PI / 2)), ( PI / 2).[

    proof

      ( PI / ( - 4)) > ( PI / ( - 2)) by XREAL_1: 99;

      then ( - ( PI / 4)) in { s where s be Real : ( - ( PI / 2)) < s & s < ( PI / 2) };

      hence thesis by RCOMP_1:def 2;

    end;

    

     Lm8: ( PI / 4) in ].( - ( PI / 2)), ( PI / 2).[

    proof

      ( PI / 4) < ( PI / 2) by XREAL_1: 76;

      then ( PI / 4) in { s where s be Real : ( - ( PI / 2)) < s & s < ( PI / 2) };

      hence thesis by RCOMP_1:def 2;

    end;

    

     Lm9: ( PI / 4) in ]. 0 , PI .[

    proof

      

       A1: ( PI / 4) < ( PI / 1) by XREAL_1: 76;

      thus thesis by A1, XXREAL_1: 4;

    end;

    

     Lm10: ((3 / 4) * PI ) in ]. 0 , PI .[

    proof

      

       A1: ((3 / 4) * PI ) < PI by XREAL_1: 157;

      thus thesis by A1, XXREAL_1: 4;

    end;

    

     Lm11: ( dom ( tan | [.( - ( PI / 4)), ( PI / 4).])) = [.( - ( PI / 4)), ( PI / 4).]

    proof

       [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      hence thesis by Th1, RELAT_1: 62, XBOOLE_1: 1;

    end;

    

     Lm12: ( dom ( cot | [.( PI / 4), ((3 / 4) * PI ).])) = [.( PI / 4), ((3 / 4) * PI ).]

    proof

       [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

      hence thesis by Th2, RELAT_1: 62, XBOOLE_1: 1;

    end;

    theorem :: SIN_COS9:13

    

     Th13: for x be Real st x in ].( - ( PI / 2)), ( PI / 2).[ holds ( tan . x) = ( tan x)

    proof

      let x be Real;

      assume x in ].( - ( PI / 2)), ( PI / 2).[;

      

      then ( tan . x) = (( sin x) / ( cos x)) by Th1, RFUNCT_1:def 1

      .= ( tan x) by SIN_COS4:def 1;

      hence thesis;

    end;

    theorem :: SIN_COS9:14

    

     Th14: for x be Real st x in ]. 0 , PI .[ holds ( cot . x) = ( cot x)

    proof

      let x be Real;

      assume x in ]. 0 , PI .[;

      

      then ( cot . x) = (( cos x) / ( sin x)) by Th2, RFUNCT_1:def 1

      .= ( cot x) by SIN_COS4:def 2;

      hence thesis;

    end;

    theorem :: SIN_COS9:15

    for x be Real st ( cos . x) <> 0 holds ( tan . x) = ( tan x)

    proof

      let x be Real;

      assume

       A1: ( cos . x) <> 0 ;

      

       A2: x in REAL by XREAL_0:def 1;

       not x in ( cos " { 0 })

      proof

        assume x in ( cos " { 0 });

        then ( cos . x) in { 0 } by FUNCT_1:def 7;

        hence contradiction by A1, TARSKI:def 1;

      end;

      then x in (( dom cos ) \ ( cos " { 0 })) by SIN_COS: 24, XBOOLE_0:def 5, A2;

      then x in (( dom sin ) /\ (( dom cos ) \ ( cos " { 0 }))) by SIN_COS: 24, XBOOLE_0:def 4, A2;

      then x in ( dom ( sin / cos )) by RFUNCT_1:def 1;

      

      then ( tan . x) = (( sin x) / ( cos x)) by RFUNCT_1:def 1

      .= ( tan x) by SIN_COS4:def 1;

      hence thesis;

    end;

    theorem :: SIN_COS9:16

    for x be Real st ( sin . x) <> 0 holds ( cot . x) = ( cot x)

    proof

      let x be Real;

      assume

       A1: ( sin . x) <> 0 ;

      

       A2: x in REAL by XREAL_0:def 1;

       not x in ( sin " { 0 })

      proof

        assume x in ( sin " { 0 });

        then ( sin . x) in { 0 } by FUNCT_1:def 7;

        hence contradiction by A1, TARSKI:def 1;

      end;

      then x in (( dom sin ) \ ( sin " { 0 })) by SIN_COS: 24, XBOOLE_0:def 5, A2;

      then x in (( dom cos ) /\ (( dom sin ) \ ( sin " { 0 }))) by SIN_COS: 24, XBOOLE_0:def 4, A2;

      then x in ( dom ( cos / sin )) by RFUNCT_1:def 1;

      

      then ( cot . x) = (( cos x) / ( sin x)) by RFUNCT_1:def 1

      .= ( cot x) by SIN_COS4:def 2;

      hence thesis;

    end;

    theorem :: SIN_COS9:17

    

     Th17: ( tan . ( - ( PI / 4))) = ( - 1) & ( tan ( - ( PI / 4))) = ( - 1)

    proof

      ( cos . ( PI / 4)) <> 0 by Lm8, COMPTRIG: 11;

      then

       A1: (( sin . ( PI / 4)) / ( cos . ( PI / 4))) = 1 by SIN_COS: 73, XCMPLX_1: 60;

      ( tan . ( - ( PI / 4))) = (( sin . ( - ( PI / 4))) / ( cos . ( - ( PI / 4)))) by Lm7, Th1, RFUNCT_1:def 1

      .= (( - ( sin . ( PI / 4))) / ( cos . ( - ( PI / 4)))) by SIN_COS: 30

      .= (( - ( sin . ( PI / 4))) / ( cos . ( PI / 4))) by SIN_COS: 30

      .= ( - 1) by A1;

      hence thesis by Lm7, Th13;

    end;

    theorem :: SIN_COS9:18

    

     Th18: ( cot . ( PI / 4)) = 1 & ( cot ( PI / 4)) = 1 & ( cot . ((3 / 4) * PI )) = ( - 1) & ( cot ((3 / 4) * PI )) = ( - 1)

    proof

      

       A1: ( sin . ( PI / 4)) <> 0 by Lm9, COMPTRIG: 7;

      

       A2: ( cot . ((3 / 4) * PI )) = (( cos . ((3 / 4) * PI )) * (( sin . ((3 / 4) * PI )) " )) by Lm10, Th2, RFUNCT_1:def 1

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

      .= (( - ( sin . ( PI / 4))) / ( cos . ( PI / 4))) by SIN_COS: 78

      .= ( - (( sin . ( PI / 4)) / ( cos . ( PI / 4))))

      .= ( - 1) by A1, SIN_COS: 73, XCMPLX_1: 60;

      ( cot . ( PI / 4)) = (( cos . ( PI / 4)) / ( sin . ( PI / 4))) by Lm9, Th2, RFUNCT_1:def 1

      .= 1 by A1, SIN_COS: 73, XCMPLX_1: 60;

      hence thesis by A2, Lm9, Lm10, Th14;

    end;

    theorem :: SIN_COS9:19

    

     Th19: for x be set st x in [.( - ( PI / 4)), ( PI / 4).] holds ( tan . x) in [.( - 1), 1.]

    proof

      let x be set;

      assume x in [.( - ( PI / 4)), ( PI / 4).];

      then x in ( ].( - ( PI / 4)), ( PI / 4).[ \/ {( - ( PI / 4)), ( PI / 4)}) by XXREAL_1: 128;

      then

       A1: x in ].( - ( PI / 4)), ( PI / 4).[ or x in {( - ( PI / 4)), ( PI / 4)} by XBOOLE_0:def 3;

      per cases by A1, TARSKI:def 2;

        suppose

         A2: x in ].( - ( PI / 4)), ( PI / 4).[;

        then x in { s where s be Real : ( - ( PI / 4)) < s & s < ( PI / 4) } by RCOMP_1:def 2;

        then

         A3: ex s be Real st s = x & ( - ( PI / 4)) < s & s < ( PI / 4);

        

         A4: ].( - ( PI / 4)), ( PI / 4).[ c= [.( - ( PI / 4)), ( PI / 4).] by XXREAL_1: 25;

        ( - ( PI / 4)) in { s where s be Real : ( - ( PI / 4)) <= s & s <= ( PI / 4) };

        then

         A5: ( - ( PI / 4)) in [.( - ( PI / 4)), ( PI / 4).] by RCOMP_1:def 1;

        

         A6: [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

        then

         A7: ( tan | [.( - ( PI / 4)), ( PI / 4).]) is increasing by Th7, RFUNCT_2: 28;

        

         A8: ( [.( - ( PI / 4)), ( PI / 4).] /\ ( dom tan )) = [.( - ( PI / 4)), ( PI / 4).] by A6, Th1, XBOOLE_1: 1, XBOOLE_1: 28;

        ( PI / 4) in { s where s be Real : ( - ( PI / 4)) <= s & s <= ( PI / 4) };

        then ( PI / 4) in ( [.( - ( PI / 4)), ( PI / 4).] /\ ( dom tan )) by A8, RCOMP_1:def 1;

        then ( tan . x) < ( tan . ( PI / 4)) by A2, A7, A8, A4, A3, RFUNCT_2: 20;

        then

         A9: ( tan . x) < 1 by SIN_COS:def 28;

        x in { s where s be Real : ( - ( PI / 4)) < s & s < ( PI / 4) } by A2, RCOMP_1:def 2;

        then ex s be Real st s = x & ( - ( PI / 4)) < s & s < ( PI / 4);

        then ( - 1) < ( tan . x) by A2, A7, A5, A8, A4, Th17, RFUNCT_2: 20;

        then ( tan . x) in { s where s be Real : ( - 1) < s & s < 1 } by A9;

        then

         A10: ( tan . x) in ].( - 1), 1.[ by RCOMP_1:def 2;

         ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

        hence thesis by A10;

      end;

        suppose x = ( - ( PI / 4));

        then ( tan . x) in { s where s be Real : ( - 1) <= s & s <= 1 } by Th17;

        hence thesis by RCOMP_1:def 1;

      end;

        suppose x = ( PI / 4);

        then ( tan . x) = 1 by SIN_COS:def 28;

        then ( tan . x) in { s where s be Real : ( - 1) <= s & s <= 1 };

        hence thesis by RCOMP_1:def 1;

      end;

    end;

    theorem :: SIN_COS9:20

    

     Th20: for x be set st x in [.( PI / 4), ((3 / 4) * PI ).] holds ( cot . x) in [.( - 1), 1.]

    proof

      let x be set;

      

       A1: (( PI / 4) * 3) > ( PI / 4) by XREAL_1: 155;

      assume x in [.( PI / 4), ((3 / 4) * PI ).];

      then x in ( ].( PI / 4), ((3 / 4) * PI ).[ \/ {( PI / 4), ((3 / 4) * PI )}) by A1, XXREAL_1: 128;

      then

       A2: x in ].( PI / 4), ((3 / 4) * PI ).[ or x in {( PI / 4), ((3 / 4) * PI )} by XBOOLE_0:def 3;

      per cases by A2, TARSKI:def 2;

        suppose

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

        then x in { s where s be Real : ( PI / 4) < s & s < ((3 / 4) * PI ) } by RCOMP_1:def 2;

        then

         A4: ex s be Real st s = x & ( PI / 4) < s & s < ((3 / 4) * PI );

        

         A5: [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

        then

         A6: ( cot | [.( PI / 4), ((3 / 4) * PI ).]) is decreasing by Th8, RFUNCT_2: 29;

        x in { s where s be Real : ( PI / 4) < s & s < ((3 / 4) * PI ) } by A3, RCOMP_1:def 2;

        then

         A7: ex s be Real st s = x & ( PI / 4) < s & s < ((3 / 4) * PI );

        

         A8: ].( PI / 4), ((3 / 4) * PI ).[ c= [.( PI / 4), ((3 / 4) * PI ).] by XXREAL_1: 25;

        

         A9: ( [.( PI / 4), ((3 / 4) * PI ).] /\ ( dom cot )) = [.( PI / 4), ((3 / 4) * PI ).] by A5, Th2, XBOOLE_1: 1, XBOOLE_1: 28;

        ((3 / 4) * PI ) in { s where s be Real : ( PI / 4) <= s & s <= ((3 / 4) * PI ) } by A1;

        then ((3 / 4) * PI ) in ( [.( PI / 4), ((3 / 4) * PI ).] /\ ( dom cot )) by A9, RCOMP_1:def 1;

        then

         A10: ( - 1) < ( cot . x) by A3, A6, A9, A8, A7, Th18, RFUNCT_2: 21;

        ( PI / 4) in { s where s be Real : ( PI / 4) <= s & s <= ((3 / 4) * PI ) } by A1;

        then ( PI / 4) in ( [.( PI / 4), ((3 / 4) * PI ).] /\ ( dom cot )) by A9, RCOMP_1:def 1;

        then ( cot . x) < 1 by A3, A6, A9, A8, A4, Th18, RFUNCT_2: 21;

        then ( cot . x) in { s where s be Real : ( - 1) < s & s < 1 } by A10;

        then

         A11: ( cot . x) in ].( - 1), 1.[ by RCOMP_1:def 2;

         ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

        hence thesis by A11;

      end;

        suppose x = ( PI / 4);

        then ( cot . x) in { s where s be Real : ( - 1) <= s & s <= 1 } by Th18;

        hence thesis by RCOMP_1:def 1;

      end;

        suppose x = ((3 / 4) * PI );

        then ( cot . x) in { s where s be Real : ( - 1) <= s & s <= 1 } by Th18;

        hence thesis by RCOMP_1:def 1;

      end;

    end;

    theorem :: SIN_COS9:21

    

     Th21: ( rng ( tan | [.( - ( PI / 4)), ( PI / 4).])) = [.( - 1), 1.]

    proof

      now

        let y be object;

        thus y in [.( - 1), 1.] implies ex x be object st x in ( dom ( tan | [.( - ( PI / 4)), ( PI / 4).])) & y = (( tan | [.( - ( PI / 4)), ( PI / 4).]) . x)

        proof

          assume

           A1: y in [.( - 1), 1.];

          then

          reconsider y1 = y as Real;

          y1 in [.( tan . ( - ( PI / 4))), ( tan . ( PI / 4)).] by A1, Th17, SIN_COS:def 28;

          then

           A2: y1 in ( [.( tan . ( - ( PI / 4))), ( tan . ( PI / 4)).] \/ [.( tan . ( PI / 4)), ( tan . ( - ( PI / 4))).]) by XBOOLE_0:def 3;

          

           A3: [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

          ( tan | ].( - ( PI / 2)), ( PI / 2).[) is continuous by Lm1, FDIFF_1: 25;

          then ( tan | [.( - ( PI / 4)), ( PI / 4).]) is continuous by A3, FCONT_1: 16;

          then

          consider x be Real such that

           A4: x in [.( - ( PI / 4)), ( PI / 4).] and

           A5: y1 = ( tan . x) by A3, A2, Th1, FCONT_2: 15, XBOOLE_1: 1;

          take x;

          thus thesis by A4, A5, Lm11, FUNCT_1: 49;

        end;

        thus (ex x be object st x in ( dom ( tan | [.( - ( PI / 4)), ( PI / 4).])) & y = (( tan | [.( - ( PI / 4)), ( PI / 4).]) . x)) implies y in [.( - 1), 1.]

        proof

          given x be object such that

           A6: x in ( dom ( tan | [.( - ( PI / 4)), ( PI / 4).])) and

           A7: y = (( tan | [.( - ( PI / 4)), ( PI / 4).]) . x);

          reconsider x1 = x as Real by A6;

          y = ( tan . x1) by A6, A7, Lm11, FUNCT_1: 49;

          hence thesis by A6, Lm11, Th19;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SIN_COS9:22

    

     Th22: ( rng ( cot | [.( PI / 4), ((3 / 4) * PI ).])) = [.( - 1), 1.]

    proof

      now

        let y be object;

        thus y in [.( - 1), 1.] implies ex x be object st x in ( dom ( cot | [.( PI / 4), ((3 / 4) * PI ).])) & y = (( cot | [.( PI / 4), ((3 / 4) * PI ).]) . x)

        proof

          

           A1: (( PI / 4) * 3) > ( PI / 4) by XREAL_1: 155;

          assume

           A2: y in [.( - 1), 1.];

          then

          reconsider y1 = y as Real;

          

           A3: y1 in ( [.( cot . ((3 / 4) * PI )), ( cot . ( PI / 4)).] \/ [.( cot . ( PI / 4)), ( cot . ((3 / 4) * PI )).]) by A2, Th18, XBOOLE_0:def 3;

          

           A4: [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

          ( cot | ]. 0 , PI .[) is continuous by Lm2, FDIFF_1: 25;

          then ( cot | [.( PI / 4), ((3 / 4) * PI ).]) is continuous by A4, FCONT_1: 16;

          then

          consider x be Real such that

           A5: x in [.( PI / 4), ((3 / 4) * PI ).] and

           A6: y1 = ( cot . x) by A1, A4, A3, Th2, FCONT_2: 15, XBOOLE_1: 1;

          take x;

          thus thesis by A5, A6, Lm12, FUNCT_1: 49;

        end;

        thus (ex x be object st x in ( dom ( cot | [.( PI / 4), ((3 / 4) * PI ).])) & y = (( cot | [.( PI / 4), ((3 / 4) * PI ).]) . x)) implies y in [.( - 1), 1.]

        proof

          given x be object such that

           A7: x in ( dom ( cot | [.( PI / 4), ((3 / 4) * PI ).])) and

           A8: y = (( cot | [.( PI / 4), ((3 / 4) * PI ).]) . x);

          reconsider x1 = x as Real by A7;

          y = ( cot . x1) by A7, A8, Lm12, FUNCT_1: 49;

          hence thesis by A7, Lm12, Th20;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SIN_COS9:23

    

     Th23: [.( - 1), 1.] c= ( dom arctan )

    proof

      

       A1: [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      ( rng ( tan | [.( - ( PI / 4)), ( PI / 4).])) c= ( rng ( tan | ].( - ( PI / 2)), ( PI / 2).[))

      proof

        let y be object;

        assume y in ( rng ( tan | [.( - ( PI / 4)), ( PI / 4).]));

        then y in ( tan .: [.( - ( PI / 4)), ( PI / 4).]) by RELAT_1: 115;

        then ex x be object st x in ( dom tan ) & x in [.( - ( PI / 4)), ( PI / 4).] & y = ( tan . x) by FUNCT_1:def 6;

        then y in ( tan .: ].( - ( PI / 2)), ( PI / 2).[) by A1, FUNCT_1:def 6;

        hence thesis by RELAT_1: 115;

      end;

      hence thesis by Th21, FUNCT_1: 33;

    end;

    theorem :: SIN_COS9:24

    

     Th24: [.( - 1), 1.] c= ( dom arccot )

    proof

      

       A1: [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

      ( rng ( cot | [.( PI / 4), ((3 / 4) * PI ).])) c= ( rng ( cot | ]. 0 , PI .[))

      proof

        let y be object;

        assume y in ( rng ( cot | [.( PI / 4), ((3 / 4) * PI ).]));

        then y in ( cot .: [.( PI / 4), ((3 / 4) * PI ).]) by RELAT_1: 115;

        then ex x be object st x in ( dom cot ) & x in [.( PI / 4), ((3 / 4) * PI ).] & y = ( cot . x) by FUNCT_1:def 6;

        then y in ( cot .: ]. 0 , PI .[) by A1, FUNCT_1:def 6;

        hence thesis by RELAT_1: 115;

      end;

      hence thesis by Th22, FUNCT_1: 33;

    end;

    

     Lm13: (( tan | [.( - ( PI / 4)), ( PI / 4).]) | [.( - ( PI / 4)), ( PI / 4).]) is increasing

    proof

       [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      then ( tan | [.( - ( PI / 4)), ( PI / 4).]) is increasing by Th7, RFUNCT_2: 28;

      hence thesis;

    end;

    

     Lm14: (( cot | [.( PI / 4), ((3 / 4) * PI ).]) | [.( PI / 4), ((3 / 4) * PI ).]) is decreasing

    proof

       [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

      then ( cot | [.( PI / 4), ((3 / 4) * PI ).]) is decreasing by Th8, RFUNCT_2: 29;

      hence thesis;

    end;

    

     Lm15: ( tan | [.( - ( PI / 4)), ( PI / 4).]) is one-to-one

    proof

       [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      then (( tan | ].( - ( PI / 2)), ( PI / 2).[) | [.( - ( PI / 4)), ( PI / 4).]) = ( tan | [.( - ( PI / 4)), ( PI / 4).]) by RELAT_1: 74;

      hence thesis;

    end;

    

     Lm16: ( cot | [.( PI / 4), ((3 / 4) * PI ).]) is one-to-one

    proof

       [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

      then (( cot | ]. 0 , PI .[) | [.( PI / 4), ((3 / 4) * PI ).]) = ( cot | [.( PI / 4), ((3 / 4) * PI ).]) by RELAT_1: 74;

      hence thesis;

    end;

    registration

      cluster ( tan | [.( - ( PI / 4)), ( PI / 4).]) -> one-to-one;

      coherence by Lm15;

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

      coherence by Lm16;

    end

    theorem :: SIN_COS9:25

    

     Th25: ( arctan | [.( - 1), 1.]) = (( tan | [.( - ( PI / 4)), ( PI / 4).]) " )

    proof

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

      

       A1: [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      

      then (( tan | [.( - ( PI / 4)), ( PI / 4).]) " ) = ((h | [.( - ( PI / 4)), ( PI / 4).]) " ) by RELAT_1: 74

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

      .= ((h " ) | ( rng (h | [.( - ( PI / 4)), ( PI / 4).]))) by RELAT_1: 115

      .= ((h " ) | [.( - 1), 1.]) by A1, Th21, RELAT_1: 74;

      hence thesis;

    end;

    theorem :: SIN_COS9:26

    

     Th26: ( arccot | [.( - 1), 1.]) = (( cot | [.( PI / 4), ((3 / 4) * PI ).]) " )

    proof

      set h = ( cot | ]. 0 , PI .[);

      

       A1: [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

      

      then (( cot | [.( PI / 4), ((3 / 4) * PI ).]) " ) = ((h | [.( PI / 4), ((3 / 4) * PI ).]) " ) by RELAT_1: 74

      .= ((h " ) | (h .: [.( PI / 4), ((3 / 4) * PI ).])) by RFUNCT_2: 17

      .= ((h " ) | ( rng (h | [.( PI / 4), ((3 / 4) * PI ).]))) by RELAT_1: 115

      .= ((h " ) | [.( - 1), 1.]) by A1, Th22, RELAT_1: 74;

      hence thesis;

    end;

    theorem :: SIN_COS9:27

    (( tan | [.( - ( PI / 4)), ( PI / 4).]) qua Function * ( arctan | [.( - 1), 1.])) = ( id [.( - 1), 1.]) by Th21, Th25, FUNCT_1: 39;

    theorem :: SIN_COS9:28

    (( cot | [.( PI / 4), ((3 / 4) * PI ).]) qua Function * ( arccot | [.( - 1), 1.])) = ( id [.( - 1), 1.]) by Th22, Th26, FUNCT_1: 39;

    theorem :: SIN_COS9:29

    (( tan | [.( - ( PI / 4)), ( PI / 4).]) * ( arctan | [.( - 1), 1.])) = ( id [.( - 1), 1.]) by Th21, Th25, FUNCT_1: 39;

    theorem :: SIN_COS9:30

    (( cot | [.( PI / 4), ((3 / 4) * PI ).]) * ( arccot | [.( - 1), 1.])) = ( id [.( - 1), 1.]) by Th22, Th26, FUNCT_1: 39;

    theorem :: SIN_COS9:31

    

     Th31: ( arctan qua Function * ( tan | ].( - ( PI / 2)), ( PI / 2).[)) = ( id ].( - ( PI / 2)), ( PI / 2).[) by Lm5, Th11, FUNCT_1: 39;

    theorem :: SIN_COS9:32

    

     Th32: ( arccot * ( cot | ]. 0 , PI .[)) = ( id ]. 0 , PI .[) by Lm6, Th12, FUNCT_1: 39;

    theorem :: SIN_COS9:33

    ( arctan qua Function * ( tan | ].( - ( PI / 2)), ( PI / 2).[)) = ( id ].( - ( PI / 2)), ( PI / 2).[) by Lm5, Th11, FUNCT_1: 39;

    theorem :: SIN_COS9:34

    ( arccot qua Function * ( cot | ]. 0 , PI .[)) = ( id ]. 0 , PI .[) by Lm6, Th12, FUNCT_1: 39;

    theorem :: SIN_COS9:35

    

     Th35: ( - ( PI / 2)) < r & r < ( PI / 2) implies ( arctan ( tan . r)) = r & ( arctan ( tan r)) = r

    proof

      assume that

       A1: ( - ( PI / 2)) < r and

       A2: r < ( PI / 2);

      

       A3: ( dom ( tan | ].( - ( PI / 2)), ( PI / 2).[)) = ].( - ( PI / 2)), ( PI / 2).[ by Th1, RELAT_1: 62;

      

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

      

      then ( arctan ( tan . r)) = ( arctan . (( tan | ].( - ( PI / 2)), ( PI / 2).[) . r)) by FUNCT_1: 49

      .= (( id ].( - ( PI / 2)), ( PI / 2).[) . r) by A4, A3, Th31, FUNCT_1: 13

      .= r by A4, FUNCT_1: 18;

      hence thesis by A4, Th13;

    end;

    theorem :: SIN_COS9:36

    

     Th36: 0 < r & r < PI implies ( arccot ( cot . r)) = r & ( arccot ( cot r)) = r

    proof

      assume that

       A1: 0 < r and

       A2: r < PI ;

      

       A3: ( dom ( cot | ]. 0 , PI .[)) = ]. 0 , PI .[ by Th2, RELAT_1: 62;

      

       A4: r in ]. 0 , PI .[ by A1, A2, XXREAL_1: 4;

      

      then ( arccot ( cot . r)) = ( arccot . (( cot | ]. 0 , PI .[) . r)) by FUNCT_1: 49

      .= (( id ]. 0 , PI .[) . r) by A4, A3, Th32, FUNCT_1: 13

      .= r by A4, FUNCT_1: 18;

      hence thesis by A4, Th14;

    end;

    theorem :: SIN_COS9:37

    

     Th37: ( arctan ( - 1)) = ( - ( PI / 4)) & ( arctan . ( - 1)) = ( - ( PI / 4))

    proof

      ( - ( PI / 2)) < ( - ( PI / 4)) by Lm7, XXREAL_1: 4;

      then ( arctan ( - 1)) = ( - ( PI / 4)) by Th17, Th35;

      hence thesis;

    end;

    theorem :: SIN_COS9:38

    

     Th38: ( arccot ( - 1)) = ((3 / 4) * PI ) & ( arccot . ( - 1)) = ((3 / 4) * PI )

    proof

      

       A1: ((3 / 4) * PI ) < PI by Lm10, XXREAL_1: 4;

      ( arccot ( - 1)) = ((3 / 4) * PI ) by A1, Th18, Th36;

      hence thesis;

    end;

    theorem :: SIN_COS9:39

    

     Th39: ( arctan 1) = ( PI / 4) & ( arctan . 1) = ( PI / 4)

    proof

      

       A1: ( arctan 1) = ( arctan ( tan . ( PI / 4))) by SIN_COS:def 28;

      ( PI / 4) < ( PI / 2) by Lm8, XXREAL_1: 4;

      hence thesis by A1, Th35;

    end;

    theorem :: SIN_COS9:40

    

     Th40: ( arccot 1) = ( PI / 4) & ( arccot . 1) = ( PI / 4)

    proof

      

       A1: ( PI / 4) < PI by Lm9, XXREAL_1: 4;

      ( arccot 1) = ( PI / 4) by A1, Th18, Th36;

      hence thesis;

    end;

    theorem :: SIN_COS9:41

    

     Th41: ( tan . 0 ) = 0 & ( tan 0 ) = 0

    proof

      

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

      

      then ( tan . 0 ) = ( 0 / ( cos . 0 )) by Th1, RFUNCT_1:def 1, SIN_COS: 30

      .= 0 ;

      hence thesis by A1, Th13;

    end;

    theorem :: SIN_COS9:42

    

     Th42: ( cot . ( PI / 2)) = 0 & ( cot ( PI / 2)) = 0

    proof

      

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

      

       A2: ( PI / 2) in ]. 0 , PI .[ by A1, XXREAL_1: 4;

      

      then ( cot . ( PI / 2)) = ( 0 / ( sin . ( PI / 2))) by Th2, RFUNCT_1:def 1, SIN_COS: 76

      .= 0 ;

      hence thesis by A2, Th14;

    end;

    theorem :: SIN_COS9:43

    ( arctan 0 ) = 0 & ( arctan . 0 ) = 0

    proof

      ( arctan 0 ) = 0 by Th35, Th41;

      hence thesis;

    end;

    theorem :: SIN_COS9:44

    ( arccot 0 ) = ( PI / 2) & ( arccot . 0 ) = ( PI / 2)

    proof

      

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

      ( arccot 0 ) = ( PI / 2) by A1, Th36, Th42;

      hence thesis;

    end;

    theorem :: SIN_COS9:45

    

     Th45: ( arctan | ( tan .: ].( - ( PI / 2)), ( PI / 2).[)) is increasing

    proof

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

      

       A1: (f .: ].( - ( PI / 2)), ( PI / 2).[) = ( rng (f | ].( - ( PI / 2)), ( PI / 2).[)) by RELAT_1: 115

      .= ( rng ( tan | ].( - ( PI / 2)), ( PI / 2).[)) by RELAT_1: 73

      .= ( tan .: ].( - ( PI / 2)), ( PI / 2).[) by RELAT_1: 115;

      (f | ].( - ( PI / 2)), ( PI / 2).[) = f by RELAT_1: 73;

      hence thesis by A1, Th7, FCONT_3: 9;

    end;

    theorem :: SIN_COS9:46

    

     Th46: ( arccot | ( cot .: ]. 0 , PI .[)) is decreasing

    proof

      set f = ( cot | ]. 0 , PI .[);

      

       A1: (f .: ]. 0 , PI .[) = ( rng (f | ]. 0 , PI .[)) by RELAT_1: 115

      .= ( rng ( cot | ]. 0 , PI .[)) by RELAT_1: 73

      .= ( cot .: ]. 0 , PI .[) by RELAT_1: 115;

      (f | ]. 0 , PI .[) = f by RELAT_1: 73;

      hence thesis by A1, Th8, FCONT_3: 10;

    end;

    theorem :: SIN_COS9:47

    

     Th47: ( arctan | [.( - 1), 1.]) is increasing

    proof

      

       A1: [.( - 1), 1.] = ( tan .: [.( - ( PI / 4)), ( PI / 4).]) by Th21, RELAT_1: 115;

       [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      hence thesis by A1, Th45, RELAT_1: 123, RFUNCT_2: 28;

    end;

    theorem :: SIN_COS9:48

    

     Th48: ( arccot | [.( - 1), 1.]) is decreasing

    proof

      

       A1: [.( - 1), 1.] = ( cot .: [.( PI / 4), ((3 / 4) * PI ).]) by Th22, RELAT_1: 115;

       [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

      hence thesis by A1, Th46, RELAT_1: 123, RFUNCT_2: 29;

    end;

    theorem :: SIN_COS9:49

    

     Th49: for x be set st x in [.( - 1), 1.] holds ( arctan . x) in [.( - ( PI / 4)), ( PI / 4).]

    proof

      let x be set;

      assume x in [.( - 1), 1.];

      then x in ( ].( - 1), 1.[ \/ {( - 1), 1}) by XXREAL_1: 128;

      then

       A1: x in ].( - 1), 1.[ or x in {( - 1), 1} by XBOOLE_0:def 3;

      per cases by A1, TARSKI:def 2;

        suppose

         A2: x in ].( - 1), 1.[;

        then x in { s where s be Real : ( - 1) < s & s < 1 } by RCOMP_1:def 2;

        then

         A3: ex s be Real st s = x & ( - 1) < s & s < 1;

        

         A4: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

        

         A5: ( [.( - 1), 1.] /\ ( dom arctan )) = [.( - 1), 1.] by Th23, XBOOLE_1: 28;

        then 1 in ( [.( - 1), 1.] /\ ( dom arctan )) by XXREAL_1: 1;

        then

         A6: ( arctan . x) < ( PI / 4) by A2, A5, A4, A3, Th39, Th47, RFUNCT_2: 20;

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

        then ( - ( PI / 4)) < ( arctan . x) by A2, A5, A4, A3, Th37, Th47, RFUNCT_2: 20;

        hence thesis by A6, XXREAL_1: 1;

      end;

        suppose x = ( - 1);

        hence thesis by Th37, XXREAL_1: 1;

      end;

        suppose x = 1;

        hence thesis by Th39, XXREAL_1: 1;

      end;

    end;

    theorem :: SIN_COS9:50

    

     Th50: for x be set st x in [.( - 1), 1.] holds ( arccot . x) in [.( PI / 4), ((3 / 4) * PI ).]

    proof

      let x be set;

      assume x in [.( - 1), 1.];

      then x in ( ].( - 1), 1.[ \/ {( - 1), 1}) by XXREAL_1: 128;

      then

       A1: x in ].( - 1), 1.[ or x in {( - 1), 1} by XBOOLE_0:def 3;

      per cases by A1, TARSKI:def 2;

        suppose

         A2: x in ].( - 1), 1.[;

        then x in { s where s be Real : ( - 1) < s & s < 1 } by RCOMP_1:def 2;

        then

         A3: ex s be Real st s = x & ( - 1) < s & s < 1;

        

         A4: ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

        

         A5: ( [.( - 1), 1.] /\ ( dom arccot )) = [.( - 1), 1.] by Th24, XBOOLE_1: 28;

        then 1 in ( [.( - 1), 1.] /\ ( dom arccot )) by XXREAL_1: 1;

        then

         A6: ( arccot . x) > ( PI / 4) by A2, A5, A4, A3, Th40, Th48, RFUNCT_2: 21;

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

        then ((3 / 4) * PI ) > ( arccot . x) by A2, A5, A4, A3, Th38, Th48, RFUNCT_2: 21;

        hence thesis by A6, XXREAL_1: 1;

      end;

        suppose

         A7: x = ( - 1);

        ( PI / 4) < (( PI / 4) * 3) by XREAL_1: 155;

        hence thesis by A7, Th38, XXREAL_1: 1;

      end;

        suppose

         A8: x = 1;

        ( PI / 4) < (( PI / 4) * 3) by XREAL_1: 155;

        hence thesis by A8, Th40, XXREAL_1: 1;

      end;

    end;

    theorem :: SIN_COS9:51

    

     Th51: ( - 1) <= r & r <= 1 implies ( tan ( arctan r)) = r

    proof

      

       A1: [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      assume that

       A2: ( - 1) <= r and

       A3: r <= 1;

      

       A4: r in [.( - 1), 1.] by A2, A3, XXREAL_1: 1;

      then

       A5: r in ( dom ( arctan | [.( - 1), 1.])) by Th23, RELAT_1: 62;

      ( arctan . r) in [.( - ( PI / 4)), ( PI / 4).] by A4, Th49;

      

      hence ( tan ( arctan r)) = ( tan . ( arctan . r)) by A1, Th13

      .= (( tan | [.( - ( PI / 4)), ( PI / 4).]) qua Function . ( arctan . r)) by A4, Th49, FUNCT_1: 49

      .= (( tan | [.( - ( PI / 4)), ( PI / 4).]) qua Function . (( arctan | [.( - 1), 1.]) . r)) by A4, FUNCT_1: 49

      .= ((( tan | [.( - ( PI / 4)), ( PI / 4).]) qua Function * ( arctan | [.( - 1), 1.])) . r) by A5, FUNCT_1: 13

      .= (( id [.( - 1), 1.]) . r) by Th21, Th25, FUNCT_1: 39

      .= r by A4, FUNCT_1: 18;

    end;

    theorem :: SIN_COS9:52

    

     Th52: ( - 1) <= r & r <= 1 implies ( cot ( arccot r)) = r

    proof

      

       A1: [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

      assume that

       A2: ( - 1) <= r and

       A3: r <= 1;

      

       A4: r in [.( - 1), 1.] by A2, A3, XXREAL_1: 1;

      then

       A5: r in ( dom ( arccot | [.( - 1), 1.])) by Th24, RELAT_1: 62;

      ( arccot . r) in [.( PI / 4), ((3 / 4) * PI ).] by A4, Th50;

      

      hence ( cot ( arccot r)) = ( cot . ( arccot . r)) by A1, Th14

      .= (( cot | [.( PI / 4), ((3 / 4) * PI ).]) qua Function . ( arccot . r)) by A4, Th50, FUNCT_1: 49

      .= (( cot | [.( PI / 4), ((3 / 4) * PI ).]) qua Function . (( arccot | [.( - 1), 1.]) . r)) by A4, FUNCT_1: 49

      .= ((( cot | [.( PI / 4), ((3 / 4) * PI ).]) qua Function * ( arccot | [.( - 1), 1.])) . r) by A5, FUNCT_1: 13

      .= (( id [.( - 1), 1.]) . r) by Th22, Th26, FUNCT_1: 39

      .= r by A4, FUNCT_1: 18;

    end;

    theorem :: SIN_COS9:53

    

     Th53: ( arctan | [.( - 1), 1.]) is continuous

    proof

      set f = ( tan | [.( - ( PI / 4)), ( PI / 4).]);

      

       A1: (f | [.( - ( PI / 4)), ( PI / 4).]) = f by RELAT_1: 72;

      (((f | [.( - ( PI / 4)), ( PI / 4).]) " ) | (f .: [.( - ( PI / 4)), ( PI / 4).])) is continuous by Lm11, Lm13, FCONT_1: 47;

      then (( arctan | [.( - 1), 1.]) | [.( - 1), 1.]) is continuous by A1, Th21, Th25, RELAT_1: 115;

      hence thesis by FCONT_1: 15;

    end;

    theorem :: SIN_COS9:54

    

     Th54: ( arccot | [.( - 1), 1.]) is continuous

    proof

      set f = ( cot | [.( PI / 4), ((3 / 4) * PI ).]);

      ( PI / 4) < (( PI / 4) * 3) by XREAL_1: 155;

      then

       A1: (((f | [.( PI / 4), ((3 / 4) * PI ).]) " ) | (f .: [.( PI / 4), ((3 / 4) * PI ).])) is continuous by Lm12, Lm14, FCONT_1: 47;

      (f | [.( PI / 4), ((3 / 4) * PI ).]) = f by RELAT_1: 72;

      then (( arccot | [.( - 1), 1.]) | [.( - 1), 1.]) is continuous by A1, Th22, Th26, RELAT_1: 115;

      hence thesis by FCONT_1: 15;

    end;

    theorem :: SIN_COS9:55

    

     Th55: ( rng ( arctan | [.( - 1), 1.])) = [.( - ( PI / 4)), ( PI / 4).]

    proof

      now

        let y be object;

        thus y in [.( - ( PI / 4)), ( PI / 4).] implies ex x be object st x in ( dom ( arctan | [.( - 1), 1.])) & y = (( arctan | [.( - 1), 1.]) . x)

        proof

          assume

           A1: y in [.( - ( PI / 4)), ( PI / 4).];

          then

          reconsider y1 = y as Real;

          y1 in ( [.( arctan . ( - 1)), ( arctan . 1).] \/ [.( arctan . 1), ( arctan . ( - 1)).]) by A1, Th37, Th39, XBOOLE_0:def 3;

          then

          consider x be Real such that

           A2: x in [.( - 1), 1.] and

           A3: y1 = ( arctan . x) by Th23, Th53, FCONT_2: 15;

          take x;

          thus thesis by A2, A3, Th23, FUNCT_1: 49, RELAT_1: 62;

        end;

        thus (ex x be object st x in ( dom ( arctan | [.( - 1), 1.])) & y = (( arctan | [.( - 1), 1.]) . x)) implies y in [.( - ( PI / 4)), ( PI / 4).]

        proof

          given x be object such that

           A4: x in ( dom ( arctan | [.( - 1), 1.])) and

           A5: y = (( arctan | [.( - 1), 1.]) . x);

          

           A6: ( dom ( arctan | [.( - 1), 1.])) = [.( - 1), 1.] by Th23, RELAT_1: 62;

          then y = ( arctan . x) by A4, A5, FUNCT_1: 49;

          hence thesis by A4, A6, Th49;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SIN_COS9:56

    

     Th56: ( rng ( arccot | [.( - 1), 1.])) = [.( PI / 4), ((3 / 4) * PI ).]

    proof

      now

        let y be object;

        thus y in [.( PI / 4), ((3 / 4) * PI ).] implies ex x be object st x in ( dom ( arccot | [.( - 1), 1.])) & y = (( arccot | [.( - 1), 1.]) . x)

        proof

          assume

           A1: y in [.( PI / 4), ((3 / 4) * PI ).];

          then

          reconsider y1 = y as Real;

          y1 in ( [.( arccot . 1), ( arccot . ( - 1)).] \/ [.( arccot . ( - 1)), ( arccot . 1).]) by A1, Th38, Th40, XBOOLE_0:def 3;

          then

          consider x be Real such that

           A2: x in [.( - 1), 1.] and

           A3: y1 = ( arccot . x) by Th24, Th54, FCONT_2: 15;

          take x;

          thus thesis by A2, A3, Th24, FUNCT_1: 49, RELAT_1: 62;

        end;

        thus (ex x be object st x in ( dom ( arccot | [.( - 1), 1.])) & y = (( arccot | [.( - 1), 1.]) . x)) implies y in [.( PI / 4), ((3 / 4) * PI ).]

        proof

          given x be object such that

           A4: x in ( dom ( arccot | [.( - 1), 1.])) and

           A5: y = (( arccot | [.( - 1), 1.]) . x);

          

           A6: ( dom ( arccot | [.( - 1), 1.])) = [.( - 1), 1.] by Th24, RELAT_1: 62;

          then y = ( arccot . x) by A4, A5, FUNCT_1: 49;

          hence thesis by A4, A6, Th50;

        end;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: SIN_COS9:57

    ( - 1) <= r & r <= 1 & ( arctan r) = ( - ( PI / 4)) implies r = ( - 1) by Th17, Th51;

    theorem :: SIN_COS9:58

    ( - 1) <= r & r <= 1 & ( arccot r) = ((3 / 4) * PI ) implies r = ( - 1) by Th18, Th52;

    theorem :: SIN_COS9:59

    ( - 1) <= r & r <= 1 & ( arctan r) = 0 implies r = 0 by Th41, Th51;

    theorem :: SIN_COS9:60

    ( - 1) <= r & r <= 1 & ( arccot r) = ( PI / 2) implies r = 0 by Th42, Th52;

    theorem :: SIN_COS9:61

    ( - 1) <= r & r <= 1 & ( arctan r) = ( PI / 4) implies r = 1

    proof

      assume that

       A1: ( - 1) <= r and

       A2: r <= 1 and

       A3: ( arctan r) = ( PI / 4);

      

      thus r = ( tan ( PI / 4)) by A1, A2, A3, Th51

      .= ( tan . ( PI / 4)) by Lm8, Th13

      .= 1 by SIN_COS:def 28;

    end;

    theorem :: SIN_COS9:62

    ( - 1) <= r & r <= 1 & ( arccot r) = ( PI / 4) implies r = 1 by Th18, Th52;

    theorem :: SIN_COS9:63

    

     Th63: ( - 1) <= r & r <= 1 implies ( - ( PI / 4)) <= ( arctan r) & ( arctan r) <= ( PI / 4)

    proof

      assume that

       A1: ( - 1) <= r and

       A2: r <= 1;

      

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

      then r in ( dom ( arctan | [.( - 1), 1.])) by Th23, RELAT_1: 62;

      then (( arctan | [.( - 1), 1.]) . r) in ( rng ( arctan | [.( - 1), 1.])) by FUNCT_1:def 3;

      then ( arctan r) in ( rng ( arctan | [.( - 1), 1.])) by A3, FUNCT_1: 49;

      hence thesis by Th55, XXREAL_1: 1;

    end;

    theorem :: SIN_COS9:64

    

     Th64: ( - 1) <= r & r <= 1 implies ( PI / 4) <= ( arccot r) & ( arccot r) <= ((3 / 4) * PI )

    proof

      assume that

       A1: ( - 1) <= r and

       A2: r <= 1;

      

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

      then r in ( dom ( arccot | [.( - 1), 1.])) by Th24, RELAT_1: 62;

      then (( arccot | [.( - 1), 1.]) . r) in ( rng ( arccot | [.( - 1), 1.])) by FUNCT_1:def 3;

      then ( arccot r) in ( rng ( arccot | [.( - 1), 1.])) by A3, FUNCT_1: 49;

      hence thesis by Th56, XXREAL_1: 1;

    end;

    theorem :: SIN_COS9:65

    ( - 1) < r & r < 1 implies ( - ( PI / 4)) < ( arctan r) & ( arctan r) < ( PI / 4)

    proof

      

       A1: ( tan ( PI / 4)) = ( tan . ( PI / 4)) by Lm8, Th13

      .= 1 by SIN_COS:def 28;

      assume that

       A2: ( - 1) < r and

       A3: r < 1;

      

       A4: ( arctan r) <= ( PI / 4) by A2, A3, Th63;

      ( - ( PI / 4)) <= ( arctan r) by A2, A3, Th63;

      then ( - ( PI / 4)) < ( arctan r) & ( arctan r) < ( PI / 4) or ( - ( PI / 4)) = ( arctan r) or ( arctan r) = ( PI / 4) by A4, XXREAL_0: 1;

      hence thesis by A2, A3, A1, Th17, Th51;

    end;

    theorem :: SIN_COS9:66

    ( - 1) < r & r < 1 implies ( PI / 4) < ( arccot r) & ( arccot r) < ((3 / 4) * PI )

    proof

      assume that

       A1: ( - 1) < r and

       A2: r < 1;

      

       A3: ( arccot r) <= ((3 / 4) * PI ) by A1, A2, Th64;

      ( PI / 4) <= ( arccot r) by A1, A2, Th64;

      then ( PI / 4) < ( arccot r) & ( arccot r) < ((3 / 4) * PI ) or ( PI / 4) = ( arccot r) or ( arccot r) = ((3 / 4) * PI ) by A3, XXREAL_0: 1;

      hence thesis by A1, A2, Th18, Th52;

    end;

    theorem :: SIN_COS9:67

    ( - 1) <= r & r <= 1 implies ( arctan r) = ( - ( arctan ( - r)))

    proof

      

       A1: [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      assume that

       A2: ( - 1) <= r and

       A3: r <= 1;

      

       A4: ( - r) >= ( - 1) by A3, XREAL_1: 24;

      

       A5: ( - ( - 1)) >= ( - r) by A2, XREAL_1: 24;

      then

       A6: ( arctan ( - r)) <= ( PI / 4) by A4, Th63;

      ( - ( PI / 4)) <= ( arctan ( - r)) by A5, A4, Th63;

      then

       A7: ( - ( arctan ( - r))) <= ( - ( - ( PI / 4))) by XREAL_1: 24;

      ( arctan ( - r)) <= ( PI / 4) by A5, A4, Th63;

      then ( - ( PI / 4)) <= ( - ( arctan ( - r))) by XREAL_1: 24;

      then

       A8: ( - ( arctan ( - r))) in [.( - ( PI / 4)), ( PI / 4).] by A7, XXREAL_1: 1;

      ( - ( PI / 4)) <= ( arctan ( - r)) by A5, A4, Th63;

      then ( arctan ( - r)) in [.( - ( PI / 4)), ( PI / 4).] by A6, XXREAL_1: 1;

      then

       A9: ( cos ( arctan ( - r))) <> 0 by A1, COMPTRIG: 11;

      ( tan ( arctan ( - r))) = ( - r) by A5, A4, Th51;

      

      then

       A10: r = ((( tan 0 ) - ( tan ( arctan ( - r)))) / (1 + (( tan 0 ) * ( tan ( arctan ( - r)))))) by Th41

      .= ( tan ( 0 - ( arctan ( - r)))) by A9, SIN_COS: 31, SIN_COS4: 8;

      

       A11: [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      then

       A12: ( - ( arctan ( - r))) < ( PI / 2) by A8, XXREAL_1: 4;

      ( - ( PI / 2)) < ( - ( arctan ( - r))) by A8, A11, XXREAL_1: 4;

      hence thesis by A10, A12, Th35;

    end;

    theorem :: SIN_COS9:68

    ( - 1) <= r & r <= 1 implies ( arccot r) = ( PI - ( arccot ( - r)))

    proof

      set x = ( arccot ( - r));

      assume that

       A1: ( - 1) <= r and

       A2: r <= 1;

      

       A3: ( - r) >= ( - 1) by A2, XREAL_1: 24;

      

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

      then ( - r) = ( cot x) by A3, Th52;

      

      then

       A5: r = ( - ( cot x))

      .= ( - (( cos x) / ( sin x))) by SIN_COS4:def 2

      .= (( cos x) / ( - ( sin x))) by XCMPLX_1: 188

      .= (( cos x) / ( sin ( - x))) by SIN_COS: 31

      .= (( cos ( - x)) / ( sin ( - x))) by SIN_COS: 31

      .= ( cot ( - x)) by SIN_COS4:def 2;

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

      then

       A6: x in [.( PI / 4), ((3 / 4) * PI ).] by Th50;

      then x <= ((3 / 4) * PI ) by XXREAL_1: 1;

      then ( - x) >= ( - ((3 / 4) * PI )) by XREAL_1: 24;

      then

       A7: ( PI + ( - x)) >= ( PI + ( - ((3 / 4) * PI ))) by XREAL_1: 6;

      ( PI / 4) <= x by A6, XXREAL_1: 1;

      then ( - ( PI / 4)) >= ( - x) by XREAL_1: 24;

      then ( PI + ( - ( PI / 4))) >= ( PI + ( - x)) by XREAL_1: 6;

      then

       A8: ( PI + ( - x)) in [.( PI / 4), ((3 / 4) * PI ).] by A7, XXREAL_1: 1;

      

       A9: [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

      then

       A10: ( PI + ( - x)) < PI by A8, XXREAL_1: 4;

      

       A11: ( cot ( PI + ( - x))) = (( cos ( PI + ( - x))) / ( sin ( PI + ( - x)))) by SIN_COS4:def 2

      .= (( - ( cos ( - x))) / ( sin ( PI + ( - x)))) by SIN_COS: 79

      .= (( - ( cos ( - x))) / ( - ( sin ( - x)))) by SIN_COS: 79

      .= (( cos ( - x)) / ( sin ( - x))) by XCMPLX_1: 191

      .= ( cot ( - x)) by SIN_COS4:def 2;

       0 < ( PI + ( - x)) by A8, A9, XXREAL_1: 4;

      hence thesis by A5, A10, A11, Th36;

    end;

    theorem :: SIN_COS9:69

    ( - 1) <= r & r <= 1 implies ( cot ( arctan r)) = (1 / r)

    proof

      set x = ( arctan r);

      assume that

       A1: ( - 1) <= r and

       A2: r <= 1;

      

       A3: (( sin x) / ( cos x)) = ( tan x) by SIN_COS4:def 1

      .= r by A1, A2, Th51;

      ( cot x) = (( cos x) / ( sin x)) by SIN_COS4:def 2

      .= (1 / r) by A3, XCMPLX_1: 57;

      hence thesis;

    end;

    theorem :: SIN_COS9:70

    ( - 1) <= r & r <= 1 implies ( tan ( arccot r)) = (1 / r)

    proof

      set x = ( arccot r);

      assume that

       A1: ( - 1) <= r and

       A2: r <= 1;

      

       A3: (( cos x) / ( sin x)) = ( cot x) by SIN_COS4:def 2

      .= r by A1, A2, Th52;

      ( tan x) = (( sin x) / ( cos x)) by SIN_COS4:def 1

      .= (1 / r) by A3, XCMPLX_1: 57;

      hence thesis;

    end;

    theorem :: SIN_COS9:71

    

     Th71: arctan is_differentiable_on ( tan .: ].( - ( PI / 2)), ( PI / 2).[)

    proof

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

      

       A1: ( dom (f " )) = ( rng ( tan | ].( - ( PI / 2)), ( PI / 2).[)) by FUNCT_1: 33

      .= ( tan .: ].( - ( PI / 2)), ( PI / 2).[) by RELAT_1: 115;

      ( dom f) = (( dom tan ) /\ ].( - ( PI / 2)), ( PI / 2).[) by RELAT_1: 61;

      then

       A2: ].( - ( PI / 2)), ( PI / 2).[ c= ( dom f) by Th1, XBOOLE_1: 19;

      

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

       A4:

      now

        

         A5: for x0 st x0 in ].( - ( PI / 2)), ( PI / 2).[ holds (1 / (( cos . x0) ^2 )) > 0

        proof

          let x0;

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

          then 0 < ( cos . x0) by COMPTRIG: 11;

          then (( cos . x0) ^2 ) > 0 ;

          then (1 / (( cos . x0) ^2 )) > ( 0 / (( cos . x0) ^2 ));

          hence thesis;

        end;

        let x0 such that

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

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

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

        .= ( diff ( tan ,x0)) by A6, Lm1, FDIFF_1:def 7

        .= (1 / (( cos . x0) ^2 )) by A6, Lm3;

        hence 0 < ( diff (f,x0)) by A6, A5;

      end;

      (f | ].( - ( PI / 2)), ( PI / 2).[) = f by RELAT_1: 72;

      hence thesis by A1, A3, A2, A4, FDIFF_2: 48;

    end;

    theorem :: SIN_COS9:72

    

     Th72: arccot is_differentiable_on ( cot .: ]. 0 , PI .[)

    proof

      set f = ( cot | ]. 0 , PI .[);

      

       A1: ( dom (f " )) = ( rng ( cot | ]. 0 , PI .[)) by FUNCT_1: 33

      .= ( cot .: ]. 0 , PI .[) by RELAT_1: 115;

      ( dom f) = (( dom cot ) /\ ]. 0 , PI .[) by RELAT_1: 61;

      then

       A2: ]. 0 , PI .[ c= ( dom f) by Th2, XBOOLE_1: 19;

      

       A3: f is_differentiable_on ]. 0 , PI .[ by Lm2, FDIFF_2: 16;

       A4:

      now

        

         A5: for x0 st x0 in ]. 0 , PI .[ holds ( - (1 / (( sin . x0) ^2 ))) < 0

        proof

          let x0;

          assume x0 in ]. 0 , PI .[;

          then 0 < ( sin . x0) by COMPTRIG: 7;

          then (( sin . x0) ^2 ) > 0 ;

          then (1 / (( sin . x0) ^2 )) > ( 0 / (( sin . x0) ^2 ));

          then ( - (1 / (( sin . x0) ^2 ))) < ( - 0 );

          hence thesis;

        end;

        let x0 such that

         A6: x0 in ]. 0 , PI .[;

        ( diff (f,x0)) = ((f `| ]. 0 , PI .[) . x0) by A3, A6, FDIFF_1:def 7

        .= (( cot `| ]. 0 , PI .[) . x0) by Lm2, FDIFF_2: 16

        .= ( diff ( cot ,x0)) by A6, Lm2, FDIFF_1:def 7

        .= ( - (1 / (( sin . x0) ^2 ))) by A6, Lm4;

        hence ( diff (f,x0)) < 0 by A6, A5;

      end;

      (f | ]. 0 , PI .[) = f by RELAT_1: 72;

      hence thesis by A1, A2, A3, A4, FDIFF_2: 48;

    end;

    theorem :: SIN_COS9:73

    

     Th73: arctan is_differentiable_on ].( - 1), 1.[

    proof

       ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then

       A1: ].( - 1), 1.[ c= ( dom arctan ) by Th23;

      for x st x in ].( - 1), 1.[ holds arctan is_differentiable_in x

      proof

        let x;

        

         A2: ( dom arctan ) = ( rng ( tan | ].( - ( PI / 2)), ( PI / 2).[)) by FUNCT_1: 33

        .= ( tan .: ].( - ( PI / 2)), ( PI / 2).[) by RELAT_1: 115;

        assume x in ].( - 1), 1.[;

        then ( arctan | ( dom arctan )) is_differentiable_in x by A1, A2, Th71, FDIFF_1:def 6;

        hence thesis by RELAT_1: 69;

      end;

      hence thesis by A1, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:74

    

     Th74: arccot is_differentiable_on ].( - 1), 1.[

    proof

       ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then

       A1: ].( - 1), 1.[ c= ( dom arccot ) by Th24;

      for x st x in ].( - 1), 1.[ holds arccot is_differentiable_in x

      proof

        let x;

        

         A2: ( dom arccot ) = ( rng ( cot | ]. 0 , PI .[)) by FUNCT_1: 33

        .= ( cot .: ]. 0 , PI .[) by RELAT_1: 115;

        assume x in ].( - 1), 1.[;

        then ( arccot | ( dom arccot )) is_differentiable_in x by A1, A2, Th72, FDIFF_1:def 6;

        hence thesis by RELAT_1: 69;

      end;

      hence thesis by A1, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:75

    

     Th75: ( - 1) <= r & r <= 1 implies ( diff ( arctan ,r)) = (1 / (1 + (r ^2 )))

    proof

      set g = arctan ;

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

      set x = ( arctan . r);

      assume that

       A1: ( - 1) <= r and

       A2: r <= 1;

      

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

      

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

       A5:

      now

        

         A6: for x0 st x0 in ].( - ( PI / 2)), ( PI / 2).[ holds (1 / (( cos . x0) ^2 )) > 0

        proof

          let x0;

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

          then 0 < ( cos . x0) by COMPTRIG: 11;

          then (( cos . x0) ^2 ) > 0 ;

          then (1 / (( cos . x0) ^2 )) > ( 0 / (( cos . x0) ^2 ));

          hence thesis;

        end;

        let x0 such that

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

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

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

        .= ( diff ( tan ,x0)) by A7, Lm1, FDIFF_1:def 7

        .= (1 / (( cos . x0) ^2 )) by A7, Lm3;

        hence 0 < ( diff (f,x0)) by A7, A6;

      end;

      

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

      then

       A9: x in [.( - ( PI / 4)), ( PI / 4).] by Th49;

      x = ( arctan r);

      

      then

       A10: r = ( tan x) by A1, A2, Th51

      .= (( sin x) / ( cos x)) by SIN_COS4:def 1;

      ( dom f) = (( dom tan ) /\ ].( - ( PI / 2)), ( PI / 2).[) by RELAT_1: 61;

      then

       A11: ].( - ( PI / 2)), ( PI / 2).[ c= ( dom f) by Th1, XBOOLE_1: 19;

      

       A12: (f | ].( - ( PI / 2)), ( PI / 2).[) = f by RELAT_1: 72;

      

       A13: [.( - ( PI / 4)), ( PI / 4).] c= ].( - ( PI / 2)), ( PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;

      then ( cos x) <> 0 by A9, COMPTRIG: 11;

      then (r * ( cos x)) = ( sin x) by A10, XCMPLX_1: 87;

      then

       A14: 1 = ((( cos x) ^2 ) * ((r ^2 ) + 1)) by A3;

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

      

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

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

      .= ( diff ( tan ,x)) by A9, A13, Lm1, FDIFF_1:def 7

      .= (1 / (( cos x) ^2 )) by A9, A13, Lm3;

      

      then ( diff (g,r)) = (1 / (1 / (( cos x) ^2 ))) by A8, A4, A5, A12, A11, Th23, FDIFF_2: 48

      .= (1 / ((r ^2 ) + 1)) by A14, XCMPLX_1: 73;

      hence thesis;

    end;

    theorem :: SIN_COS9:76

    

     Th76: ( - 1) <= r & r <= 1 implies ( diff ( arccot ,r)) = ( - (1 / (1 + (r ^2 ))))

    proof

      set g = arccot ;

      set f = ( cot | ]. 0 , PI .[);

      set x = ( arccot . r);

      assume that

       A1: ( - 1) <= r and

       A2: r <= 1;

      

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

      

       A4: f is_differentiable_on ]. 0 , PI .[ by Lm2, FDIFF_2: 16;

       A5:

      now

        

         A6: for x0 st x0 in ]. 0 , PI .[ holds ( - (1 / (( sin . x0) ^2 ))) < 0

        proof

          let x0;

          assume x0 in ]. 0 , PI .[;

          then 0 < ( sin . x0) by COMPTRIG: 7;

          then (( sin . x0) ^2 ) > 0 ;

          then (1 / (( sin . x0) ^2 )) > ( 0 / (( sin . x0) ^2 ));

          then ( - (1 / (( sin . x0) ^2 ))) < ( - 0 );

          hence thesis;

        end;

        let x0 such that

         A7: x0 in ]. 0 , PI .[;

        ( diff (f,x0)) = ((f `| ]. 0 , PI .[) . x0) by A4, A7, FDIFF_1:def 7

        .= (( cot `| ]. 0 , PI .[) . x0) by Lm2, FDIFF_2: 16

        .= ( diff ( cot ,x0)) by A7, Lm2, FDIFF_1:def 7

        .= ( - (1 / (( sin . x0) ^2 ))) by A7, Lm4;

        hence ( diff (f,x0)) < 0 by A7, A6;

      end;

      

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

      then

       A9: x in [.( PI / 4), ((3 / 4) * PI ).] by Th50;

      x = ( arccot r);

      

      then

       A10: r = ( cot x) by A1, A2, Th52

      .= (( cos x) / ( sin x)) by SIN_COS4:def 2;

      ( dom f) = (( dom cot ) /\ ]. 0 , PI .[) by RELAT_1: 61;

      then

       A11: ]. 0 , PI .[ c= ( dom f) by Th2, XBOOLE_1: 19;

      

       A12: (f | ]. 0 , PI .[) = f by RELAT_1: 72;

      

       A13: [.( PI / 4), ((3 / 4) * PI ).] c= ]. 0 , PI .[ by Lm9, Lm10, XXREAL_2:def 12;

      then ( sin x) <> 0 by A9, COMPTRIG: 7;

      then (r * ( sin x)) = ( cos x) by A10, XCMPLX_1: 87;

      then

       A14: 1 = ((( sin x) ^2 ) * ((r ^2 ) + 1)) by A3;

      f is_differentiable_on ]. 0 , PI .[ by Lm2, FDIFF_2: 16;

      

      then ( diff (f,x)) = ((f `| ]. 0 , PI .[) . x) by A9, A13, FDIFF_1:def 7

      .= (( cot `| ]. 0 , PI .[) . x) by Lm2, FDIFF_2: 16

      .= ( diff ( cot ,x)) by A9, A13, Lm2, FDIFF_1:def 7

      .= ( - (1 / (( sin x) ^2 ))) by A9, A13, Lm4;

      

      then ( diff (g,r)) = (1 / ( - (1 / (( sin x) ^2 )))) by A8, A4, A5, A12, A11, Th24, FDIFF_2: 48

      .= ( - (1 / (1 / (( sin x) ^2 )))) by XCMPLX_1: 188

      .= ( - (1 / ((r ^2 ) + 1))) by A14, XCMPLX_1: 73;

      hence thesis;

    end;

    theorem :: SIN_COS9:77

    ( arctan | ( tan .: ].( - ( PI / 2)), ( PI / 2).[)) is continuous by Th71, FDIFF_1: 25;

    theorem :: SIN_COS9:78

    ( arccot | ( cot .: ]. 0 , PI .[)) is continuous by Th72, FDIFF_1: 25;

    theorem :: SIN_COS9:79

    ( dom arctan ) is open

    proof

      for x0 st x0 in ].( - ( PI / 2)), ( PI / 2).[ holds 0 < ( diff ( tan ,x0))

      proof

        let x0;

        assume

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

        then 0 < ( cos . x0) by COMPTRIG: 11;

        then (( cos . x0) ^2 ) > 0 ;

        then (1 / (( cos . x0) ^2 )) > ( 0 / (( cos . x0) ^2 ));

        hence thesis by A1, Lm3;

      end;

      then ( rng ( tan | ].( - ( PI / 2)), ( PI / 2).[)) is open by Lm1, Th1, FDIFF_2: 41;

      hence thesis by FUNCT_1: 33;

    end;

    theorem :: SIN_COS9:80

    ( dom arccot ) is open

    proof

      for x0 st x0 in ]. 0 , PI .[ holds ( diff ( cot ,x0)) < 0

      proof

        let x0;

        assume

         A1: x0 in ]. 0 , PI .[;

        then 0 < ( sin . x0) by COMPTRIG: 7;

        then (( sin . x0) ^2 ) > 0 ;

        then (1 / (( sin . x0) ^2 )) > ( 0 / (( sin . x0) ^2 ));

        then ( - (1 / (( sin . x0) ^2 ))) < ( - 0 );

        hence thesis by A1, Lm4;

      end;

      then ( rng ( cot | ]. 0 , PI .[)) is open by Lm2, Th2, FDIFF_2: 41;

      hence thesis by FUNCT_1: 33;

    end;

    begin

    theorem :: SIN_COS9:81

    

     Th81: Z c= ].( - 1), 1.[ implies arctan is_differentiable_on Z & for x st x in Z holds (( arctan `| Z) . x) = (1 / (1 + (x ^2 )))

    proof

      assume

       A1: Z c= ].( - 1), 1.[;

      then

       A2: arctan is_differentiable_on Z by Th73, FDIFF_1: 26;

      for x st x in Z holds (( arctan `| Z) . x) = (1 / (1 + (x ^2 )))

      proof

        let x;

        assume

         A3: x in Z;

        then

         A4: ( - 1) <= x by A1, XXREAL_1: 4;

        

         A5: x <= 1 by A1, A3, XXREAL_1: 4;

        

        thus (( arctan `| Z) . x) = ( diff ( arctan ,x)) by A2, A3, FDIFF_1:def 7

        .= (1 / (1 + (x ^2 ))) by A4, A5, Th75;

      end;

      hence thesis by A1, Th73, FDIFF_1: 26;

    end;

    theorem :: SIN_COS9:82

    

     Th82: Z c= ].( - 1), 1.[ implies arccot is_differentiable_on Z & for x st x in Z holds (( arccot `| Z) . x) = ( - (1 / (1 + (x ^2 ))))

    proof

      assume

       A1: Z c= ].( - 1), 1.[;

      then

       A2: arccot is_differentiable_on Z by Th74, FDIFF_1: 26;

      for x st x in Z holds (( arccot `| Z) . x) = ( - (1 / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A3: x in Z;

        then

         A4: ( - 1) <= x by A1, XXREAL_1: 4;

        

         A5: x <= 1 by A1, A3, XXREAL_1: 4;

        

        thus (( arccot `| Z) . x) = ( diff ( arccot ,x)) by A2, A3, FDIFF_1:def 7

        .= ( - (1 / (1 + (x ^2 )))) by A4, A5, Th76;

      end;

      hence thesis by A1, Th74, FDIFF_1: 26;

    end;

    theorem :: SIN_COS9:83

    Z c= ].( - 1), 1.[ implies (r (#) arctan ) is_differentiable_on Z & for x st x in Z holds (((r (#) arctan ) `| Z) . x) = (r / (1 + (x ^2 )))

    proof

      assume

       A1: Z c= ].( - 1), 1.[;

       ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arctan ) by Th23;

      then Z c= ( dom arctan ) by A1;

      then

       A2: Z c= ( dom (r (#) arctan )) by VALUED_1:def 5;

      

       A3: arctan is_differentiable_on Z by A1, Th81;

      for x st x in Z holds (((r (#) arctan ) `| Z) . x) = (r / (1 + (x ^2 )))

      proof

        let x;

        assume

         A4: x in Z;

        then

         A5: ( - 1) < x by A1, XXREAL_1: 4;

        

         A6: x < 1 by A1, A4, XXREAL_1: 4;

        (((r (#) arctan ) `| Z) . x) = (r * ( diff ( arctan ,x))) by A2, A3, A4, FDIFF_1: 20

        .= (r * (1 / (1 + (x ^2 )))) by A5, A6, Th75

        .= (r / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A2, A3, FDIFF_1: 20;

    end;

    theorem :: SIN_COS9:84

    Z c= ].( - 1), 1.[ implies (r (#) arccot ) is_differentiable_on Z & for x st x in Z holds (((r (#) arccot ) `| Z) . x) = ( - (r / (1 + (x ^2 ))))

    proof

      assume

       A1: Z c= ].( - 1), 1.[;

       ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by Th24;

      then Z c= ( dom arccot ) by A1;

      then

       A2: Z c= ( dom (r (#) arccot )) by VALUED_1:def 5;

      

       A3: arccot is_differentiable_on Z by A1, Th82;

      for x st x in Z holds (((r (#) arccot ) `| Z) . x) = ( - (r / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A4: x in Z;

        then

         A5: ( - 1) < x by A1, XXREAL_1: 4;

        

         A6: x < 1 by A1, A4, XXREAL_1: 4;

        (((r (#) arccot ) `| Z) . x) = (r * ( diff ( arccot ,x))) by A2, A3, A4, FDIFF_1: 20

        .= (r * ( - (1 / (1 + (x ^2 ))))) by A5, A6, Th76

        .= ( - (r / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A2, A3, FDIFF_1: 20;

    end;

    theorem :: SIN_COS9:85

    

     Th85: f is_differentiable_in x & (f . x) > ( - 1) & (f . x) < 1 implies ( arctan * f) is_differentiable_in x & ( diff (( arctan * f),x)) = (( diff (f,x)) / (1 + ((f . x) ^2 )))

    proof

      assume that

       A1: f is_differentiable_in x and

       A2: (f . x) > ( - 1) and

       A3: (f . x) < 1;

      (f . x) in ].( - 1), 1.[ by A2, A3, XXREAL_1: 4;

      then

       A4: arctan is_differentiable_in (f . x) by Th73, FDIFF_1: 9;

      

      then ( diff (( arctan * f),x)) = (( diff ( arctan ,(f . x))) * ( diff (f,x))) by A1, FDIFF_2: 13

      .= (( diff (f,x)) * (1 / (1 + ((f . x) ^2 )))) by A2, A3, Th75

      .= (( diff (f,x)) / (1 + ((f . x) ^2 )));

      hence thesis by A1, A4, FDIFF_2: 13;

    end;

    theorem :: SIN_COS9:86

    

     Th86: f is_differentiable_in x & (f . x) > ( - 1) & (f . x) < 1 implies ( arccot * f) is_differentiable_in x & ( diff (( arccot * f),x)) = ( - (( diff (f,x)) / (1 + ((f . x) ^2 ))))

    proof

      assume that

       A1: f is_differentiable_in x and

       A2: (f . x) > ( - 1) and

       A3: (f . x) < 1;

      (f . x) in ].( - 1), 1.[ by A2, A3, XXREAL_1: 4;

      then

       A4: arccot is_differentiable_in (f . x) by Th74, FDIFF_1: 9;

      

      then ( diff (( arccot * f),x)) = (( diff ( arccot ,(f . x))) * ( diff (f,x))) by A1, FDIFF_2: 13

      .= (( diff (f,x)) * ( - (1 / (1 + ((f . x) ^2 ))))) by A2, A3, Th76

      .= ( - (( diff (f,x)) / (1 + ((f . x) ^2 ))));

      hence thesis by A1, A4, FDIFF_2: 13;

    end;

    theorem :: SIN_COS9:87

    

     Th87: Z c= ( dom ( arctan * f)) & (for x st x in Z holds (f . x) = ((r * x) + s) & (f . x) > ( - 1) & (f . x) < 1) implies ( arctan * f) is_differentiable_on Z & for x st x in Z holds ((( arctan * f) `| Z) . x) = (r / (1 + (((r * x) + s) ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( arctan * f)) and

       A2: for x st x in Z holds (f . x) = ((r * x) + s) & (f . x) > ( - 1) & (f . x) < 1;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom f);

      

       A4: for x st x in Z holds (f . x) = ((r * x) + s) by A2;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: for x st x in Z holds ( arctan * f) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: (f . x) > ( - 1) by A2;

        

         A9: (f . x) < 1 by A2, A7;

        f is_differentiable_in x by A5, A7, FDIFF_1: 9;

        hence thesis by A8, A9, Th85;

      end;

      then

       A10: ( arctan * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arctan * f) `| Z) . x) = (r / (1 + (((r * x) + s) ^2 )))

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: (f . x) > ( - 1) by A2;

        

         A13: (f . x) < 1 by A2, A11;

        f is_differentiable_in x by A5, A11, FDIFF_1: 9;

        

        then ( diff (( arctan * f),x)) = (( diff (f,x)) / (1 + ((f . x) ^2 ))) by A12, A13, Th85

        .= (((f `| Z) . x) / (1 + ((f . x) ^2 ))) by A5, A11, FDIFF_1:def 7

        .= (r / (1 + ((f . x) ^2 ))) by A4, A3, A11, FDIFF_1: 23

        .= (r / (1 + (((r * x) + s) ^2 ))) by A2, A11;

        hence thesis by A10, A11, FDIFF_1:def 7;

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:88

    

     Th88: Z c= ( dom ( arccot * f)) & (for x st x in Z holds (f . x) = ((r * x) + s) & (f . x) > ( - 1) & (f . x) < 1) implies ( arccot * f) is_differentiable_on Z & for x st x in Z holds ((( arccot * f) `| Z) . x) = ( - (r / (1 + (((r * x) + s) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( arccot * f)) and

       A2: for x st x in Z holds (f . x) = ((r * x) + s) & (f . x) > ( - 1) & (f . x) < 1;

      for y be object st y in Z holds y in ( dom f) by A1, FUNCT_1: 11;

      then

       A3: Z c= ( dom f);

      

       A4: for x st x in Z holds (f . x) = ((r * x) + s) by A2;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: for x st x in Z holds ( arccot * f) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: (f . x) > ( - 1) by A2;

        

         A9: (f . x) < 1 by A2, A7;

        f is_differentiable_in x by A5, A7, FDIFF_1: 9;

        hence thesis by A8, A9, Th86;

      end;

      then

       A10: ( arccot * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arccot * f) `| Z) . x) = ( - (r / (1 + (((r * x) + s) ^2 ))))

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: (f . x) > ( - 1) by A2;

        

         A13: (f . x) < 1 by A2, A11;

        f is_differentiable_in x by A5, A11, FDIFF_1: 9;

        

        then ( diff (( arccot * f),x)) = ( - (( diff (f,x)) / (1 + ((f . x) ^2 )))) by A12, A13, Th86

        .= ( - (((f `| Z) . x) / (1 + ((f . x) ^2 )))) by A5, A11, FDIFF_1:def 7

        .= ( - (r / (1 + ((f . x) ^2 )))) by A4, A3, A11, FDIFF_1: 23

        .= ( - (r / (1 + (((r * x) + s) ^2 )))) by A2, A11;

        hence thesis by A10, A11, FDIFF_1:def 7;

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:89

    Z c= ( dom ( ln * arctan )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arctan . x) > 0 ) implies ( ln * arctan ) is_differentiable_on Z & for x st x in Z holds ((( ln * arctan ) `| Z) . x) = (1 / ((1 + (x ^2 )) * ( arctan . x)))

    proof

      assume that

       A1: Z c= ( dom ( ln * arctan )) and

       A2: Z c= ].( - 1), 1.[ and

       A3: for x st x in Z holds ( arctan . x) > 0 ;

      

       A4: for x st x in Z holds ( ln * arctan ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

         arctan is_differentiable_on Z by A2, Th81;

        then

         A6: arctan is_differentiable_in x by A5, FDIFF_1: 9;

        ( arctan . x) > 0 by A3, A5;

        hence thesis by A6, TAYLOR_1: 20;

      end;

      then

       A7: ( ln * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * arctan ) `| Z) . x) = (1 / ((1 + (x ^2 )) * ( arctan . x)))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( - 1) < x by A2, XXREAL_1: 4;

         arctan is_differentiable_on Z by A2, Th81;

        then

         A10: arctan is_differentiable_in x by A8, FDIFF_1: 9;

        

         A11: x < 1 by A2, A8, XXREAL_1: 4;

        ( arctan . x) > 0 by A3, A8;

        

        then ( diff (( ln * arctan ),x)) = (( diff ( arctan ,x)) / ( arctan . x)) by A10, TAYLOR_1: 20

        .= ((1 / (1 + (x ^2 ))) / ( arctan . x)) by A9, A11, Th75

        .= (1 / ((1 + (x ^2 )) * ( arctan . x))) by XCMPLX_1: 78;

        hence thesis by A7, A8, FDIFF_1:def 7;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:90

    Z c= ( dom ( ln * arccot )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds ( arccot . x) > 0 ) implies ( ln * arccot ) is_differentiable_on Z & for x st x in Z holds ((( ln * arccot ) `| Z) . x) = ( - (1 / ((1 + (x ^2 )) * ( arccot . x))))

    proof

      assume that

       A1: Z c= ( dom ( ln * arccot )) and

       A2: Z c= ].( - 1), 1.[ and

       A3: for x st x in Z holds ( arccot . x) > 0 ;

      

       A4: for x st x in Z holds ( ln * arccot ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

         arccot is_differentiable_on Z by A2, Th82;

        then

         A6: arccot is_differentiable_in x by A5, FDIFF_1: 9;

        ( arccot . x) > 0 by A3, A5;

        hence thesis by A6, TAYLOR_1: 20;

      end;

      then

       A7: ( ln * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * arccot ) `| Z) . x) = ( - (1 / ((1 + (x ^2 )) * ( arccot . x))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( - 1) < x by A2, XXREAL_1: 4;

         arccot is_differentiable_on Z by A2, Th82;

        then

         A10: arccot is_differentiable_in x by A8, FDIFF_1: 9;

        

         A11: x < 1 by A2, A8, XXREAL_1: 4;

        ( arccot . x) > 0 by A3, A8;

        

        then ( diff (( ln * arccot ),x)) = (( diff ( arccot ,x)) / ( arccot . x)) by A10, TAYLOR_1: 20

        .= (( - (1 / (1 + (x ^2 )))) / ( arccot . x)) by A9, A11, Th76

        .= ( - ((1 / (1 + (x ^2 ))) / ( arccot . x)))

        .= ( - (1 / ((1 + (x ^2 )) * ( arccot . x)))) by XCMPLX_1: 78;

        hence thesis by A7, A8, FDIFF_1:def 7;

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:91

    

     Th91: Z c= ( dom (( #Z n) * arctan )) & Z c= ].( - 1), 1.[ implies (( #Z n) * arctan ) is_differentiable_on Z & for x st x in Z holds (((( #Z n) * arctan ) `| Z) . x) = ((n * (( arctan . x) #Z (n - 1))) / (1 + (x ^2 )))

    proof

      assume that

       A1: Z c= ( dom (( #Z n) * arctan )) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: for x st x in Z holds (( #Z n) * arctan ) is_differentiable_in x

      proof

        let x;

        assume

         A4: x in Z;

         arctan is_differentiable_on Z by A2, Th81;

        then arctan is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A5: (( #Z n) * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #Z n) * arctan ) `| Z) . x) = ((n * (( arctan . x) #Z (n - 1))) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( - 1) < x by A2, XXREAL_1: 4;

         arctan is_differentiable_on Z by A2, Th81;

        then

         A8: arctan is_differentiable_in x by A6, FDIFF_1: 9;

        

         A9: x < 1 by A2, A6, XXREAL_1: 4;

        (((( #Z n) * arctan ) `| Z) . x) = ( diff ((( #Z n) * arctan ),x)) by A5, A6, FDIFF_1:def 7

        .= ((n * (( arctan . x) #Z (n - 1))) * ( diff ( arctan ,x))) by A8, TAYLOR_1: 3

        .= ((n * (( arctan . x) #Z (n - 1))) * (1 / (1 + (x ^2 )))) by A7, A9, Th75

        .= ((n * (( arctan . x) #Z (n - 1))) / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:92

    

     Th92: Z c= ( dom (( #Z n) * arccot )) & Z c= ].( - 1), 1.[ implies (( #Z n) * arccot ) is_differentiable_on Z & for x st x in Z holds (((( #Z n) * arccot ) `| Z) . x) = ( - ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom (( #Z n) * arccot )) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: for x st x in Z holds (( #Z n) * arccot ) is_differentiable_in x

      proof

        let x;

        assume

         A4: x in Z;

         arccot is_differentiable_on Z by A2, Th82;

        then arccot is_differentiable_in x by A4, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A5: (( #Z n) * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #Z n) * arccot ) `| Z) . x) = ( - ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( - 1) < x by A2, XXREAL_1: 4;

         arccot is_differentiable_on Z by A2, Th82;

        then

         A8: arccot is_differentiable_in x by A6, FDIFF_1: 9;

        

         A9: x < 1 by A2, A6, XXREAL_1: 4;

        (((( #Z n) * arccot ) `| Z) . x) = ( diff ((( #Z n) * arccot ),x)) by A5, A6, FDIFF_1:def 7

        .= ((n * (( arccot . x) #Z (n - 1))) * ( diff ( arccot ,x))) by A8, TAYLOR_1: 3

        .= ((n * (( arccot . x) #Z (n - 1))) * ( - (1 / (1 + (x ^2 ))))) by A7, A9, Th76

        .= ( - ((n * (( arccot . x) #Z (n - 1))) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:93

    Z c= ( dom ((1 / 2) (#) (( #Z 2) * arctan ))) & Z c= ].( - 1), 1.[ implies ((1 / 2) (#) (( #Z 2) * arctan )) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) (( #Z 2) * arctan )) `| Z) . x) = (( arctan . x) / (1 + (x ^2 )))

    proof

      assume that

       A1: Z c= ( dom ((1 / 2) (#) (( #Z 2) * arctan ))) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: Z c= ( dom (( #Z 2) * arctan )) by A1, VALUED_1:def 5;

      then

       A4: (( #Z 2) * arctan ) is_differentiable_on Z by A2, Th91;

      for x st x in Z holds ((((1 / 2) (#) (( #Z 2) * arctan )) `| Z) . x) = (( arctan . x) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((((1 / 2) (#) (( #Z 2) * arctan )) `| Z) . x) = ((1 / 2) * ( diff ((( #Z 2) * arctan ),x))) by A1, A4, FDIFF_1: 20

        .= ((1 / 2) * (((( #Z 2) * arctan ) `| Z) . x)) by A4, A5, FDIFF_1:def 7

        .= ((1 / 2) * ((2 * (( arctan . x) #Z (2 - 1))) / (1 + (x ^2 )))) by A2, A3, A5, Th91

        .= ((1 / 2) * ((2 * ( arctan . x)) / (1 + (x ^2 )))) by PREPOWER: 35

        .= (( arctan . x) / (1 + (x ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: SIN_COS9:94

    Z c= ( dom ((1 / 2) (#) (( #Z 2) * arccot ))) & Z c= ].( - 1), 1.[ implies ((1 / 2) (#) (( #Z 2) * arccot )) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) (( #Z 2) * arccot )) `| Z) . x) = ( - (( arccot . x) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ((1 / 2) (#) (( #Z 2) * arccot ))) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: Z c= ( dom (( #Z 2) * arccot )) by A1, VALUED_1:def 5;

      then

       A4: (( #Z 2) * arccot ) is_differentiable_on Z by A2, Th92;

      for x st x in Z holds ((((1 / 2) (#) (( #Z 2) * arccot )) `| Z) . x) = ( - (( arccot . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((((1 / 2) (#) (( #Z 2) * arccot )) `| Z) . x) = ((1 / 2) * ( diff ((( #Z 2) * arccot ),x))) by A1, A4, FDIFF_1: 20

        .= ((1 / 2) * (((( #Z 2) * arccot ) `| Z) . x)) by A4, A5, FDIFF_1:def 7

        .= ((1 / 2) * ( - ((2 * (( arccot . x) #Z (2 - 1))) / (1 + (x ^2 ))))) by A2, A3, A5, Th92

        .= ( - ((1 / 2) * ((2 * (( arccot . x) #Z 1)) / (1 + (x ^2 )))))

        .= ( - ((1 / 2) * ((2 * ( arccot . x)) / (1 + (x ^2 ))))) by PREPOWER: 35

        .= ( - (( arccot . x) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A4, FDIFF_1: 20;

    end;

    theorem :: SIN_COS9:95

    

     Th95: Z c= ].( - 1), 1.[ implies (( id Z) (#) arctan ) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) arctan ) `| Z) . x) = (( arctan . x) + (x / (1 + (x ^2 ))))

    proof

      assume

       A1: Z c= ].( - 1), 1.[;

      

       A2: Z c= ( dom ( id Z)) by FUNCT_1: 17;

       ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arctan ) by Th23;

      then Z c= ( dom arctan ) by A1;

      then Z c= (( dom ( id Z)) /\ ( dom arctan )) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom (( id Z) (#) arctan )) by VALUED_1:def 4;

      

       A4: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      then

       A5: ( id Z) is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A6: arctan is_differentiable_on Z by A1, Th81;

      for x st x in Z holds (((( id Z) (#) arctan ) `| Z) . x) = (( arctan . x) + (x / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( - 1) < x by A1, XXREAL_1: 4;

        

         A9: x < 1 by A1, A7, XXREAL_1: 4;

        (((( id Z) (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff ( arctan ,x)))) by A3, A5, A6, A7, FDIFF_1: 21

        .= ((( arctan . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff ( arctan ,x)))) by A5, A7, FDIFF_1:def 7

        .= ((( arctan . x) * 1) + ((( id Z) . x) * ( diff ( arctan ,x)))) by A2, A4, A7, FDIFF_1: 23

        .= (( arctan . x) + (x * ( diff ( arctan ,x)))) by A7, FUNCT_1: 18

        .= (( arctan . x) + (x * (1 / (1 + (x ^2 ))))) by A8, A9, Th75

        .= (( arctan . x) + (x / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A3, A5, A6, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:96

    

     Th96: Z c= ].( - 1), 1.[ implies (( id Z) (#) arccot ) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) arccot ) `| Z) . x) = (( arccot . x) - (x / (1 + (x ^2 ))))

    proof

      assume

       A1: Z c= ].( - 1), 1.[;

      

       A2: Z c= ( dom ( id Z)) by FUNCT_1: 17;

       ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by Th24;

      then Z c= ( dom arccot ) by A1;

      then Z c= (( dom ( id Z)) /\ ( dom arccot )) by A2, XBOOLE_1: 19;

      then

       A3: Z c= ( dom (( id Z) (#) arccot )) by VALUED_1:def 4;

      

       A4: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      then

       A5: ( id Z) is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A6: arccot is_differentiable_on Z by A1, Th82;

      for x st x in Z holds (((( id Z) (#) arccot ) `| Z) . x) = (( arccot . x) - (x / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( - 1) < x by A1, XXREAL_1: 4;

        

         A9: x < 1 by A1, A7, XXREAL_1: 4;

        (((( id Z) (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff ( arccot ,x)))) by A3, A5, A6, A7, FDIFF_1: 21

        .= ((( arccot . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff ( arccot ,x)))) by A5, A7, FDIFF_1:def 7

        .= ((( arccot . x) * 1) + ((( id Z) . x) * ( diff ( arccot ,x)))) by A2, A4, A7, FDIFF_1: 23

        .= (( arccot . x) + (x * ( diff ( arccot ,x)))) by A7, FUNCT_1: 18

        .= (( arccot . x) + (x * ( - (1 / (1 + (x ^2 )))))) by A8, A9, Th76

        .= (( arccot . x) - (x / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A3, A5, A6, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:97

    Z c= ( dom (f (#) arctan )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f . x) = ((r * x) + s)) implies (f (#) arctan ) is_differentiable_on Z & for x st x in Z holds (((f (#) arctan ) `| Z) . x) = ((r * ( arctan . x)) + (((r * x) + s) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom (f (#) arctan )) and

       A2: Z c= ].( - 1), 1.[ and

       A3: for x st x in Z holds (f . x) = ((r * x) + s);

      Z c= (( dom f) /\ ( dom arctan )) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom f) by XBOOLE_1: 18;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: arctan is_differentiable_on Z by A2, Th81;

      for x st x in Z holds (((f (#) arctan ) `| Z) . x) = ((r * ( arctan . x)) + (((r * x) + s) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( - 1) < x by A2, XXREAL_1: 4;

        

         A9: x < 1 by A2, A7, XXREAL_1: 4;

        (((f (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff (f,x))) + ((f . x) * ( diff ( arctan ,x)))) by A1, A5, A6, A7, FDIFF_1: 21

        .= ((( arctan . x) * ((f `| Z) . x)) + ((f . x) * ( diff ( arctan ,x)))) by A5, A7, FDIFF_1:def 7

        .= ((( arctan . x) * r) + ((f . x) * ( diff ( arctan ,x)))) by A3, A4, A7, FDIFF_1: 23

        .= ((( arctan . x) * r) + ((f . x) * (1 / (1 + (x ^2 ))))) by A8, A9, Th75

        .= ((r * ( arctan . x)) + (((r * x) + s) / (1 + (x ^2 )))) by A3, A7;

        hence thesis;

      end;

      hence thesis by A1, A5, A6, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:98

    Z c= ( dom (f (#) arccot )) & Z c= ].( - 1), 1.[ & (for x st x in Z holds (f . x) = ((r * x) + s)) implies (f (#) arccot ) is_differentiable_on Z & for x st x in Z holds (((f (#) arccot ) `| Z) . x) = ((r * ( arccot . x)) - (((r * x) + s) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom (f (#) arccot )) and

       A2: Z c= ].( - 1), 1.[ and

       A3: for x st x in Z holds (f . x) = ((r * x) + s);

      Z c= (( dom f) /\ ( dom arccot )) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom f) by XBOOLE_1: 18;

      then

       A5: f is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: arccot is_differentiable_on Z by A2, Th82;

      for x st x in Z holds (((f (#) arccot ) `| Z) . x) = ((r * ( arccot . x)) - (((r * x) + s) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( - 1) < x by A2, XXREAL_1: 4;

        

         A9: x < 1 by A2, A7, XXREAL_1: 4;

        (((f (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff (f,x))) + ((f . x) * ( diff ( arccot ,x)))) by A1, A5, A6, A7, FDIFF_1: 21

        .= ((( arccot . x) * ((f `| Z) . x)) + ((f . x) * ( diff ( arccot ,x)))) by A5, A7, FDIFF_1:def 7

        .= ((( arccot . x) * r) + ((f . x) * ( diff ( arccot ,x)))) by A3, A4, A7, FDIFF_1: 23

        .= ((( arccot . x) * r) + ((f . x) * ( - (1 / (1 + (x ^2 )))))) by A8, A9, Th76

        .= ((( arccot . x) * r) - ((f . x) * (1 / (1 + (x ^2 )))))

        .= ((r * ( arccot . x)) - (((r * x) + s) / (1 + (x ^2 )))) by A3, A7;

        hence thesis;

      end;

      hence thesis by A1, A5, A6, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:99

    Z c= ( dom ((1 / 2) (#) ( arctan * f))) & (for x st x in Z holds (f . x) = (2 * x) & (f . x) > ( - 1) & (f . x) < 1) implies ((1 / 2) (#) ( arctan * f)) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) ( arctan * f)) `| Z) . x) = (1 / (1 + ((2 * x) ^2 )))

    proof

      assume that

       A1: Z c= ( dom ((1 / 2) (#) ( arctan * f))) and

       A2: for x st x in Z holds (f . x) = (2 * x) & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: for x st x in Z holds (f . x) = ((2 * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A2;

      

       A4: Z c= ( dom ( arctan * f)) by A1, VALUED_1:def 5;

      then

       A5: ( arctan * f) is_differentiable_on Z by A3, Th87;

      for x st x in Z holds ((((1 / 2) (#) ( arctan * f)) `| Z) . x) = (1 / (1 + ((2 * x) ^2 )))

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((((1 / 2) (#) ( arctan * f)) `| Z) . x) = ((1 / 2) * ( diff (( arctan * f),x))) by A1, A5, FDIFF_1: 20

        .= ((1 / 2) * ((( arctan * f) `| Z) . x)) by A5, A6, FDIFF_1:def 7

        .= ((1 / 2) * (2 / (1 + (((2 * x) + 0 ) ^2 )))) by A4, A3, A6, Th87

        .= (1 / (1 + ((2 * x) ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 20;

    end;

    theorem :: SIN_COS9:100

    Z c= ( dom ((1 / 2) (#) ( arccot * f))) & (for x st x in Z holds (f . x) = (2 * x) & (f . x) > ( - 1) & (f . x) < 1) implies ((1 / 2) (#) ( arccot * f)) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) ( arccot * f)) `| Z) . x) = ( - (1 / (1 + ((2 * x) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ((1 / 2) (#) ( arccot * f))) and

       A2: for x st x in Z holds (f . x) = (2 * x) & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: for x st x in Z holds (f . x) = ((2 * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A2;

      

       A4: Z c= ( dom ( arccot * f)) by A1, VALUED_1:def 5;

      then

       A5: ( arccot * f) is_differentiable_on Z by A3, Th88;

      for x st x in Z holds ((((1 / 2) (#) ( arccot * f)) `| Z) . x) = ( - (1 / (1 + ((2 * x) ^2 ))))

      proof

        let x;

        assume

         A6: x in Z;

        

        then ((((1 / 2) (#) ( arccot * f)) `| Z) . x) = ((1 / 2) * ( diff (( arccot * f),x))) by A1, A5, FDIFF_1: 20

        .= ((1 / 2) * ((( arccot * f) `| Z) . x)) by A5, A6, FDIFF_1:def 7

        .= ((1 / 2) * ( - (2 / (1 + (((2 * x) + 0 ) ^2 ))))) by A4, A3, A6, Th88

        .= ( - (1 / (1 + ((2 * x) ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 20;

    end;

    theorem :: SIN_COS9:101

    

     Th101: Z c= ( dom (f1 + f2)) & (for x st x in Z holds (f1 . x) = 1) & f2 = ( #Z 2) implies (f1 + f2) is_differentiable_on Z & for x st x in Z holds (((f1 + f2) `| Z) . x) = (2 * x)

    proof

      assume that

       A1: Z c= ( dom (f1 + f2)) and

       A2: for x st x in Z holds (f1 . x) = 1 and

       A3: f2 = ( #Z 2);

      

       A4: for x st x in Z holds f2 is_differentiable_in x by A3, TAYLOR_1: 2;

      

       A5: Z c= (( dom f1) /\ ( dom f2)) by A1, VALUED_1:def 1;

      then

       A6: Z c= ( dom f1) by XBOOLE_1: 18;

      

       A7: for x st x in Z holds (f1 . x) = (( 0 * x) + 1) by A2;

      then

       A8: f1 is_differentiable_on Z by A6, FDIFF_1: 23;

      Z c= ( dom f2) by A5, XBOOLE_1: 18;

      then

       A9: f2 is_differentiable_on Z by A4, FDIFF_1: 9;

      

       A10: for x st x in Z holds ((f2 `| Z) . x) = (2 * x)

      proof

        let x;

        (2 * (x #Z (2 - 1))) = (2 * x) by PREPOWER: 35;

        then

         A11: ( diff (f2,x)) = (2 * x) by A3, TAYLOR_1: 2;

        assume x in Z;

        hence thesis by A9, A11, FDIFF_1:def 7;

      end;

      for x st x in Z holds (((f1 + f2) `| Z) . x) = (2 * x)

      proof

        let x;

        assume

         A12: x in Z;

        

        then (((f1 + f2) `| Z) . x) = (( diff (f1,x)) + ( diff (f2,x))) by A1, A8, A9, FDIFF_1: 18

        .= (((f1 `| Z) . x) + ( diff (f2,x))) by A8, A12, FDIFF_1:def 7

        .= (((f1 `| Z) . x) + ((f2 `| Z) . x)) by A9, A12, FDIFF_1:def 7

        .= ( 0 + ((f2 `| Z) . x)) by A6, A7, A12, FDIFF_1: 23

        .= (2 * x) by A10, A12;

        hence thesis;

      end;

      hence thesis by A1, A8, A9, FDIFF_1: 18;

    end;

    theorem :: SIN_COS9:102

    

     Th102: Z c= ( dom ((1 / 2) (#) ( ln * (f1 + f2)))) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = 1) implies ((1 / 2) (#) ( ln * (f1 + f2))) is_differentiable_on Z & for x st x in Z holds ((((1 / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = (x / (1 + (x ^2 )))

    proof

      assume that

       A1: Z c= ( dom ((1 / 2) (#) ( ln * (f1 + f2)))) and

       A2: f2 = ( #Z 2) and

       A3: for x st x in Z holds (f1 . x) = 1;

      

       A4: Z c= ( dom ( ln * (f1 + f2))) by A1, VALUED_1:def 5;

      then for y be object st y in Z holds y in ( dom (f1 + f2)) by FUNCT_1: 11;

      then

       A5: Z c= ( dom (f1 + f2));

      then

       A6: (f1 + f2) is_differentiable_on Z by A2, A3, Th101;

      for x st x in Z holds ( ln * (f1 + f2)) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by A5, VALUED_1:def 1

        .= (1 + (f2 . x)) by A3, A7

        .= (1 + (x #Z (1 + 1))) by A2, TAYLOR_1:def 1

        .= (1 + ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= (1 + (x * (x #Z 1))) by PREPOWER: 35

        .= (1 + (x * x)) by PREPOWER: 35;

        then

         A8: ((f1 + f2) . x) > 0 by XREAL_1: 34, XREAL_1: 63;

        (f1 + f2) is_differentiable_in x by A6, A7, FDIFF_1: 9;

        hence thesis by A8, TAYLOR_1: 20;

      end;

      then

       A9: ( ln * (f1 + f2)) is_differentiable_on Z by A4, FDIFF_1: 9;

      for x st x in Z holds ((((1 / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = (x / (1 + (x ^2 )))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: (f1 + f2) is_differentiable_in x by A6, FDIFF_1: 9;

        

         A12: ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by A5, A10, VALUED_1:def 1

        .= (1 + (f2 . x)) by A3, A10

        .= (1 + (x #Z (1 + 1))) by A2, TAYLOR_1:def 1

        .= (1 + ((x #Z 1) * (x #Z 1))) by TAYLOR_1: 1

        .= (1 + (x * (x #Z 1))) by PREPOWER: 35

        .= (1 + (x * x)) by PREPOWER: 35;

        then ((f1 + f2) . x) > 0 by XREAL_1: 34, XREAL_1: 63;

        

        then ( diff (( ln * (f1 + f2)),x)) = (( diff ((f1 + f2),x)) / ((f1 + f2) . x)) by A11, TAYLOR_1: 20

        .= ((((f1 + f2) `| Z) . x) / ((f1 + f2) . x)) by A6, A10, FDIFF_1:def 7

        .= ((2 * x) / (1 + (x ^2 ))) by A2, A3, A5, A10, A12, Th101;

        

        hence ((((1 / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = ((1 / 2) * ((2 * x) / (1 + (x ^2 )))) by A1, A9, A10, FDIFF_1: 20

        .= (x / (1 + (x ^2 )));

      end;

      hence thesis by A1, A9, FDIFF_1: 20;

    end;

    theorem :: SIN_COS9:103

    Z c= ( dom ((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2))))) & Z c= ].( - 1), 1.[ & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = 1) implies ((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) is_differentiable_on Z & for x st x in Z holds ((((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arctan . x)

    proof

      assume that

       A1: Z c= ( dom ((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2))))) and

       A2: Z c= ].( - 1), 1.[ and

       A3: f2 = ( #Z 2) and

       A4: for x st x in Z holds (f1 . x) = 1;

      Z c= (( dom (( id Z) (#) arctan )) /\ ( dom ((1 / 2) (#) ( ln * (f1 + f2))))) by A1, VALUED_1: 12;

      then

       A5: Z c= ( dom ((1 / 2) (#) ( ln * (f1 + f2)))) by XBOOLE_1: 18;

      then

       A6: ((1 / 2) (#) ( ln * (f1 + f2))) is_differentiable_on Z by A3, A4, Th102;

      

       A7: (( id Z) (#) arctan ) is_differentiable_on Z by A2, Th95;

      for x st x in Z holds ((((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arctan . x)

      proof

        let x;

        assume

         A8: x in Z;

        

        hence ((((( id Z) (#) arctan ) - ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = (( diff ((( id Z) (#) arctan ),x)) - ( diff (((1 / 2) (#) ( ln * (f1 + f2))),x))) by A1, A7, A6, FDIFF_1: 19

        .= ((((( id Z) (#) arctan ) `| Z) . x) - ( diff (((1 / 2) (#) ( ln * (f1 + f2))),x))) by A7, A8, FDIFF_1:def 7

        .= ((((( id Z) (#) arctan ) `| Z) . x) - ((((1 / 2) (#) ( ln * (f1 + f2))) `| Z) . x)) by A6, A8, FDIFF_1:def 7

        .= ((( arctan . x) + (x / (1 + (x ^2 )))) - ((((1 / 2) (#) ( ln * (f1 + f2))) `| Z) . x)) by A2, A8, Th95

        .= ((( arctan . x) + (x / (1 + (x ^2 )))) - (x / (1 + (x ^2 )))) by A3, A4, A5, A8, Th102

        .= ( arctan . x);

      end;

      hence thesis by A1, A7, A6, FDIFF_1: 19;

    end;

    theorem :: SIN_COS9:104

    Z c= ( dom ((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2))))) & Z c= ].( - 1), 1.[ & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = 1) implies ((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) is_differentiable_on Z & for x st x in Z holds ((((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arccot . x)

    proof

      assume that

       A1: Z c= ( dom ((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2))))) and

       A2: Z c= ].( - 1), 1.[ and

       A3: f2 = ( #Z 2) and

       A4: for x st x in Z holds (f1 . x) = 1;

      Z c= (( dom (( id Z) (#) arccot )) /\ ( dom ((1 / 2) (#) ( ln * (f1 + f2))))) by A1, VALUED_1:def 1;

      then

       A5: Z c= ( dom ((1 / 2) (#) ( ln * (f1 + f2)))) by XBOOLE_1: 18;

      then

       A6: ((1 / 2) (#) ( ln * (f1 + f2))) is_differentiable_on Z by A3, A4, Th102;

      

       A7: (( id Z) (#) arccot ) is_differentiable_on Z by A2, Th96;

      for x st x in Z holds ((((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arccot . x)

      proof

        let x;

        assume

         A8: x in Z;

        

        hence ((((( id Z) (#) arccot ) + ((1 / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = (( diff ((( id Z) (#) arccot ),x)) + ( diff (((1 / 2) (#) ( ln * (f1 + f2))),x))) by A1, A7, A6, FDIFF_1: 18

        .= ((((( id Z) (#) arccot ) `| Z) . x) + ( diff (((1 / 2) (#) ( ln * (f1 + f2))),x))) by A7, A8, FDIFF_1:def 7

        .= ((((( id Z) (#) arccot ) `| Z) . x) + ((((1 / 2) (#) ( ln * (f1 + f2))) `| Z) . x)) by A6, A8, FDIFF_1:def 7

        .= ((( arccot . x) - (x / (1 + (x ^2 )))) + ((((1 / 2) (#) ( ln * (f1 + f2))) `| Z) . x)) by A2, A8, Th96

        .= ((( arccot . x) - (x / (1 + (x ^2 )))) + (x / (1 + (x ^2 )))) by A3, A4, A5, A8, Th102

        .= ( arccot . x);

      end;

      hence thesis by A1, A7, A6, FDIFF_1: 18;

    end;

    theorem :: SIN_COS9:105

    

     Th105: Z c= ( dom (( id Z) (#) ( arctan * f))) & (for x st x in Z holds (f . x) = (x / r) & (f . x) > ( - 1) & (f . x) < 1) implies (( id Z) (#) ( arctan * f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) ( arctan * f)) `| Z) . x) = (( arctan . (x / r)) + (x / (r * (1 + ((x / r) ^2 )))))

    proof

      assume that

       A1: Z c= ( dom (( id Z) (#) ( arctan * f))) and

       A2: for x st x in Z holds (f . x) = (x / r) & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: Z c= (( dom ( id Z)) /\ ( dom ( arctan * f))) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom ( id Z)) by XBOOLE_1: 18;

      

       A5: Z c= ( dom ( arctan * f)) by A3, XBOOLE_1: 18;

      for x st x in Z holds (f . x) = (((1 / r) * x) + 0 )

      proof

        let x;

        assume x in Z;

        then (f . x) = (x / r) by A2;

        hence thesis;

      end;

      then

       A6: for x st x in Z holds (f . x) = (((1 / r) * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A2;

      then

       A7: ( arctan * f) is_differentiable_on Z by A5, Th87;

      

       A8: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      then

       A9: ( id Z) is_differentiable_on Z by A4, FDIFF_1: 23;

      

       A10: for x st x in Z holds ((( arctan * f) `| Z) . x) = (1 / (r * (1 + ((x / r) ^2 ))))

      proof

        let x;

        assume x in Z;

        

        then ((( arctan * f) `| Z) . x) = ((1 / r) / (1 + ((((1 / r) * x) + 0 ) ^2 ))) by A6, A5, Th87

        .= (1 / (r * (1 + ((x / r) ^2 )))) by XCMPLX_1: 78;

        hence thesis;

      end;

      for x st x in Z holds (((( id Z) (#) ( arctan * f)) `| Z) . x) = (( arctan . (x / r)) + (x / (r * (1 + ((x / r) ^2 )))))

      proof

        let x;

        assume

         A11: x in Z;

        

        then

         A12: (( arctan * f) . x) = ( arctan . (f . x)) by A5, FUNCT_1: 12

        .= ( arctan . (x / r)) by A2, A11;

        (((( id Z) (#) ( arctan * f)) `| Z) . x) = (((( arctan * f) . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff (( arctan * f),x)))) by A1, A9, A7, A11, FDIFF_1: 21

        .= (((( arctan * f) . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff (( arctan * f),x)))) by A9, A11, FDIFF_1:def 7

        .= (((( arctan * f) . x) * 1) + ((( id Z) . x) * ( diff (( arctan * f),x)))) by A4, A8, A11, FDIFF_1: 23

        .= (((( arctan * f) . x) * 1) + ((( id Z) . x) * ((( arctan * f) `| Z) . x))) by A7, A11, FDIFF_1:def 7

        .= ((( arctan * f) . x) + (x * ((( arctan * f) `| Z) . x))) by A11, FUNCT_1: 18

        .= (( arctan . (x / r)) + (x * (1 / (r * (1 + ((x / r) ^2 )))))) by A10, A11, A12

        .= (( arctan . (x / r)) + (x / (r * (1 + ((x / r) ^2 )))));

        hence thesis;

      end;

      hence thesis by A1, A9, A7, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:106

    

     Th106: Z c= ( dom (( id Z) (#) ( arccot * f))) & (for x st x in Z holds (f . x) = (x / r) & (f . x) > ( - 1) & (f . x) < 1) implies (( id Z) (#) ( arccot * f)) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) ( arccot * f)) `| Z) . x) = (( arccot . (x / r)) - (x / (r * (1 + ((x / r) ^2 )))))

    proof

      assume that

       A1: Z c= ( dom (( id Z) (#) ( arccot * f))) and

       A2: for x st x in Z holds (f . x) = (x / r) & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: Z c= (( dom ( id Z)) /\ ( dom ( arccot * f))) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom ( id Z)) by XBOOLE_1: 18;

      

       A5: Z c= ( dom ( arccot * f)) by A3, XBOOLE_1: 18;

      for x st x in Z holds (f . x) = (((1 / r) * x) + 0 )

      proof

        let x;

        assume x in Z;

        then (f . x) = (x / r) by A2;

        hence thesis;

      end;

      then

       A6: for x st x in Z holds (f . x) = (((1 / r) * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A2;

      then

       A7: ( arccot * f) is_differentiable_on Z by A5, Th88;

      

       A8: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      then

       A9: ( id Z) is_differentiable_on Z by A4, FDIFF_1: 23;

      

       A10: for x st x in Z holds ((( arccot * f) `| Z) . x) = ( - (1 / (r * (1 + ((x / r) ^2 )))))

      proof

        let x;

        assume x in Z;

        

        then ((( arccot * f) `| Z) . x) = ( - ((1 / r) / (1 + ((((1 / r) * x) + 0 ) ^2 )))) by A6, A5, Th88

        .= ( - (1 / (r * (1 + ((x / r) ^2 ))))) by XCMPLX_1: 78;

        hence thesis;

      end;

      for x st x in Z holds (((( id Z) (#) ( arccot * f)) `| Z) . x) = (( arccot . (x / r)) - (x / (r * (1 + ((x / r) ^2 )))))

      proof

        let x;

        assume

         A11: x in Z;

        

        then

         A12: (( arccot * f) . x) = ( arccot . (f . x)) by A5, FUNCT_1: 12

        .= ( arccot . (x / r)) by A2, A11;

        (((( id Z) (#) ( arccot * f)) `| Z) . x) = (((( arccot * f) . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff (( arccot * f),x)))) by A1, A9, A7, A11, FDIFF_1: 21

        .= (((( arccot * f) . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff (( arccot * f),x)))) by A9, A11, FDIFF_1:def 7

        .= (((( arccot * f) . x) * 1) + ((( id Z) . x) * ( diff (( arccot * f),x)))) by A4, A8, A11, FDIFF_1: 23

        .= (((( arccot * f) . x) * 1) + ((( id Z) . x) * ((( arccot * f) `| Z) . x))) by A7, A11, FDIFF_1:def 7

        .= ((( arccot * f) . x) + (x * ((( arccot * f) `| Z) . x))) by A11, FUNCT_1: 18

        .= (( arccot . (x / r)) + (x * ( - (1 / (r * (1 + ((x / r) ^2 ))))))) by A10, A11, A12

        .= (( arccot . (x / r)) - (x / (r * (1 + ((x / r) ^2 )))));

        hence thesis;

      end;

      hence thesis by A1, A9, A7, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:107

    

     Th107: Z c= ( dom (f1 + f2)) & (for x st x in Z holds (f1 . x) = 1) & f2 = (( #Z 2) * f) & (for x st x in Z holds (f . x) = (x / r)) implies (f1 + f2) is_differentiable_on Z & for x st x in Z holds (((f1 + f2) `| Z) . x) = ((2 * x) / (r ^2 ))

    proof

      assume that

       A1: Z c= ( dom (f1 + f2)) and

       A2: for x st x in Z holds (f1 . x) = 1 and

       A3: f2 = (( #Z 2) * f) and

       A4: for x st x in Z holds (f . x) = (x / r);

      

       A5: for x st x in Z holds (f1 . x) = (( 0 * x) + 1) by A2;

      

       A6: Z c= (( dom f1) /\ ( dom f2)) by A1, VALUED_1:def 1;

      then

       A7: Z c= ( dom f1) by XBOOLE_1: 18;

      then

       A8: f1 is_differentiable_on Z by A5, FDIFF_1: 23;

      

       A9: for x st x in Z holds (f . x) = (((1 / r) * x) + 0 )

      proof

        let x;

        assume x in Z;

        

        hence (f . x) = (x / r) by A4

        .= (((1 / r) * x) + 0 );

      end;

      

       A10: for x st x in Z holds f2 is_differentiable_in x

      proof

        let x;

        Z c= ( dom (( #Z 2) * f)) by A3, A6, XBOOLE_1: 18;

        then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

        then Z c= ( dom f);

        then

         A11: f is_differentiable_on Z by A9, FDIFF_1: 23;

        assume x in Z;

        then f is_differentiable_in x by A11, FDIFF_1: 9;

        hence thesis by A3, TAYLOR_1: 3;

      end;

      Z c= ( dom f2) by A6, XBOOLE_1: 18;

      then

       A12: f2 is_differentiable_on Z by A10, FDIFF_1: 9;

      

       A13: for x st x in Z holds ((f2 `| Z) . x) = ((2 * x) / (r ^2 ))

      proof

        let x;

        assume

         A14: x in Z;

        Z c= ( dom (( #Z 2) * f)) by A3, A6, XBOOLE_1: 18;

        then for y be object st y in Z holds y in ( dom f) by FUNCT_1: 11;

        then

         A15: Z c= ( dom f);

        then

         A16: f is_differentiable_on Z by A9, FDIFF_1: 23;

        then

         A17: f is_differentiable_in x by A14, FDIFF_1: 9;

        ((f2 `| Z) . x) = ( diff ((( #Z 2) * f),x)) by A3, A12, A14, FDIFF_1:def 7

        .= ((2 * ((f . x) #Z (2 - 1))) * ( diff (f,x))) by A17, TAYLOR_1: 3

        .= ((2 * (f . x)) * ( diff (f,x))) by PREPOWER: 35

        .= ((2 * (x / r)) * ( diff (f,x))) by A4, A14

        .= ((2 * (x / r)) * ((f `| Z) . x)) by A14, A16, FDIFF_1:def 7

        .= ((2 * (x / r)) * (1 / r)) by A9, A14, A15, FDIFF_1: 23

        .= (2 * ((x / r) * (1 / r)))

        .= (2 * ((x * 1) / (r * r))) by XCMPLX_1: 76

        .= ((2 * x) / (r ^2 ));

        hence thesis;

      end;

      for x st x in Z holds (((f1 + f2) `| Z) . x) = ((2 * x) / (r ^2 ))

      proof

        let x;

        assume

         A18: x in Z;

        

        then (((f1 + f2) `| Z) . x) = (( diff (f1,x)) + ( diff (f2,x))) by A1, A8, A12, FDIFF_1: 18

        .= (((f1 `| Z) . x) + ( diff (f2,x))) by A8, A18, FDIFF_1:def 7

        .= (((f1 `| Z) . x) + ((f2 `| Z) . x)) by A12, A18, FDIFF_1:def 7

        .= ( 0 + ((f2 `| Z) . x)) by A7, A5, A18, FDIFF_1: 23

        .= ((2 * x) / (r ^2 )) by A13, A18;

        hence thesis;

      end;

      hence thesis by A1, A8, A12, FDIFF_1: 18;

    end;

    theorem :: SIN_COS9:108

    

     Th108: Z c= ( dom ((r / 2) (#) ( ln * (f1 + f2)))) & (for x st x in Z holds (f1 . x) = 1) & r <> 0 & f2 = (( #Z 2) * f) & (for x st x in Z holds (f . x) = (x / r)) implies ((r / 2) (#) ( ln * (f1 + f2))) is_differentiable_on Z & for x st x in Z holds ((((r / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = (x / (r * (1 + ((x / r) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ((r / 2) (#) ( ln * (f1 + f2)))) and

       A2: for x st x in Z holds (f1 . x) = 1 and

       A3: r <> 0 and

       A4: f2 = (( #Z 2) * f) and

       A5: for x st x in Z holds (f . x) = (x / r);

      

       A6: Z c= ( dom ( ln * (f1 + f2))) by A1, VALUED_1:def 5;

      then for y be object st y in Z holds y in ( dom (f1 + f2)) by FUNCT_1: 11;

      then

       A7: Z c= ( dom (f1 + f2));

      then

       A8: (f1 + f2) is_differentiable_on Z by A2, A4, A5, Th107;

      ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

      then

       A9: Z c= ( dom f2) by A7, XBOOLE_1: 18;

      for x st x in Z holds ( ln * (f1 + f2)) is_differentiable_in x

      proof

        let x;

        set g = ( #Z 2);

        assume

         A10: x in Z;

        

        then ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by A7, VALUED_1:def 1

        .= (1 + ((g * f) . x)) by A2, A4, A10

        .= (1 + (g . (f . x))) by A4, A9, A10, FUNCT_1: 12

        .= (1 + (g . (x / r))) by A5, A10

        .= (1 + ((x / r) #Z (1 + 1))) by TAYLOR_1:def 1

        .= (1 + (((x / r) #Z 1) * ((x / r) #Z 1))) by TAYLOR_1: 1

        .= (1 + ((x / r) * ((x / r) #Z 1))) by PREPOWER: 35

        .= (1 + ((x / r) * (x / r))) by PREPOWER: 35;

        then

         A11: ((f1 + f2) . x) > 0 by XREAL_1: 34, XREAL_1: 63;

        (f1 + f2) is_differentiable_in x by A8, A10, FDIFF_1: 9;

        hence thesis by A11, TAYLOR_1: 20;

      end;

      then

       A12: ( ln * (f1 + f2)) is_differentiable_on Z by A6, FDIFF_1: 9;

      for x st x in Z holds ((((r / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = (x / (r * (1 + ((x / r) ^2 ))))

      proof

        let x;

        set g = ( #Z 2);

        assume

         A13: x in Z;

        then

         A14: (f1 + f2) is_differentiable_in x by A8, FDIFF_1: 9;

        

         A15: ((f1 + f2) . x) = ((f1 . x) + (f2 . x)) by A7, A13, VALUED_1:def 1

        .= (1 + ((g * f) . x)) by A2, A4, A13

        .= (1 + (g . (f . x))) by A4, A9, A13, FUNCT_1: 12

        .= (1 + (g . (x / r))) by A5, A13

        .= (1 + ((x / r) #Z (1 + 1))) by TAYLOR_1:def 1

        .= (1 + (((x / r) #Z 1) * ((x / r) #Z 1))) by TAYLOR_1: 1

        .= (1 + ((x / r) * ((x / r) #Z 1))) by PREPOWER: 35

        .= (1 + ((x / r) * (x / r))) by PREPOWER: 35;

        then ((f1 + f2) . x) > 0 by XREAL_1: 34, XREAL_1: 63;

        

        then

         A16: ( diff (( ln * (f1 + f2)),x)) = (( diff ((f1 + f2),x)) / ((f1 + f2) . x)) by A14, TAYLOR_1: 20

        .= ((((f1 + f2) `| Z) . x) / ((f1 + f2) . x)) by A8, A13, FDIFF_1:def 7

        .= (((2 * x) / (r ^2 )) / (1 + ((x / r) ^2 ))) by A2, A4, A5, A7, A13, A15, Th107;

        

        thus ((((r / 2) (#) ( ln * (f1 + f2))) `| Z) . x) = ((r / 2) * ( diff (( ln * (f1 + f2)),x))) by A1, A12, A13, FDIFF_1: 20

        .= (((r * x) / (r ^2 )) / (1 + ((x / r) ^2 ))) by A16

        .= (((r / r) * (x / r)) / (1 + ((x / r) ^2 ))) by XCMPLX_1: 76

        .= ((1 * (x / r)) / (1 + ((x / r) ^2 ))) by A3, XCMPLX_1: 60

        .= (x / (r * (1 + ((x / r) ^2 )))) by XCMPLX_1: 78;

      end;

      hence thesis by A1, A12, FDIFF_1: 20;

    end;

    theorem :: SIN_COS9:109

    Z c= ( dom ((( id Z) (#) ( arctan * f)) - ((r / 2) (#) ( ln * (f1 + f2))))) & r <> 0 & (for x st x in Z holds (f . x) = (x / r) & (f . x) > ( - 1) & (f . x) < 1) & (for x st x in Z holds (f1 . x) = 1) & f2 = (( #Z 2) * f) & (for x st x in Z holds (f . x) = (x / r)) implies ((( id Z) (#) ( arctan * f)) - ((r / 2) (#) ( ln * (f1 + f2)))) is_differentiable_on Z & for x st x in Z holds ((((( id Z) (#) ( arctan * f)) - ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arctan . (x / r))

    proof

      assume that

       A1: Z c= ( dom ((( id Z) (#) ( arctan * f)) - ((r / 2) (#) ( ln * (f1 + f2))))) and

       A2: r <> 0 and

       A3: for x st x in Z holds (f . x) = (x / r) & (f . x) > ( - 1) & (f . x) < 1 and

       A4: for x st x in Z holds (f1 . x) = 1 and

       A5: f2 = (( #Z 2) * f) and

       A6: for x st x in Z holds (f . x) = (x / r);

      

       A7: Z c= (( dom (( id Z) (#) ( arctan * f))) /\ ( dom ((r / 2) (#) ( ln * (f1 + f2))))) by A1, VALUED_1: 12;

      then

       A8: Z c= ( dom ((r / 2) (#) ( ln * (f1 + f2)))) by XBOOLE_1: 18;

      then

       A9: ((r / 2) (#) ( ln * (f1 + f2))) is_differentiable_on Z by A2, A4, A5, A6, Th108;

      

       A10: Z c= ( dom (( id Z) (#) ( arctan * f))) by A7, XBOOLE_1: 18;

      then

       A11: (( id Z) (#) ( arctan * f)) is_differentiable_on Z by A3, Th105;

      for x st x in Z holds ((((( id Z) (#) ( arctan * f)) - ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arctan . (x / r))

      proof

        let x;

        assume

         A12: x in Z;

        

        hence ((((( id Z) (#) ( arctan * f)) - ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = (( diff ((( id Z) (#) ( arctan * f)),x)) - ( diff (((r / 2) (#) ( ln * (f1 + f2))),x))) by A1, A11, A9, FDIFF_1: 19

        .= ((((( id Z) (#) ( arctan * f)) `| Z) . x) - ( diff (((r / 2) (#) ( ln * (f1 + f2))),x))) by A11, A12, FDIFF_1:def 7

        .= ((((( id Z) (#) ( arctan * f)) `| Z) . x) - ((((r / 2) (#) ( ln * (f1 + f2))) `| Z) . x)) by A9, A12, FDIFF_1:def 7

        .= ((( arctan . (x / r)) + (x / (r * (1 + ((x / r) ^2 ))))) - ((((r / 2) (#) ( ln * (f1 + f2))) `| Z) . x)) by A3, A10, A12, Th105

        .= ((( arctan . (x / r)) + (x / (r * (1 + ((x / r) ^2 ))))) - (x / (r * (1 + ((x / r) ^2 ))))) by A2, A4, A5, A6, A8, A12, Th108

        .= ( arctan . (x / r));

      end;

      hence thesis by A1, A11, A9, FDIFF_1: 19;

    end;

    theorem :: SIN_COS9:110

    Z c= ( dom ((( id Z) (#) ( arccot * f)) + ((r / 2) (#) ( ln * (f1 + f2))))) & r <> 0 & (for x st x in Z holds (f . x) = (x / r) & (f . x) > ( - 1) & (f . x) < 1) & (for x st x in Z holds (f1 . x) = 1) & f2 = (( #Z 2) * f) & (for x st x in Z holds (f . x) = (x / r)) implies ((( id Z) (#) ( arccot * f)) + ((r / 2) (#) ( ln * (f1 + f2)))) is_differentiable_on Z & for x st x in Z holds ((((( id Z) (#) ( arccot * f)) + ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arccot . (x / r))

    proof

      assume that

       A1: Z c= ( dom ((( id Z) (#) ( arccot * f)) + ((r / 2) (#) ( ln * (f1 + f2))))) and

       A2: r <> 0 and

       A3: for x st x in Z holds (f . x) = (x / r) & (f . x) > ( - 1) & (f . x) < 1 and

       A4: for x st x in Z holds (f1 . x) = 1 and

       A5: f2 = (( #Z 2) * f) and

       A6: for x st x in Z holds (f . x) = (x / r);

      

       A7: Z c= (( dom (( id Z) (#) ( arccot * f))) /\ ( dom ((r / 2) (#) ( ln * (f1 + f2))))) by A1, VALUED_1:def 1;

      then

       A8: Z c= ( dom ((r / 2) (#) ( ln * (f1 + f2)))) by XBOOLE_1: 18;

      then

       A9: ((r / 2) (#) ( ln * (f1 + f2))) is_differentiable_on Z by A2, A4, A5, A6, Th108;

      

       A10: Z c= ( dom (( id Z) (#) ( arccot * f))) by A7, XBOOLE_1: 18;

      then

       A11: (( id Z) (#) ( arccot * f)) is_differentiable_on Z by A3, Th106;

      for x st x in Z holds ((((( id Z) (#) ( arccot * f)) + ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = ( arccot . (x / r))

      proof

        let x;

        assume

         A12: x in Z;

        

        hence ((((( id Z) (#) ( arccot * f)) + ((r / 2) (#) ( ln * (f1 + f2)))) `| Z) . x) = (( diff ((( id Z) (#) ( arccot * f)),x)) + ( diff (((r / 2) (#) ( ln * (f1 + f2))),x))) by A1, A11, A9, FDIFF_1: 18

        .= ((((( id Z) (#) ( arccot * f)) `| Z) . x) + ( diff (((r / 2) (#) ( ln * (f1 + f2))),x))) by A11, A12, FDIFF_1:def 7

        .= ((((( id Z) (#) ( arccot * f)) `| Z) . x) + ((((r / 2) (#) ( ln * (f1 + f2))) `| Z) . x)) by A9, A12, FDIFF_1:def 7

        .= ((( arccot . (x / r)) - (x / (r * (1 + ((x / r) ^2 ))))) + ((((r / 2) (#) ( ln * (f1 + f2))) `| Z) . x)) by A3, A10, A12, Th106

        .= ((( arccot . (x / r)) - (x / (r * (1 + ((x / r) ^2 ))))) + (x / (r * (1 + ((x / r) ^2 ))))) by A2, A4, A5, A6, A8, A12, Th108

        .= ( arccot . (x / r));

      end;

      hence thesis by A1, A11, A9, FDIFF_1: 18;

    end;

    theorem :: SIN_COS9:111

     not 0 in Z & Z c= ( dom ( arctan * (( id Z) ^ ))) & (for x st x in Z holds ((( id Z) ^ ) . x) > ( - 1) & ((( id Z) ^ ) . x) < 1) implies ( arctan * (( id Z) ^ )) is_differentiable_on Z & for x st x in Z holds ((( arctan * (( id Z) ^ )) `| Z) . x) = ( - (1 / (1 + (x ^2 ))))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ( arctan * (( id Z) ^ ))) and

       A3: for x st x in Z holds ((( id Z) ^ ) . x) > ( - 1) & ((( id Z) ^ ) . x) < 1;

      ( dom ( arctan * (f ^ ))) c= ( dom (f ^ )) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f ^ )) by A2;

      

       A5: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

       A6: for x st x in Z holds ( arctan * (f ^ )) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ((f ^ ) . x) > ( - 1) by A3;

        

         A9: ((f ^ ) . x) < 1 by A3, A7;

        (f ^ ) is_differentiable_in x by A5, A7, FDIFF_1: 9;

        hence thesis by A8, A9, Th85;

      end;

      then

       A10: ( arctan * (f ^ )) is_differentiable_on Z by A2, FDIFF_1: 9;

      for x st x in Z holds ((( arctan * (f ^ )) `| Z) . x) = ( - (1 / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: (f ^ ) is_differentiable_in x by A5, FDIFF_1: 9;

        

         A13: ((f ^ ) . x) < 1 by A3, A11;

        

         A14: ((f ^ ) . x) > ( - 1) by A3, A11;

        (f . x) = x by A11, FUNCT_1: 18;

        then x <> 0 by A4, A11, RFUNCT_1: 3;

        then

         A15: (x ^2 ) <> 0 ;

        ((( arctan * (f ^ )) `| Z) . x) = ( diff (( arctan * (f ^ )),x)) by A10, A11, FDIFF_1:def 7

        .= (( diff ((f ^ ),x)) / (1 + (((f ^ ) . x) ^2 ))) by A12, A14, A13, Th85

        .= ((((f ^ ) `| Z) . x) / (1 + (((f ^ ) . x) ^2 ))) by A5, A11, FDIFF_1:def 7

        .= (( - (1 / (x ^2 ))) / (1 + (((f ^ ) . x) ^2 ))) by A1, A11, FDIFF_5: 4

        .= (( - (1 / (x ^2 ))) / (1 + (((f . x) " ) ^2 ))) by A4, A11, RFUNCT_1:def 2

        .= (( - (1 / (x ^2 ))) / (1 + ((1 / x) ^2 ))) by A11, FUNCT_1: 18

        .= ( - ((1 / (x ^2 )) / (1 + ((1 / x) ^2 ))))

        .= ( - (1 / ((x ^2 ) * (1 + ((1 / x) ^2 ))))) by XCMPLX_1: 78

        .= ( - (1 / (((x ^2 ) * 1) + ((x ^2 ) * ((1 / x) ^2 )))))

        .= ( - (1 / ((x ^2 ) + ((x ^2 ) * (1 / (x * x)))))) by XCMPLX_1: 102

        .= ( - (1 / ((x ^2 ) + (((x ^2 ) * 1) / (x ^2 )))))

        .= ( - (1 / (1 + (x ^2 )))) by A15, XCMPLX_1: 60;

        hence thesis;

      end;

      hence thesis by A2, A6, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:112

     not 0 in Z & Z c= ( dom ( arccot * (( id Z) ^ ))) & (for x st x in Z holds ((( id Z) ^ ) . x) > ( - 1) & ((( id Z) ^ ) . x) < 1) implies ( arccot * (( id Z) ^ )) is_differentiable_on Z & for x st x in Z holds ((( arccot * (( id Z) ^ )) `| Z) . x) = (1 / (1 + (x ^2 )))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ( arccot * (f ^ ))) and

       A3: for x st x in Z holds ((f ^ ) . x) > ( - 1) & ((f ^ ) . x) < 1;

      ( dom ( arccot * (f ^ ))) c= ( dom (f ^ )) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f ^ )) by A2;

      

       A5: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

       A6: for x st x in Z holds ( arccot * (f ^ )) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ((f ^ ) . x) > ( - 1) by A3;

        

         A9: ((f ^ ) . x) < 1 by A3, A7;

        (f ^ ) is_differentiable_in x by A5, A7, FDIFF_1: 9;

        hence thesis by A8, A9, Th86;

      end;

      then

       A10: ( arccot * (f ^ )) is_differentiable_on Z by A2, FDIFF_1: 9;

      for x st x in Z holds ((( arccot * (f ^ )) `| Z) . x) = (1 / (1 + (x ^2 )))

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: (f ^ ) is_differentiable_in x by A5, FDIFF_1: 9;

        

         A13: ((f ^ ) . x) < 1 by A3, A11;

        

         A14: ((f ^ ) . x) > ( - 1) by A3, A11;

        (f . x) = x by A11, FUNCT_1: 18;

        then x <> 0 by A4, A11, RFUNCT_1: 3;

        then

         A15: (x ^2 ) <> 0 ;

        ((( arccot * (f ^ )) `| Z) . x) = ( diff (( arccot * (f ^ )),x)) by A10, A11, FDIFF_1:def 7

        .= ( - (( diff ((f ^ ),x)) / (1 + (((f ^ ) . x) ^2 )))) by A12, A14, A13, Th86

        .= ( - ((((f ^ ) `| Z) . x) / (1 + (((f ^ ) . x) ^2 )))) by A5, A11, FDIFF_1:def 7

        .= ( - (( - (1 / (x ^2 ))) / (1 + (((f ^ ) . x) ^2 )))) by A1, A11, FDIFF_5: 4

        .= ( - (( - (1 / (x ^2 ))) / (1 + (((f . x) " ) ^2 )))) by A4, A11, RFUNCT_1:def 2

        .= ( - (( - (1 / (x ^2 ))) / (1 + ((1 / x) ^2 )))) by A11, FUNCT_1: 18

        .= ((1 / (x ^2 )) / (1 + ((1 / x) ^2 )))

        .= (1 / ((x ^2 ) * (1 + ((1 / x) ^2 )))) by XCMPLX_1: 78

        .= (1 / (((x ^2 ) * 1) + ((x ^2 ) * ((1 / x) ^2 ))))

        .= (1 / ((x ^2 ) + ((x ^2 ) * (1 / (x * x))))) by XCMPLX_1: 102

        .= (1 / ((x ^2 ) + (((x ^2 ) * 1) / (x ^2 ))))

        .= (1 / (1 + (x ^2 ))) by A15, XCMPLX_1: 60;

        hence thesis;

      end;

      hence thesis by A2, A6, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:113

    Z c= ( dom ( arctan * f)) & f = (f1 + (h (#) f2)) & (for x st x in Z holds (f . x) > ( - 1) & (f . x) < 1) & (for x st x in Z holds (f1 . x) = (r + (s * x))) & f2 = ( #Z 2) implies ( arctan * (f1 + (h (#) f2))) is_differentiable_on Z & for x st x in Z holds ((( arctan * (f1 + (h (#) f2))) `| Z) . x) = ((s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2 ))) ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( arctan * f)) and

       A2: f = (f1 + (h (#) f2)) and

       A3: for x st x in Z holds (f . x) > ( - 1) & (f . x) < 1 and

       A4: for x st x in Z holds (f1 . x) = (r + (s * x)) and

       A5: f2 = ( #Z 2);

      ( dom ( arctan * f)) c= ( dom f) by RELAT_1: 25;

      then

       A6: Z c= ( dom (f1 + (h (#) f2))) by A1, A2;

      then Z c= (( dom f1) /\ ( dom (h (#) f2))) by VALUED_1:def 1;

      then

       A7: Z c= ( dom (h (#) f2)) by XBOOLE_1: 18;

      

       A8: (f1 + (h (#) f2)) is_differentiable_on Z by A4, A5, A6, FDIFF_4: 12;

      

       A9: for x st x in Z holds ( arctan * (f1 + (h (#) f2))) is_differentiable_in x

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: (f . x) > ( - 1) by A3;

        

         A12: (f . x) < 1 by A3, A10;

        f is_differentiable_in x by A2, A8, A10, FDIFF_1: 9;

        hence thesis by A2, A11, A12, Th85;

      end;

      then

       A13: ( arctan * (f1 + (h (#) f2))) is_differentiable_on Z by A1, A2, FDIFF_1: 9;

      for x st x in Z holds ((( arctan * (f1 + (h (#) f2))) `| Z) . x) = ((s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2 ))) ^2 )))

      proof

        let x;

        assume

         A14: x in Z;

        

        then

         A15: ((f1 + (h (#) f2)) . x) = ((f1 . x) + ((h (#) f2) . x)) by A6, VALUED_1:def 1

        .= ((f1 . x) + (h * (f2 . x))) by A7, A14, VALUED_1:def 5

        .= ((r + (s * x)) + (h * (f2 . x))) by A4, A14

        .= ((r + (s * x)) + (h * (x #Z (1 + 1)))) by A5, TAYLOR_1:def 1

        .= ((r + (s * x)) + (h * ((x #Z 1) * (x #Z 1)))) by TAYLOR_1: 1

        .= ((r + (s * x)) + (h * (x * (x #Z 1)))) by PREPOWER: 35

        .= ((r + (s * x)) + (h * (x ^2 ))) by PREPOWER: 35;

        

         A16: f is_differentiable_in x by A2, A8, A14, FDIFF_1: 9;

        

         A17: (f . x) > ( - 1) by A3, A14;

        

         A18: (f . x) < 1 by A3, A14;

        ((( arctan * (f1 + (h (#) f2))) `| Z) . x) = ( diff (( arctan * f),x)) by A2, A13, A14, FDIFF_1:def 7

        .= (( diff (f,x)) / (1 + ((f . x) ^2 ))) by A16, A17, A18, Th85

        .= ((((f1 + (h (#) f2)) `| Z) . x) / (1 + ((f . x) ^2 ))) by A2, A8, A14, FDIFF_1:def 7

        .= ((s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2 ))) ^2 ))) by A2, A4, A5, A6, A14, A15, FDIFF_4: 12;

        hence thesis;

      end;

      hence thesis by A1, A2, A9, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:114

    Z c= ( dom ( arccot * f)) & f = (f1 + (h (#) f2)) & (for x st x in Z holds (f . x) > ( - 1) & (f . x) < 1) & (for x st x in Z holds (f1 . x) = (r + (s * x))) & f2 = ( #Z 2) implies ( arccot * (f1 + (h (#) f2))) is_differentiable_on Z & for x st x in Z holds ((( arccot * (f1 + (h (#) f2))) `| Z) . x) = ( - ((s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2 ))) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( arccot * f)) and

       A2: f = (f1 + (h (#) f2)) and

       A3: for x st x in Z holds (f . x) > ( - 1) & (f . x) < 1 and

       A4: for x st x in Z holds (f1 . x) = (r + (s * x)) and

       A5: f2 = ( #Z 2);

      ( dom ( arccot * f)) c= ( dom f) by RELAT_1: 25;

      then

       A6: Z c= ( dom (f1 + (h (#) f2))) by A1, A2;

      then Z c= (( dom f1) /\ ( dom (h (#) f2))) by VALUED_1:def 1;

      then

       A7: Z c= ( dom (h (#) f2)) by XBOOLE_1: 18;

      

       A8: (f1 + (h (#) f2)) is_differentiable_on Z by A4, A5, A6, FDIFF_4: 12;

      

       A9: for x st x in Z holds ( arccot * (f1 + (h (#) f2))) is_differentiable_in x

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: (f . x) > ( - 1) by A3;

        

         A12: (f . x) < 1 by A3, A10;

        f is_differentiable_in x by A2, A8, A10, FDIFF_1: 9;

        hence thesis by A2, A11, A12, Th86;

      end;

      then

       A13: ( arccot * (f1 + (h (#) f2))) is_differentiable_on Z by A1, A2, FDIFF_1: 9;

      for x st x in Z holds ((( arccot * (f1 + (h (#) f2))) `| Z) . x) = ( - ((s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2 ))) ^2 ))))

      proof

        let x;

        assume

         A14: x in Z;

        

        then

         A15: ((f1 + (h (#) f2)) . x) = ((f1 . x) + ((h (#) f2) . x)) by A6, VALUED_1:def 1

        .= ((f1 . x) + (h * (f2 . x))) by A7, A14, VALUED_1:def 5

        .= ((r + (s * x)) + (h * (f2 . x))) by A4, A14

        .= ((r + (s * x)) + (h * (x #Z (1 + 1)))) by A5, TAYLOR_1:def 1

        .= ((r + (s * x)) + (h * ((x #Z 1) * (x #Z 1)))) by TAYLOR_1: 1

        .= ((r + (s * x)) + (h * (x * (x #Z 1)))) by PREPOWER: 35

        .= ((r + (s * x)) + (h * (x ^2 ))) by PREPOWER: 35;

        

         A16: f is_differentiable_in x by A2, A8, A14, FDIFF_1: 9;

        

         A17: (f . x) > ( - 1) by A3, A14;

        

         A18: (f . x) < 1 by A3, A14;

        ((( arccot * (f1 + (h (#) f2))) `| Z) . x) = ( diff (( arccot * f),x)) by A2, A13, A14, FDIFF_1:def 7

        .= ( - (( diff (f,x)) / (1 + ((f . x) ^2 )))) by A16, A17, A18, Th86

        .= ( - ((((f1 + (h (#) f2)) `| Z) . x) / (1 + ((f . x) ^2 )))) by A2, A8, A14, FDIFF_1:def 7

        .= ( - ((s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2 ))) ^2 )))) by A2, A4, A5, A6, A14, A15, FDIFF_4: 12;

        hence thesis;

      end;

      hence thesis by A1, A2, A9, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:115

    Z c= ( dom ( arctan * exp_R )) & (for x st x in Z holds ( exp_R . x) < 1) implies ( arctan * exp_R ) is_differentiable_on Z & for x st x in Z holds ((( arctan * exp_R ) `| Z) . x) = (( exp_R . x) / (1 + (( exp_R . x) ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( arctan * exp_R )) and

       A2: for x st x in Z holds ( exp_R . x) < 1;

      

       A3: for x st x in Z holds ( arctan * exp_R ) is_differentiable_in x

      proof

        let x;

        

         A4: exp_R is_differentiable_in x by SIN_COS: 65;

        assume x in Z;

        then

         A5: ( exp_R . x) < 1 by A2;

        (( exp_R . x) + 0 ) > ( 0 + ( - 1)) by SIN_COS: 54;

        hence thesis by A5, A4, Th85;

      end;

      then

       A6: ( arctan * exp_R ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arctan * exp_R ) `| Z) . x) = (( exp_R . x) / (1 + (( exp_R . x) ^2 )))

      proof

        let x;

        

         A7: (( exp_R . x) + 0 ) > ( 0 + ( - 1)) by SIN_COS: 54;

        

         A8: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A9: x in Z;

        then

         A10: ( exp_R . x) < 1 by A2;

        ((( arctan * exp_R ) `| Z) . x) = ( diff (( arctan * exp_R ),x)) by A6, A9, FDIFF_1:def 7

        .= (( diff ( exp_R ,x)) / (1 + (( exp_R . x) ^2 ))) by A7, A10, A8, Th85

        .= (( exp_R . x) / (1 + (( exp_R . x) ^2 ))) by SIN_COS: 65;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:116

    Z c= ( dom ( arccot * exp_R )) & (for x st x in Z holds ( exp_R . x) < 1) implies ( arccot * exp_R ) is_differentiable_on Z & for x st x in Z holds ((( arccot * exp_R ) `| Z) . x) = ( - (( exp_R . x) / (1 + (( exp_R . x) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( arccot * exp_R )) and

       A2: for x st x in Z holds ( exp_R . x) < 1;

      

       A3: for x st x in Z holds ( arccot * exp_R ) is_differentiable_in x

      proof

        let x;

        

         A4: exp_R is_differentiable_in x by SIN_COS: 65;

        assume x in Z;

        then

         A5: ( exp_R . x) < 1 by A2;

        (( exp_R . x) + 0 ) > ( 0 + ( - 1)) by SIN_COS: 54;

        hence thesis by A5, A4, Th86;

      end;

      then

       A6: ( arccot * exp_R ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( arccot * exp_R ) `| Z) . x) = ( - (( exp_R . x) / (1 + (( exp_R . x) ^2 ))))

      proof

        let x;

        

         A7: (( exp_R . x) + 0 ) > ( 0 + ( - 1)) by SIN_COS: 54;

        

         A8: exp_R is_differentiable_in x by SIN_COS: 65;

        assume

         A9: x in Z;

        then

         A10: ( exp_R . x) < 1 by A2;

        ((( arccot * exp_R ) `| Z) . x) = ( diff (( arccot * exp_R ),x)) by A6, A9, FDIFF_1:def 7

        .= ( - (( diff ( exp_R ,x)) / (1 + (( exp_R . x) ^2 )))) by A7, A10, A8, Th86

        .= ( - (( exp_R . x) / (1 + (( exp_R . x) ^2 )))) by SIN_COS: 65;

        hence thesis;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:117

    Z c= ( dom ( arctan * ln )) & (for x st x in Z holds ( ln . x) > ( - 1) & ( ln . x) < 1) implies ( arctan * ln ) is_differentiable_on Z & for x st x in Z holds ((( arctan * ln ) `| Z) . x) = (1 / (x * (1 + (( ln . x) ^2 ))))

    proof

      

       A1: ( right_open_halfline 0 ) = { g where g be Real : 0 < g } by XXREAL_1: 230;

      assume that

       A2: Z c= ( dom ( arctan * ln )) and

       A3: for x st x in Z holds ( ln . x) > ( - 1) & ( ln . x) < 1;

      ( dom ( arctan * ln )) c= ( dom ln ) by RELAT_1: 25;

      then

       A4: Z c= ( dom ln ) by A2;

      

       A5: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A4, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by A1;

        hence thesis;

      end;

      

       A6: for x st x in Z holds ( arctan * ln ) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( ln . x) > ( - 1) by A3;

        

         A9: ( ln . x) < 1 by A3, A7;

         ln is_differentiable_in x by A5, A7, TAYLOR_1: 18;

        hence thesis by A8, A9, Th85;

      end;

      then

       A10: ( arctan * ln ) is_differentiable_on Z by A2, FDIFF_1: 9;

      for x st x in Z holds ((( arctan * ln ) `| Z) . x) = (1 / (x * (1 + (( ln . x) ^2 ))))

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: ln is_differentiable_in x by A5, TAYLOR_1: 18;

        

         A13: ( ln . x) < 1 by A3, A11;

        

         A14: ( ln . x) > ( - 1) by A3, A11;

        x > 0 by A5, A11;

        then

         A15: x in ( right_open_halfline 0 ) by A1;

        ((( arctan * ln ) `| Z) . x) = ( diff (( arctan * ln ),x)) by A10, A11, FDIFF_1:def 7

        .= (( diff ( ln ,x)) / (1 + (( ln . x) ^2 ))) by A12, A14, A13, Th85

        .= ((1 / x) / (1 + (( ln . x) ^2 ))) by A15, TAYLOR_1: 18

        .= (1 / (x * (1 + (( ln . x) ^2 )))) by XCMPLX_1: 78;

        hence thesis;

      end;

      hence thesis by A2, A6, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:118

    Z c= ( dom ( arccot * ln )) & (for x st x in Z holds ( ln . x) > ( - 1) & ( ln . x) < 1) implies ( arccot * ln ) is_differentiable_on Z & for x st x in Z holds ((( arccot * ln ) `| Z) . x) = ( - (1 / (x * (1 + (( ln . x) ^2 )))))

    proof

      

       A1: ( right_open_halfline 0 ) = { g where g be Real : 0 < g } by XXREAL_1: 230;

      assume that

       A2: Z c= ( dom ( arccot * ln )) and

       A3: for x st x in Z holds ( ln . x) > ( - 1) & ( ln . x) < 1;

      ( dom ( arccot * ln )) c= ( dom ln ) by RELAT_1: 25;

      then

       A4: Z c= ( dom ln ) by A2;

      

       A5: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A4, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by A1;

        hence thesis;

      end;

      

       A6: for x st x in Z holds ( arccot * ln ) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( ln . x) > ( - 1) by A3;

        

         A9: ( ln . x) < 1 by A3, A7;

         ln is_differentiable_in x by A5, A7, TAYLOR_1: 18;

        hence thesis by A8, A9, Th86;

      end;

      then

       A10: ( arccot * ln ) is_differentiable_on Z by A2, FDIFF_1: 9;

      for x st x in Z holds ((( arccot * ln ) `| Z) . x) = ( - (1 / (x * (1 + (( ln . x) ^2 )))))

      proof

        let x;

        assume

         A11: x in Z;

        then

         A12: ln is_differentiable_in x by A5, TAYLOR_1: 18;

        

         A13: ( ln . x) < 1 by A3, A11;

        

         A14: ( ln . x) > ( - 1) by A3, A11;

        x > 0 by A5, A11;

        then

         A15: x in ( right_open_halfline 0 ) by A1;

        ((( arccot * ln ) `| Z) . x) = ( diff (( arccot * ln ),x)) by A10, A11, FDIFF_1:def 7

        .= ( - (( diff ( ln ,x)) / (1 + (( ln . x) ^2 )))) by A12, A14, A13, Th86

        .= ( - ((1 / x) / (1 + (( ln . x) ^2 )))) by A15, TAYLOR_1: 18

        .= ( - (1 / (x * (1 + (( ln . x) ^2 ))))) by XCMPLX_1: 78;

        hence thesis;

      end;

      hence thesis by A2, A6, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:119

    Z c= ( dom ( exp_R * arctan )) & Z c= ].( - 1), 1.[ implies ( exp_R * arctan ) is_differentiable_on Z & for x st x in Z holds ((( exp_R * arctan ) `| Z) . x) = (( exp_R . ( arctan . x)) / (1 + (x ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( exp_R * arctan )) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: for x st x in Z holds ( exp_R * arctan ) is_differentiable_in x

      proof

        let x;

        assume

         A4: x in Z;

         arctan is_differentiable_on Z by A2, Th81;

        then

         A5: arctan is_differentiable_in x by A4, FDIFF_1: 9;

         exp_R is_differentiable_in ( arctan . x) by SIN_COS: 65;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( exp_R * arctan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R * arctan ) `| Z) . x) = (( exp_R . ( arctan . x)) / (1 + (x ^2 )))

      proof

        let x;

        assume

         A7: x in Z;

        

         A8: exp_R is_differentiable_in ( arctan . x) by SIN_COS: 65;

        

         A9: arctan is_differentiable_on Z by A2, Th81;

        then arctan is_differentiable_in x by A7, FDIFF_1: 9;

        

        then ( diff (( exp_R * arctan ),x)) = (( diff ( exp_R ,( arctan . x))) * ( diff ( arctan ,x))) by A8, FDIFF_2: 13

        .= (( diff ( exp_R ,( arctan . x))) * (( arctan `| Z) . x)) by A7, A9, FDIFF_1:def 7

        .= (( diff ( exp_R ,( arctan . x))) * (1 / (1 + (x ^2 )))) by A2, A7, Th81

        .= (( exp_R . ( arctan . x)) / (1 + (x ^2 ))) by SIN_COS: 65;

        hence thesis by A6, A7, FDIFF_1:def 7;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:120

    Z c= ( dom ( exp_R * arccot )) & Z c= ].( - 1), 1.[ implies ( exp_R * arccot ) is_differentiable_on Z & for x st x in Z holds ((( exp_R * arccot ) `| Z) . x) = ( - (( exp_R . ( arccot . x)) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( exp_R * arccot )) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: for x st x in Z holds ( exp_R * arccot ) is_differentiable_in x

      proof

        let x;

        assume

         A4: x in Z;

         arccot is_differentiable_on Z by A2, Th82;

        then

         A5: arccot is_differentiable_in x by A4, FDIFF_1: 9;

         exp_R is_differentiable_in ( arccot . x) by SIN_COS: 65;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( exp_R * arccot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R * arccot ) `| Z) . x) = ( - (( exp_R . ( arccot . x)) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A7: x in Z;

        

         A8: exp_R is_differentiable_in ( arccot . x) by SIN_COS: 65;

        

         A9: arccot is_differentiable_on Z by A2, Th82;

        then arccot is_differentiable_in x by A7, FDIFF_1: 9;

        

        then ( diff (( exp_R * arccot ),x)) = (( diff ( exp_R ,( arccot . x))) * ( diff ( arccot ,x))) by A8, FDIFF_2: 13

        .= (( diff ( exp_R ,( arccot . x))) * (( arccot `| Z) . x)) by A7, A9, FDIFF_1:def 7

        .= (( diff ( exp_R ,( arccot . x))) * ( - (1 / (1 + (x ^2 ))))) by A2, A7, Th82

        .= ( - (( diff ( exp_R ,( arccot . x))) * (1 / (1 + (x ^2 )))))

        .= ( - (( exp_R . ( arccot . x)) / (1 + (x ^2 )))) by SIN_COS: 65;

        hence thesis by A6, A7, FDIFF_1:def 7;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: SIN_COS9:121

    Z c= ( dom ( arctan - ( id Z))) & Z c= ].( - 1), 1.[ implies ( arctan - ( id Z)) is_differentiable_on Z & for x st x in Z holds ((( arctan - ( id Z)) `| Z) . x) = ( - ((x ^2 ) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ( arctan - ( id Z))) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      Z c= (( dom arctan ) /\ ( dom ( id Z))) by A1, VALUED_1: 12;

      then

       A4: Z c= ( dom ( id Z)) by XBOOLE_1: 18;

      then

       A5: ( id Z) is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A6: arctan is_differentiable_on Z by A2, Th81;

      for x st x in Z holds ((( arctan - ( id Z)) `| Z) . x) = ( - ((x ^2 ) / (1 + (x ^2 ))))

      proof

        let x;

        

         A7: (1 + (x ^2 )) > 0 by XREAL_1: 34, XREAL_1: 63;

        assume

         A8: x in Z;

        

        then ((( arctan - ( id Z)) `| Z) . x) = (( diff ( arctan ,x)) - ( diff (( id Z),x))) by A1, A5, A6, FDIFF_1: 19

        .= ((( arctan `| Z) . x) - ( diff (( id Z),x))) by A6, A8, FDIFF_1:def 7

        .= ((1 / (1 + (x ^2 ))) - ( diff (( id Z),x))) by A2, A8, Th81

        .= ((1 / (1 + (x ^2 ))) - ((( id Z) `| Z) . x)) by A5, A8, FDIFF_1:def 7

        .= ((1 / (1 + (x ^2 ))) - 1) by A4, A3, A8, FDIFF_1: 23

        .= ((1 / (1 + (x ^2 ))) - ((1 + (x ^2 )) / (1 + (x ^2 )))) by A7, XCMPLX_1: 60

        .= ( - ((x ^2 ) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A5, A6, FDIFF_1: 19;

    end;

    theorem :: SIN_COS9:122

    Z c= ( dom (( - arccot ) - ( id Z))) & Z c= ].( - 1), 1.[ implies (( - arccot ) - ( id Z)) is_differentiable_on Z & for x st x in Z holds (((( - arccot ) - ( id Z)) `| Z) . x) = ( - ((x ^2 ) / (1 + (x ^2 ))))

    proof

      assume that

       A1: Z c= ( dom (( - arccot ) - ( id Z))) and

       A2: Z c= ].( - 1), 1.[;

      

       A3: arccot is_differentiable_on Z by A2, Th82;

      

       A4: Z c= (( dom ( - arccot )) /\ ( dom ( id Z))) by A1, VALUED_1: 12;

      then

       A5: Z c= ( dom ( id Z)) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      then

       A7: ( id Z) is_differentiable_on Z by A5, FDIFF_1: 23;

      

       A8: Z c= ( dom (( - 1) (#) arccot )) by A4, XBOOLE_1: 18;

      then

       A9: ( - arccot ) is_differentiable_on Z by A3, FDIFF_1: 20;

      for x st x in Z holds (((( - arccot ) - ( id Z)) `| Z) . x) = ( - ((x ^2 ) / (1 + (x ^2 ))))

      proof

        let x;

        

         A10: (1 + (x ^2 )) > 0 by XREAL_1: 34, XREAL_1: 63;

        assume

         A11: x in Z;

        

        then (((( - arccot ) - ( id Z)) `| Z) . x) = (( diff (( - arccot ),x)) - ( diff (( id Z),x))) by A1, A7, A9, FDIFF_1: 19

        .= (((( - arccot ) `| Z) . x) - ( diff (( id Z),x))) by A9, A11, FDIFF_1:def 7

        .= ((( - 1) * ( diff ( arccot ,x))) - ( diff (( id Z),x))) by A8, A3, A11, FDIFF_1: 20

        .= ((( - 1) * (( arccot `| Z) . x)) - ( diff (( id Z),x))) by A3, A11, FDIFF_1:def 7

        .= ((( - 1) * ( - (1 / (1 + (x ^2 ))))) - ( diff (( id Z),x))) by A2, A11, Th82

        .= ((1 / (1 + (x ^2 ))) - ((( id Z) `| Z) . x)) by A7, A11, FDIFF_1:def 7

        .= ((1 / (1 + (x ^2 ))) - 1) by A5, A6, A11, FDIFF_1: 23

        .= ((1 / (1 + (x ^2 ))) - ((1 + (x ^2 )) / (1 + (x ^2 )))) by A10, XCMPLX_1: 60

        .= ( - ((x ^2 ) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A7, A9, FDIFF_1: 19;

    end;

    theorem :: SIN_COS9:123

    Z c= ].( - 1), 1.[ implies ( exp_R (#) arctan ) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) arctan ) `| Z) . x) = ((( exp_R . x) * ( arctan . x)) + (( exp_R . x) / (1 + (x ^2 ))))

    proof

      assume

       A1: Z c= ].( - 1), 1.[;

      then

       A2: arctan is_differentiable_on Z by Th81;

       ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arctan ) by Th23;

      then Z c= ( dom arctan ) by A1;

      then Z c= (( dom exp_R ) /\ ( dom arctan )) by SIN_COS: 47, XBOOLE_1: 19;

      then

       A3: Z c= ( dom ( exp_R (#) arctan )) by VALUED_1:def 4;

      for x st x in Z holds exp_R is_differentiable_in x by SIN_COS: 65;

      then

       A4: exp_R is_differentiable_on Z by FDIFF_1: 9, SIN_COS: 47;

      for x st x in Z holds ((( exp_R (#) arctan ) `| Z) . x) = ((( exp_R . x) * ( arctan . x)) + (( exp_R . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((( exp_R (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff ( arctan ,x)))) by A3, A4, A2, FDIFF_1: 21

        .= ((( arctan . x) * ( exp_R . x)) + (( exp_R . x) * ( diff ( arctan ,x)))) by SIN_COS: 65

        .= ((( exp_R . x) * ( arctan . x)) + (( exp_R . x) * (( arctan `| Z) . x))) by A2, A5, FDIFF_1:def 7

        .= ((( exp_R . x) * ( arctan . x)) + (( exp_R . x) * (1 / (1 + (x ^2 ))))) by A1, A5, Th81

        .= ((( exp_R . x) * ( arctan . x)) + (( exp_R . x) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A3, A4, A2, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:124

    Z c= ].( - 1), 1.[ implies ( exp_R (#) arccot ) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) arccot ) `| Z) . x) = ((( exp_R . x) * ( arccot . x)) - (( exp_R . x) / (1 + (x ^2 ))))

    proof

      assume

       A1: Z c= ].( - 1), 1.[;

      then

       A2: arccot is_differentiable_on Z by Th82;

       ].( - 1), 1.[ c= [.( - 1), 1.] by XXREAL_1: 25;

      then ].( - 1), 1.[ c= ( dom arccot ) by Th24;

      then Z c= ( dom arccot ) by A1;

      then Z c= (( dom exp_R ) /\ ( dom arccot )) by SIN_COS: 47, XBOOLE_1: 19;

      then

       A3: Z c= ( dom ( exp_R (#) arccot )) by VALUED_1:def 4;

      for x st x in Z holds exp_R is_differentiable_in x by SIN_COS: 65;

      then

       A4: exp_R is_differentiable_on Z by FDIFF_1: 9, SIN_COS: 47;

      for x st x in Z holds ((( exp_R (#) arccot ) `| Z) . x) = ((( exp_R . x) * ( arccot . x)) - (( exp_R . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((( exp_R (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff ( arccot ,x)))) by A3, A4, A2, FDIFF_1: 21

        .= ((( arccot . x) * ( exp_R . x)) + (( exp_R . x) * ( diff ( arccot ,x)))) by SIN_COS: 65

        .= ((( exp_R . x) * ( arccot . x)) + (( exp_R . x) * (( arccot `| Z) . x))) by A2, A5, FDIFF_1:def 7

        .= ((( exp_R . x) * ( arccot . x)) + (( exp_R . x) * ( - (1 / (1 + (x ^2 )))))) by A1, A5, Th82

        .= ((( exp_R . x) * ( arccot . x)) - (( exp_R . x) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A3, A4, A2, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:125

    Z c= ( dom (((1 / r) (#) ( arctan * f)) - ( id Z))) & (for x st x in Z holds (f . x) = (r * x) & r <> 0 & (f . x) > ( - 1) & (f . x) < 1) implies (((1 / r) (#) ( arctan * f)) - ( id Z)) is_differentiable_on Z & for x st x in Z holds (((((1 / r) (#) ( arctan * f)) - ( id Z)) `| Z) . x) = ( - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom (((1 / r) (#) ( arctan * f)) - ( id Z))) and

       A2: for x st x in Z holds (f . x) = (r * x) & r <> 0 & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: for x st x in Z holds (f . x) = ((r * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A2;

      set g = ((1 / r) (#) ( arctan * f));

      

       A4: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      

       A5: Z c= (( dom ((1 / r) (#) ( arctan * f))) /\ ( dom ( id Z))) by A1, VALUED_1: 12;

      then

       A6: Z c= ( dom ((1 / r) (#) ( arctan * f))) by XBOOLE_1: 18;

      

       A7: Z c= ( dom ( id Z)) by A5, XBOOLE_1: 18;

      then

       A8: ( id Z) is_differentiable_on Z by A4, FDIFF_1: 23;

      

       A9: Z c= ( dom ( arctan * f)) by A6, VALUED_1:def 5;

      then

       A10: ( arctan * f) is_differentiable_on Z by A3, Th87;

      then

       A11: ((1 / r) (#) ( arctan * f)) is_differentiable_on Z by A6, FDIFF_1: 20;

      for x st x in Z holds (((((1 / r) (#) ( arctan * f)) - ( id Z)) `| Z) . x) = ( - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))))

      proof

        let x;

        

         A12: (1 + ((r * x) ^2 )) > 0 by XREAL_1: 34, XREAL_1: 63;

        assume

         A13: x in Z;

        then

         A14: r <> 0 by A2;

        (((g - ( id Z)) `| Z) . x) = (( diff (g,x)) - ( diff (( id Z),x))) by A1, A11, A8, A13, FDIFF_1: 19

        .= (((g `| Z) . x) - ( diff (( id Z),x))) by A11, A13, FDIFF_1:def 7

        .= (((1 / r) * ( diff (( arctan * f),x))) - ( diff (( id Z),x))) by A6, A10, A13, FDIFF_1: 20

        .= (((1 / r) * ((( arctan * f) `| Z) . x)) - ( diff (( id Z),x))) by A10, A13, FDIFF_1:def 7

        .= (((1 / r) * ((( arctan * f) `| Z) . x)) - ((( id Z) `| Z) . x)) by A8, A13, FDIFF_1:def 7

        .= (((1 / r) * (r / (1 + (((r * x) + 0 ) ^2 )))) - ((( id Z) `| Z) . x)) by A3, A9, A13, Th87

        .= (((1 / r) * (r / (1 + ((r * x) ^2 )))) - 1) by A7, A4, A13, FDIFF_1: 23

        .= (((1 * r) / (r * (1 + ((r * x) ^2 )))) - 1) by XCMPLX_1: 76

        .= ((1 / (1 + ((r * x) ^2 ))) - 1) by A14, XCMPLX_1: 91

        .= ((1 / (1 + ((r * x) ^2 ))) - ((1 + ((r * x) ^2 )) / (1 + ((r * x) ^2 )))) by A12, XCMPLX_1: 60

        .= ( - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A11, A8, FDIFF_1: 19;

    end;

    theorem :: SIN_COS9:126

    Z c= ( dom ((( - (1 / r)) (#) ( arccot * f)) - ( id Z))) & (for x st x in Z holds (f . x) = (r * x) & r <> 0 & (f . x) > ( - 1) & (f . x) < 1) implies ((( - (1 / r)) (#) ( arccot * f)) - ( id Z)) is_differentiable_on Z & for x st x in Z holds ((((( - (1 / r)) (#) ( arccot * f)) - ( id Z)) `| Z) . x) = ( - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))))

    proof

      assume that

       A1: Z c= ( dom ((( - (1 / r)) (#) ( arccot * f)) - ( id Z))) and

       A2: for x st x in Z holds (f . x) = (r * x) & r <> 0 & (f . x) > ( - 1) & (f . x) < 1;

      

       A3: for x st x in Z holds (f . x) = ((r * x) + 0 ) & (f . x) > ( - 1) & (f . x) < 1 by A2;

      set g = (( - (1 / r)) (#) ( arccot * f));

      

       A4: for x st x in Z holds (( id Z) . x) = ((1 * x) + 0 ) by FUNCT_1: 18;

      

       A5: Z c= (( dom (( - (1 / r)) (#) ( arccot * f))) /\ ( dom ( id Z))) by A1, VALUED_1: 12;

      then

       A6: Z c= ( dom (( - (1 / r)) (#) ( arccot * f))) by XBOOLE_1: 18;

      

       A7: Z c= ( dom ( id Z)) by A5, XBOOLE_1: 18;

      then

       A8: ( id Z) is_differentiable_on Z by A4, FDIFF_1: 23;

      

       A9: Z c= ( dom ( arccot * f)) by A6, VALUED_1:def 5;

      then

       A10: ( arccot * f) is_differentiable_on Z by A3, Th88;

      then

       A11: (( - (1 / r)) (#) ( arccot * f)) is_differentiable_on Z by A6, FDIFF_1: 20;

      for x st x in Z holds ((((( - (1 / r)) (#) ( arccot * f)) - ( id Z)) `| Z) . x) = ( - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))))

      proof

        let x;

        

         A12: (1 + ((r * x) ^2 )) > 0 by XREAL_1: 34, XREAL_1: 63;

        assume

         A13: x in Z;

        then

         A14: r <> 0 by A2;

        (((g - ( id Z)) `| Z) . x) = (( diff (g,x)) - ( diff (( id Z),x))) by A1, A11, A8, A13, FDIFF_1: 19

        .= (((g `| Z) . x) - ( diff (( id Z),x))) by A11, A13, FDIFF_1:def 7

        .= ((( - (1 / r)) * ( diff (( arccot * f),x))) - ( diff (( id Z),x))) by A6, A10, A13, FDIFF_1: 20

        .= ((( - (1 / r)) * ((( arccot * f) `| Z) . x)) - ( diff (( id Z),x))) by A10, A13, FDIFF_1:def 7

        .= ((( - (1 / r)) * ((( arccot * f) `| Z) . x)) - ((( id Z) `| Z) . x)) by A8, A13, FDIFF_1:def 7

        .= ((( - (1 / r)) * ( - (r / (1 + (((r * x) + 0 ) ^2 ))))) - ((( id Z) `| Z) . x)) by A3, A9, A13, Th88

        .= (((( - 1) / r) * (( - r) / (1 + ((r * x) ^2 )))) - 1) by A7, A4, A13, FDIFF_1: 23

        .= (((( - 1) * ( - r)) / (r * (1 + ((r * x) ^2 )))) - 1) by XCMPLX_1: 76

        .= (((1 * r) / (r * (1 + ((r * x) ^2 )))) - 1)

        .= ((1 / (1 + ((r * x) ^2 ))) - 1) by A14, XCMPLX_1: 91

        .= ((1 / (1 + ((r * x) ^2 ))) - ((1 + ((r * x) ^2 )) / (1 + ((r * x) ^2 )))) by A12, XCMPLX_1: 60

        .= ( - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))));

        hence thesis;

      end;

      hence thesis by A1, A11, A8, FDIFF_1: 19;

    end;

    theorem :: SIN_COS9:127

    Z c= ( dom ( ln (#) arctan )) & Z c= ].( - 1), 1.[ implies ( ln (#) arctan ) is_differentiable_on Z & for x st x in Z holds ((( ln (#) arctan ) `| Z) . x) = ((( arctan . x) / x) + (( ln . x) / (1 + (x ^2 ))))

    proof

      

       A1: ( right_open_halfline 0 ) = { g where g be Real : 0 < g } by XXREAL_1: 230;

      assume that

       A2: Z c= ( dom ( ln (#) arctan )) and

       A3: Z c= ].( - 1), 1.[;

      

       A4: arctan is_differentiable_on Z by A3, Th81;

      Z c= (( dom ln ) /\ ( dom arctan )) by A2, VALUED_1:def 4;

      then

       A5: Z c= ( dom ln ) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A5, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by A1;

        hence thesis;

      end;

      then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1: 18;

      then

       A7: ln is_differentiable_on Z by A5, FDIFF_1: 9;

      

       A8: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A6;

        then x in ( right_open_halfline 0 ) by A1;

        hence thesis by TAYLOR_1: 18;

      end;

      for x st x in Z holds ((( ln (#) arctan ) `| Z) . x) = ((( arctan . x) / x) + (( ln . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A9: x in Z;

        

        then ((( ln (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff ( ln ,x))) + (( ln . x) * ( diff ( arctan ,x)))) by A2, A7, A4, FDIFF_1: 21

        .= ((( arctan . x) * (1 / x)) + (( ln . x) * ( diff ( arctan ,x)))) by A8, A9

        .= ((( arctan . x) * (1 / x)) + (( ln . x) * (( arctan `| Z) . x))) by A4, A9, FDIFF_1:def 7

        .= (((( arctan . x) * 1) / x) + (( ln . x) * (1 / (1 + (x ^2 ))))) by A3, A9, Th81

        .= ((( arctan . x) / x) + (( ln . x) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A2, A7, A4, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:128

    Z c= ( dom ( ln (#) arccot )) & Z c= ].( - 1), 1.[ implies ( ln (#) arccot ) is_differentiable_on Z & for x st x in Z holds ((( ln (#) arccot ) `| Z) . x) = ((( arccot . x) / x) - (( ln . x) / (1 + (x ^2 ))))

    proof

      

       A1: ( right_open_halfline 0 ) = { g where g be Real : 0 < g } by XXREAL_1: 230;

      assume that

       A2: Z c= ( dom ( ln (#) arccot )) and

       A3: Z c= ].( - 1), 1.[;

      

       A4: arccot is_differentiable_on Z by A3, Th82;

      Z c= (( dom ln ) /\ ( dom arccot )) by A2, VALUED_1:def 4;

      then

       A5: Z c= ( dom ln ) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A5, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by A1;

        hence thesis;

      end;

      then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1: 18;

      then

       A7: ln is_differentiable_on Z by A5, FDIFF_1: 9;

      

       A8: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A6;

        then x in ( right_open_halfline 0 ) by A1;

        hence thesis by TAYLOR_1: 18;

      end;

      for x st x in Z holds ((( ln (#) arccot ) `| Z) . x) = ((( arccot . x) / x) - (( ln . x) / (1 + (x ^2 ))))

      proof

        let x;

        assume

         A9: x in Z;

        

        then ((( ln (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ( ln ,x))) + (( ln . x) * ( diff ( arccot ,x)))) by A2, A7, A4, FDIFF_1: 21

        .= ((( arccot . x) * (1 / x)) + (( ln . x) * ( diff ( arccot ,x)))) by A8, A9

        .= ((( arccot . x) * (1 / x)) + (( ln . x) * (( arccot `| Z) . x))) by A4, A9, FDIFF_1:def 7

        .= ((( arccot . x) * (1 / x)) + (( ln . x) * ( - (1 / (1 + (x ^2 )))))) by A3, A9, Th82

        .= ((( arccot . x) / x) - (( ln . x) / (1 + (x ^2 ))));

        hence thesis;

      end;

      hence thesis by A2, A7, A4, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:129

     not 0 in Z & Z c= ( dom ((( id Z) ^ ) (#) arctan )) & Z c= ].( - 1), 1.[ implies ((( id Z) ^ ) (#) arctan ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) ^ ) (#) arctan ) `| Z) . x) = (( - (( arctan . x) / (x ^2 ))) + (1 / (x * (1 + (x ^2 )))))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ((f ^ ) (#) arctan )) and

       A3: Z c= ].( - 1), 1.[;

      

       A4: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

       A5: arctan is_differentiable_on Z by A3, Th81;

      Z c= (( dom (f ^ )) /\ ( dom arctan )) by A2, VALUED_1:def 4;

      then

       A6: Z c= ( dom (f ^ )) by XBOOLE_1: 18;

      for x st x in Z holds ((((f ^ ) (#) arctan ) `| Z) . x) = (( - (( arctan . x) / (x ^2 ))) + (1 / (x * (1 + (x ^2 )))))

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((((f ^ ) (#) arctan ) `| Z) . x) = ((( arctan . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( arctan ,x)))) by A2, A4, A5, FDIFF_1: 21

        .= ((( arctan . x) * (((f ^ ) `| Z) . x)) + (((f ^ ) . x) * ( diff ( arctan ,x)))) by A4, A7, FDIFF_1:def 7

        .= ((( arctan . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( arctan ,x)))) by A1, A7, FDIFF_5: 4

        .= (( - (( arctan . x) * (1 / (x ^2 )))) + (((f ^ ) . x) * (( arctan `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (( - ((( arctan . x) * 1) / (x ^2 ))) + (((f ^ ) . x) * (1 / (1 + (x ^2 ))))) by A3, A7, Th81

        .= (( - (( arctan . x) / (x ^2 ))) + (((f . x) " ) * (1 / (1 + (x ^2 ))))) by A6, A7, RFUNCT_1:def 2

        .= (( - (( arctan . x) / (x ^2 ))) + ((1 / x) * (1 / (1 + (x ^2 ))))) by A7, FUNCT_1: 18

        .= (( - (( arctan . x) / (x ^2 ))) + ((1 * 1) / (x * (1 + (x ^2 ))))) by XCMPLX_1: 76

        .= (( - (( arctan . x) / (x ^2 ))) + (1 / (x * (1 + (x ^2 )))));

        hence thesis;

      end;

      hence thesis by A2, A4, A5, FDIFF_1: 21;

    end;

    theorem :: SIN_COS9:130

     not 0 in Z & Z c= ( dom ((( id Z) ^ ) (#) arccot )) & Z c= ].( - 1), 1.[ implies ((( id Z) ^ ) (#) arccot ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) ^ ) (#) arccot ) `| Z) . x) = (( - (( arccot . x) / (x ^2 ))) - (1 / (x * (1 + (x ^2 )))))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ((f ^ ) (#) arccot )) and

       A3: Z c= ].( - 1), 1.[;

      

       A4: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

       A5: arccot is_differentiable_on Z by A3, Th82;

      Z c= (( dom (f ^ )) /\ ( dom arccot )) by A2, VALUED_1:def 4;

      then

       A6: Z c= ( dom (f ^ )) by XBOOLE_1: 18;

      for x st x in Z holds ((((f ^ ) (#) arccot ) `| Z) . x) = (( - (( arccot . x) / (x ^2 ))) - (1 / (x * (1 + (x ^2 )))))

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((((f ^ ) (#) arccot ) `| Z) . x) = ((( arccot . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( arccot ,x)))) by A2, A4, A5, FDIFF_1: 21

        .= ((( arccot . x) * (((f ^ ) `| Z) . x)) + (((f ^ ) . x) * ( diff ( arccot ,x)))) by A4, A7, FDIFF_1:def 7

        .= ((( arccot . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( arccot ,x)))) by A1, A7, FDIFF_5: 4

        .= (( - (( arccot . x) * (1 / (x ^2 )))) + (((f ^ ) . x) * (( arccot `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (( - (( arccot . x) * (1 / (x ^2 )))) + (((f ^ ) . x) * ( - (1 / (1 + (x ^2 )))))) by A3, A7, Th82

        .= (( - ((( arccot . x) * 1) / (x ^2 ))) - (((f ^ ) . x) * (1 / (1 + (x ^2 )))))

        .= (( - (( arccot . x) / (x ^2 ))) - (((f . x) " ) * (1 / (1 + (x ^2 ))))) by A6, A7, RFUNCT_1:def 2

        .= (( - (( arccot . x) / (x ^2 ))) - ((1 / x) * (1 / (1 + (x ^2 ))))) by A7, FUNCT_1: 18

        .= (( - (( arccot . x) / (x ^2 ))) - ((1 * 1) / (x * (1 + (x ^2 ))))) by XCMPLX_1: 76

        .= (( - (( arccot . x) / (x ^2 ))) - (1 / (x * (1 + (x ^2 )))));

        hence thesis;

      end;

      hence thesis by A2, A4, A5, FDIFF_1: 21;

    end;