fdiff_8.miz



    begin

    reserve x,a,b,c for Real,

n for Nat,

Z for open Subset of REAL ,

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

    theorem :: FDIFF_8:1

    

     Th1: x in ( dom tan ) implies ( cos . x) <> 0

    proof

      assume x in ( dom tan );

      then x in (( dom sin ) /\ (( dom cos ) \ ( cos " { 0 }))) by RFUNCT_1:def 1;

      then x in (( dom cos ) \ ( cos " { 0 })) by XBOOLE_0:def 4;

      then x in ( dom ( cos ^ )) by RFUNCT_1:def 2;

      hence thesis by RFUNCT_1: 3;

    end;

    theorem :: FDIFF_8:2

    

     Th2: x in ( dom cot ) implies ( sin . x) <> 0

    proof

      assume x in ( dom cot );

      then x in (( dom cos ) /\ (( dom sin ) \ ( sin " { 0 }))) by RFUNCT_1:def 1;

      then x in (( dom sin ) \ ( sin " { 0 })) by XBOOLE_0:def 4;

      then x in ( dom ( sin ^ )) by RFUNCT_1:def 2;

      hence thesis by RFUNCT_1: 3;

    end;

    theorem :: FDIFF_8:3

    

     Th3: Z c= ( dom (f1 / f2)) implies for x st x in Z holds (((f1 / f2) . x) #Z n) = (((f1 . x) #Z n) / ((f2 . x) #Z n))

    proof

      assume

       A1: Z c= ( dom (f1 / f2));

      let x;

      assume x in Z;

      

      then (((f1 / f2) . x) #Z n) = (((f1 . x) / (f2 . x)) #Z n) by A1, RFUNCT_1:def 1

      .= (((f1 . x) / (f2 . x)) |^ n) by PREPOWER: 36

      .= (((f1 . x) |^ n) / ((f2 . x) |^ n)) by PREPOWER: 8

      .= (((f1 . x) #Z n) / ((f2 . x) |^ n)) by PREPOWER: 36

      .= (((f1 . x) #Z n) / ((f2 . x) #Z n)) by PREPOWER: 36;

      hence thesis;

    end;

    theorem :: FDIFF_8:4

    Z c= ( dom (f1 / f2)) & (for x st x in Z holds (f1 . x) = (x + a) & (f2 . x) = (x - b)) implies (f1 / f2) is_differentiable_on Z & for x st x in Z holds (((f1 / f2) `| Z) . x) = ((( - a) - b) / ((x - b) ^2 ))

    proof

      assume that

       A1: Z c= ( dom (f1 / f2)) and

       A2: for x st x in Z holds (f1 . x) = (x + a) & (f2 . x) = (x - b);

      Z c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by A1, RFUNCT_1:def 1;

      then

       A3: Z c= (( dom f2) \ (f2 " { 0 })) by XBOOLE_1: 18;

      for x st x in Z holds (f2 . x) <> 0

      proof

        let x;

        assume x in Z;

        then x in (( dom f2) \ (f2 " { 0 })) by A3;

        then x in ( dom (f2 ^ )) by RFUNCT_1:def 2;

        hence thesis by RFUNCT_1: 3;

      end;

      then for x st x in Z holds (f1 . x) = (x - ( - a)) & (f2 . x) = (x - b) & (f2 . x) <> 0 by A2;

      hence thesis by A1, FDIFF_5: 3;

    end;

    

     Lm1: ( right_open_halfline 0 ) = { g where g be Real : 0 < g } by XXREAL_1: 230;

    theorem :: FDIFF_8:5

     not 0 in Z & Z c= ( dom ( ln * (( id Z) ^ ))) implies ( ln * (( id Z) ^ )) is_differentiable_on Z & for x st x in Z holds ((( ln * (( id Z) ^ )) `| Z) . x) = ( - (1 / x))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ( ln * (( id Z) ^ )));

      ( dom ( ln * (f ^ ))) c= ( dom (f ^ )) by RELAT_1: 25;

      then

       A3: Z c= ( dom (f ^ )) by A2, XBOOLE_1: 1;

      

       A4: for x st x in Z holds ((f ^ ) . x) > 0

      proof

        let x;

        assume

         A5: x in Z;

        

        then

         A6: ((f ^ ) . x) = ((f . x) " ) by A3, RFUNCT_1:def 2

        .= (1 / x) by A5, FUNCT_1: 18;

        ((f ^ ) . x) in ( right_open_halfline 0 ) by A2, A5, FUNCT_1: 11, TAYLOR_1: 18;

        then ex g be Real st (1 / x) = g & 0 < g by A6, Lm1;

        hence thesis by A6;

      end;

      

       A7: for x st x in Z holds (f . x) > 0

      proof

        let x;

        assume

         A8: x in Z;

        then ((f ^ ) . x) > 0 by A4;

        then ((f . x) " ) > 0 by A3, A8, RFUNCT_1:def 2;

        hence thesis;

      end;

      

       A9: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

       A10: for x st x in Z holds ( ln * (f ^ )) is_differentiable_in x & ( diff (( ln * (f ^ )),x)) = (( diff ((f ^ ),x)) / ((f ^ ) . x))

      proof

        let x;

        assume x in Z;

        then (f ^ ) is_differentiable_in x & ((f ^ ) . x) > 0 by A4, A9, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A11: for x st x in Z holds ( ln * (f ^ )) is_differentiable_in x;

      then

       A12: ( ln * (f ^ )) is_differentiable_on Z by A2, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A13: x in Z;

        then (f . x) <> 0 by A7;

        then

         A14: x <> 0 by A13, FUNCT_1: 18;

        ( diff (( ln * (f ^ )),x)) = (( diff ((f ^ ),x)) / ((f ^ ) . x)) by A10, A13

        .= ((((f ^ ) `| Z) . x) / ((f ^ ) . x)) by A9, A13, FDIFF_1:def 7

        .= ((((f ^ ) `| Z) . x) / ((f . x) " )) by A3, A13, RFUNCT_1:def 2

        .= ((((f ^ ) `| Z) . x) / (1 * (x " ))) by A13, FUNCT_1: 18

        .= (( - (1 / (x ^2 ))) / (1 * (x " ))) by A1, A13, FDIFF_5: 4

        .= ( - (x / (x ^2 )))

        .= ( - ((x / x) / x)) by XCMPLX_1: 78

        .= ( - (1 / x)) by A14, XCMPLX_1: 60;

        hence thesis by A12, A13, FDIFF_1:def 7;

      end;

      hence thesis by A2, A11, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:6

    

     Th6: Z c= ( dom ( tan * f)) & (for x st x in Z holds (f . x) = ((a * x) + b)) implies ( tan * f) is_differentiable_on Z & for x st x in Z holds ((( tan * f) `| Z) . x) = (a / (( cos . ((a * x) + b)) ^2 ))

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = ((a * x) + b);

      ( dom ( tan * f)) c= ( dom f) by RELAT_1: 25;

      then

       A3: Z c= ( dom f) by A1, XBOOLE_1: 1;

      then

       A4: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A5: for x st x in Z holds ( cos . (f . x)) <> 0

      proof

        let x;

        assume x in Z;

        then (f . x) in ( dom ( sin / cos )) by A1, FUNCT_1: 11;

        hence thesis by Th1;

      end;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        then ( cos . (f . x)) <> 0 by A5;

        then

         A8: tan is_differentiable_in (f . x) by FDIFF_7: 46;

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

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( tan * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( tan * f) `| Z) . x) = (a / (( cos . ((a * x) + b)) ^2 ))

      proof

        let x;

        assume

         A10: x in Z;

        then

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

        

         A12: ( cos . (f . x)) <> 0 by A5, A10;

        then tan is_differentiable_in (f . x) by FDIFF_7: 46;

        

        then ( diff (( tan * f),x)) = (( diff ( tan ,(f . x))) * ( diff (f,x))) by A11, FDIFF_2: 13

        .= ((1 / (( cos . (f . x)) ^2 )) * ( diff (f,x))) by A12, FDIFF_7: 46

        .= (( diff (f,x)) / (( cos . ((a * x) + b)) ^2 )) by A2, A10

        .= (((f `| Z) . x) / (( cos . ((a * x) + b)) ^2 )) by A4, A10, FDIFF_1:def 7

        .= (a / (( cos . ((a * x) + b)) ^2 )) by A2, A3, A10, FDIFF_1: 23;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:7

    

     Th7: Z c= ( dom ( cot * f)) & (for x st x in Z holds (f . x) = ((a * x) + b)) implies ( cot * f) is_differentiable_on Z & for x st x in Z holds ((( cot * f) `| Z) . x) = ( - (a / (( sin . ((a * x) + b)) ^2 )))

    proof

      assume that

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

       A2: for x st x in Z holds (f . x) = ((a * x) + b);

      ( dom ( cot * f)) c= ( dom f) by RELAT_1: 25;

      then

       A3: Z c= ( dom f) by A1, XBOOLE_1: 1;

      then

       A4: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A5: for x st x in Z holds ( sin . (f . x)) <> 0

      proof

        let x;

        assume x in Z;

        then (f . x) in ( dom ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by Th2;

      end;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        then ( sin . (f . x)) <> 0 by A5;

        then

         A8: cot is_differentiable_in (f . x) by FDIFF_7: 47;

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

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( cot * f) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cot * f) `| Z) . x) = ( - (a / (( sin . ((a * x) + b)) ^2 )))

      proof

        let x;

        assume

         A10: x in Z;

        then

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

        

         A12: ( sin . (f . x)) <> 0 by A5, A10;

        then cot is_differentiable_in (f . x) by FDIFF_7: 47;

        

        then ( diff (( cot * f),x)) = (( diff ( cot ,(f . x))) * ( diff (f,x))) by A11, FDIFF_2: 13

        .= (( - (1 / (( sin . (f . x)) ^2 ))) * ( diff (f,x))) by A12, FDIFF_7: 47

        .= ( - (( diff (f,x)) / (( sin . (f . x)) ^2 )))

        .= ( - (( diff (f,x)) / (( sin . ((a * x) + b)) ^2 ))) by A2, A10

        .= ( - (((f `| Z) . x) / (( sin . ((a * x) + b)) ^2 ))) by A4, A10, FDIFF_1:def 7

        .= ( - (a / (( sin . ((a * x) + b)) ^2 ))) by A2, A3, A10, FDIFF_1: 23;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:8

     not 0 in Z & Z c= ( dom ( tan * (( id Z) ^ ))) implies ( tan * (( id Z) ^ )) is_differentiable_on Z & for x st x in Z holds ((( tan * (( id Z) ^ )) `| Z) . x) = ( - (1 / ((x ^2 ) * (( cos . (1 / x)) ^2 ))))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ( tan * (( id Z) ^ )));

      

       A3: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      ( dom ( tan * (f ^ ))) c= ( dom (f ^ )) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f ^ )) by A2, XBOOLE_1: 1;

      

       A5: for x st x in Z holds ( cos . ((f ^ ) . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ((f ^ ) . x) in ( dom ( sin / cos )) by A2, FUNCT_1: 11;

        hence thesis by Th1;

      end;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        then ( cos . ((f ^ ) . x)) <> 0 by A5;

        then

         A8: tan is_differentiable_in ((f ^ ) . x) by FDIFF_7: 46;

        (f ^ ) is_differentiable_in x by A3, A7, FDIFF_1: 9;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( tan * (f ^ )) is_differentiable_on Z by A2, FDIFF_1: 9;

      for x st x in Z holds ((( tan * (f ^ )) `| Z) . x) = ( - (1 / ((x ^2 ) * (( cos . (1 / x)) ^2 ))))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: (f ^ ) is_differentiable_in x by A3, FDIFF_1: 9;

        

         A12: ( cos . ((f ^ ) . x)) <> 0 by A5, A10;

        then tan is_differentiable_in ((f ^ ) . x) by FDIFF_7: 46;

        

        then ( diff (( tan * (f ^ )),x)) = (( diff ( tan ,((f ^ ) . x))) * ( diff ((f ^ ),x))) by A11, FDIFF_2: 13

        .= ((1 / (( cos . ((f ^ ) . x)) ^2 )) * ( diff ((f ^ ),x))) by A12, FDIFF_7: 46

        .= (( diff ((f ^ ),x)) / (( cos . ((f . x) " )) ^2 )) by A4, A10, RFUNCT_1:def 2

        .= (( diff ((f ^ ),x)) / (( cos . (1 * (x " ))) ^2 )) by A10, FUNCT_1: 18

        .= ((((f ^ ) `| Z) . x) / (( cos . (1 * (x " ))) ^2 )) by A3, A10, FDIFF_1:def 7

        .= (( - (1 / (x ^2 ))) / (( cos . (1 * (x " ))) ^2 )) by A1, A10, FDIFF_5: 4

        .= ((( - 1) / (x ^2 )) / (( cos . (1 / x)) ^2 ))

        .= (( - 1) / ((x ^2 ) * (( cos . (1 / x)) ^2 ))) by XCMPLX_1: 78

        .= ( - (1 / ((x ^2 ) * (( cos . (1 / x)) ^2 ))));

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

      end;

      hence thesis by A2, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:9

     not 0 in Z & Z c= ( dom ( cot * (( id Z) ^ ))) implies ( cot * (( id Z) ^ )) is_differentiable_on Z & for x st x in Z holds ((( cot * (( id Z) ^ )) `| Z) . x) = (1 / ((x ^2 ) * (( sin . (1 / x)) ^2 )))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ( cot * (f ^ )));

      

       A3: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      ( dom ( cot * (f ^ ))) c= ( dom (f ^ )) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f ^ )) by A2, XBOOLE_1: 1;

      

       A5: for x st x in Z holds ( sin . ((f ^ ) . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ((f ^ ) . x) in ( dom ( cos / sin )) by A2, FUNCT_1: 11;

        hence thesis by Th2;

      end;

      

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

      proof

        let x;

        assume

         A7: x in Z;

        then ( sin . ((f ^ ) . x)) <> 0 by A5;

        then

         A8: cot is_differentiable_in ((f ^ ) . x) by FDIFF_7: 47;

        (f ^ ) is_differentiable_in x by A3, A7, FDIFF_1: 9;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( cot * (f ^ )) is_differentiable_on Z by A2, FDIFF_1: 9;

      for x st x in Z holds ((( cot * (f ^ )) `| Z) . x) = (1 / ((x ^2 ) * (( sin . (1 / x)) ^2 )))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: (f ^ ) is_differentiable_in x by A3, FDIFF_1: 9;

        

         A12: ( sin . ((f ^ ) . x)) <> 0 by A5, A10;

        then cot is_differentiable_in ((f ^ ) . x) by FDIFF_7: 47;

        

        then ( diff (( cot * (f ^ )),x)) = (( diff ( cot ,((f ^ ) . x))) * ( diff ((f ^ ),x))) by A11, FDIFF_2: 13

        .= (( - (1 / (( sin . ((f ^ ) . x)) ^2 ))) * ( diff ((f ^ ),x))) by A12, FDIFF_7: 47

        .= ( - (( diff ((f ^ ),x)) / (( sin . ((f ^ ) . x)) ^2 )))

        .= ( - (( diff ((f ^ ),x)) / (( sin . ((f . x) " )) ^2 ))) by A4, A10, RFUNCT_1:def 2

        .= ( - (( diff ((f ^ ),x)) / (( sin . (1 * (x " ))) ^2 ))) by A10, FUNCT_1: 18

        .= ( - ((((f ^ ) `| Z) . x) / (( sin . (1 * (x " ))) ^2 ))) by A3, A10, FDIFF_1:def 7

        .= ( - (( - (1 / (x ^2 ))) / (( sin . (1 * (x " ))) ^2 ))) by A1, A10, FDIFF_5: 4

        .= ( - ((( - 1) / (x ^2 )) / (( sin . (1 / x)) ^2 )))

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

        .= (1 / ((x ^2 ) * (( sin . (1 / x)) ^2 )));

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

      end;

      hence thesis by A2, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:10

    Z c= ( dom ( tan * (f1 + (c (#) f2)))) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a + (b * x))) implies ( tan * (f1 + (c (#) f2))) is_differentiable_on Z & for x st x in Z holds ((( tan * (f1 + (c (#) f2))) `| Z) . x) = ((b + ((2 * c) * x)) / (( cos . ((a + (b * x)) + (c * (x ^2 )))) ^2 ))

    proof

      assume that

       A1: Z c= ( dom ( tan * (f1 + (c (#) f2)))) and

       A2: f2 = ( #Z 2) and

       A3: for x st x in Z holds (f1 . x) = (a + (b * x));

      ( dom ( tan * (f1 + (c (#) f2)))) c= ( dom (f1 + (c (#) f2))) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f1 + (c (#) f2))) by A1, XBOOLE_1: 1;

      then

       A5: (f1 + (c (#) f2)) is_differentiable_on Z by A2, A3, FDIFF_4: 12;

      Z c= (( dom f1) /\ ( dom (c (#) f2))) by A4, VALUED_1:def 1;

      then

       A6: Z c= ( dom (c (#) f2)) by XBOOLE_1: 18;

      

       A7: for x st x in Z holds ( cos . ((f1 + (c (#) f2)) . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ((f1 + (c (#) f2)) . x) in ( dom ( sin / cos )) by A1, FUNCT_1: 11;

        hence thesis by Th1;

      end;

      

       A8: for x st x in Z holds ( tan * (f1 + (c (#) f2))) is_differentiable_in x

      proof

        let x;

        assume

         A9: x in Z;

        then ( cos . ((f1 + (c (#) f2)) . x)) <> 0 by A7;

        then

         A10: tan is_differentiable_in ((f1 + (c (#) f2)) . x) by FDIFF_7: 46;

        (f1 + (c (#) f2)) is_differentiable_in x by A5, A9, FDIFF_1: 9;

        hence thesis by A10, FDIFF_2: 13;

      end;

      then

       A11: ( tan * (f1 + (c (#) f2))) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( tan * (f1 + (c (#) f2))) `| Z) . x) = ((b + ((2 * c) * x)) / (( cos . ((a + (b * x)) + (c * (x ^2 )))) ^2 ))

      proof

        let x;

        assume

         A12: x in Z;

        

        then

         A13: ((f1 + (c (#) f2)) . x) = ((f1 . x) + ((c (#) f2) . x)) by A4, VALUED_1:def 1

        .= ((f1 . x) + (c * (f2 . x))) by A6, A12, VALUED_1:def 5

        .= ((a + (b * x)) + (c * (f2 . x))) by A3, A12

        .= ((a + (b * x)) + (c * (x #Z 2))) by A2, TAYLOR_1:def 1

        .= ((a + (b * x)) + (c * (x |^ 2))) by PREPOWER: 36

        .= ((a + (b * x)) + (c * (x ^2 ))) by NEWTON: 81;

        

         A14: (f1 + (c (#) f2)) is_differentiable_in x by A5, A12, FDIFF_1: 9;

        

         A15: ( cos . ((f1 + (c (#) f2)) . x)) <> 0 by A7, A12;

        then tan is_differentiable_in ((f1 + (c (#) f2)) . x) by FDIFF_7: 46;

        

        then ( diff (( tan * (f1 + (c (#) f2))),x)) = (( diff ( tan ,((f1 + (c (#) f2)) . x))) * ( diff ((f1 + (c (#) f2)),x))) by A14, FDIFF_2: 13

        .= ((1 / (( cos . ((f1 + (c (#) f2)) . x)) ^2 )) * ( diff ((f1 + (c (#) f2)),x))) by A15, FDIFF_7: 46

        .= ((((f1 + (c (#) f2)) `| Z) . x) / (( cos . ((a + (b * x)) + (c * (x ^2 )))) ^2 )) by A5, A12, A13, FDIFF_1:def 7

        .= ((b + ((2 * c) * x)) / (( cos . ((a + (b * x)) + (c * (x ^2 )))) ^2 )) by A2, A3, A4, A12, FDIFF_4: 12;

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

      end;

      hence thesis by A1, A8, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:11

    Z c= ( dom ( cot * (f1 + (c (#) f2)))) & f2 = ( #Z 2) & (for x st x in Z holds (f1 . x) = (a + (b * x))) implies ( cot * (f1 + (c (#) f2))) is_differentiable_on Z & for x st x in Z holds ((( cot * (f1 + (c (#) f2))) `| Z) . x) = ( - ((b + ((2 * c) * x)) / (( sin . ((a + (b * x)) + (c * (x ^2 )))) ^2 )))

    proof

      assume that

       A1: Z c= ( dom ( cot * (f1 + (c (#) f2)))) and

       A2: f2 = ( #Z 2) and

       A3: for x st x in Z holds (f1 . x) = (a + (b * x));

      ( dom ( cot * (f1 + (c (#) f2)))) c= ( dom (f1 + (c (#) f2))) by RELAT_1: 25;

      then

       A4: Z c= ( dom (f1 + (c (#) f2))) by A1, XBOOLE_1: 1;

      then

       A5: (f1 + (c (#) f2)) is_differentiable_on Z by A2, A3, FDIFF_4: 12;

      Z c= (( dom f1) /\ ( dom (c (#) f2))) by A4, VALUED_1:def 1;

      then

       A6: Z c= ( dom (c (#) f2)) by XBOOLE_1: 18;

      

       A7: for x st x in Z holds ( sin . ((f1 + (c (#) f2)) . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ((f1 + (c (#) f2)) . x) in ( dom ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by Th2;

      end;

      

       A8: for x st x in Z holds ( cot * (f1 + (c (#) f2))) is_differentiable_in x

      proof

        let x;

        assume

         A9: x in Z;

        then ( sin . ((f1 + (c (#) f2)) . x)) <> 0 by A7;

        then

         A10: cot is_differentiable_in ((f1 + (c (#) f2)) . x) by FDIFF_7: 47;

        (f1 + (c (#) f2)) is_differentiable_in x by A5, A9, FDIFF_1: 9;

        hence thesis by A10, FDIFF_2: 13;

      end;

      then

       A11: ( cot * (f1 + (c (#) f2))) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cot * (f1 + (c (#) f2))) `| Z) . x) = ( - ((b + ((2 * c) * x)) / (( sin . ((a + (b * x)) + (c * (x ^2 )))) ^2 )))

      proof

        let x;

        assume

         A12: x in Z;

        

        then

         A13: ((f1 + (c (#) f2)) . x) = ((f1 . x) + ((c (#) f2) . x)) by A4, VALUED_1:def 1

        .= ((f1 . x) + (c * (f2 . x))) by A6, A12, VALUED_1:def 5

        .= ((a + (b * x)) + (c * (f2 . x))) by A3, A12

        .= ((a + (b * x)) + (c * (x #Z 2))) by A2, TAYLOR_1:def 1

        .= ((a + (b * x)) + (c * (x |^ 2))) by PREPOWER: 36

        .= ((a + (b * x)) + (c * (x ^2 ))) by NEWTON: 81;

        

         A14: (f1 + (c (#) f2)) is_differentiable_in x by A5, A12, FDIFF_1: 9;

        

         A15: ( sin . ((f1 + (c (#) f2)) . x)) <> 0 by A7, A12;

        then cot is_differentiable_in ((f1 + (c (#) f2)) . x) by FDIFF_7: 47;

        

        then ( diff (( cot * (f1 + (c (#) f2))),x)) = (( diff ( cot ,((f1 + (c (#) f2)) . x))) * ( diff ((f1 + (c (#) f2)),x))) by A14, FDIFF_2: 13

        .= (( - (1 / (( sin . ((f1 + (c (#) f2)) . x)) ^2 ))) * ( diff ((f1 + (c (#) f2)),x))) by A15, FDIFF_7: 47

        .= ( - (( diff ((f1 + (c (#) f2)),x)) / (( sin . ((a + (b * x)) + (c * (x ^2 )))) ^2 ))) by A13

        .= ( - ((((f1 + (c (#) f2)) `| Z) . x) / (( sin . ((a + (b * x)) + (c * (x ^2 )))) ^2 ))) by A5, A12, FDIFF_1:def 7

        .= ( - ((b + ((2 * c) * x)) / (( sin . ((a + (b * x)) + (c * (x ^2 )))) ^2 ))) by A2, A3, A4, A12, FDIFF_4: 12;

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

      end;

      hence thesis by A1, A8, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:12

    Z c= ( dom ( tan * exp_R )) implies ( tan * exp_R ) is_differentiable_on Z & for x st x in Z holds ((( tan * exp_R ) `| Z) . x) = (( exp_R . x) / (( cos . ( exp_R . x)) ^2 ))

    proof

      assume

       A1: Z c= ( dom ( tan * exp_R ));

      

       A2: for x st x in Z holds ( cos . ( exp_R . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ( exp_R . x) in ( dom ( sin / cos )) by A1, FUNCT_1: 11;

        hence thesis by Th1;

      end;

      

       A3: for x st x in Z holds ( tan * exp_R ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . ( exp_R . x)) <> 0 by A2;

        then exp_R is_differentiable_in x & tan is_differentiable_in ( exp_R . x) by FDIFF_7: 46, SIN_COS: 65;

        hence thesis by FDIFF_2: 13;

      end;

      then

       A4: ( tan * exp_R ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( tan * exp_R ) `| Z) . x) = (( exp_R . x) / (( cos . ( exp_R . x)) ^2 ))

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( cos . ( exp_R . x)) <> 0 by A2;

        then exp_R is_differentiable_in x & tan is_differentiable_in ( exp_R . x) by FDIFF_7: 46, SIN_COS: 65;

        

        then ( diff (( tan * exp_R ),x)) = (( diff ( tan ,( exp_R . x))) * ( diff ( exp_R ,x))) by FDIFF_2: 13

        .= ((1 / (( cos . ( exp_R . x)) ^2 )) * ( diff ( exp_R ,x))) by A6, FDIFF_7: 46

        .= (( exp_R . x) / (( cos . ( exp_R . x)) ^2 )) by SIN_COS: 65;

        hence thesis by A4, A5, FDIFF_1:def 7;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:13

    Z c= ( dom ( cot * exp_R )) implies ( cot * exp_R ) is_differentiable_on Z & for x st x in Z holds ((( cot * exp_R ) `| Z) . x) = ( - (( exp_R . x) / (( sin . ( exp_R . x)) ^2 )))

    proof

      assume

       A1: Z c= ( dom ( cot * exp_R ));

      

       A2: for x st x in Z holds ( sin . ( exp_R . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ( exp_R . x) in ( dom ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by Th2;

      end;

      

       A3: for x st x in Z holds ( cot * exp_R ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . ( exp_R . x)) <> 0 by A2;

        then exp_R is_differentiable_in x & cot is_differentiable_in ( exp_R . x) by FDIFF_7: 47, SIN_COS: 65;

        hence thesis by FDIFF_2: 13;

      end;

      then

       A4: ( cot * exp_R ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( cot * exp_R ) `| Z) . x) = ( - (( exp_R . x) / (( sin . ( exp_R . x)) ^2 )))

      proof

        let x;

        assume

         A5: x in Z;

        then

         A6: ( sin . ( exp_R . x)) <> 0 by A2;

        then exp_R is_differentiable_in x & cot is_differentiable_in ( exp_R . x) by FDIFF_7: 47, SIN_COS: 65;

        

        then ( diff (( cot * exp_R ),x)) = (( diff ( cot ,( exp_R . x))) * ( diff ( exp_R ,x))) by FDIFF_2: 13

        .= (( - (1 / (( sin . ( exp_R . x)) ^2 ))) * ( diff ( exp_R ,x))) by A6, FDIFF_7: 47

        .= ( - (( diff ( exp_R ,x)) / (( sin . ( exp_R . x)) ^2 )))

        .= ( - (( exp_R . x) / (( sin . ( exp_R . x)) ^2 ))) by SIN_COS: 65;

        hence thesis by A4, A5, FDIFF_1:def 7;

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:14

    Z c= ( dom ( tan * ln )) implies ( tan * ln ) is_differentiable_on Z & for x st x in Z holds ((( tan * ln ) `| Z) . x) = (1 / (x * (( cos . ( ln . x)) ^2 )))

    proof

      assume

       A1: Z c= ( dom ( tan * ln ));

      ( dom ( tan * ln )) c= ( dom ln ) by RELAT_1: 25;

      then

       A2: Z c= ( dom ln ) by A1, XBOOLE_1: 1;

      

       A3: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A2, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by Lm1;

        hence thesis;

      end;

      

       A4: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A3;

        then x in ( right_open_halfline 0 ) by Lm1;

        hence thesis by TAYLOR_1: 18;

      end;

      

       A5: for x st x in Z holds ( cos . ( ln . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ( ln . x) in ( dom ( sin / cos )) by A1, FUNCT_1: 11;

        hence thesis by Th1;

      end;

      

       A6: for x st x in Z holds ( tan * ln ) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then ( cos . ( ln . x)) <> 0 by A5;

        then

         A8: tan is_differentiable_in ( ln . x) by FDIFF_7: 46;

         ln is_differentiable_in x by A3, A7, TAYLOR_1: 18;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( tan * ln ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: ln is_differentiable_in x by A3, TAYLOR_1: 18;

        

         A12: ( cos . ( ln . x)) <> 0 by A5, A10;

        then tan is_differentiable_in ( ln . x) by FDIFF_7: 46;

        

        then ( diff (( tan * ln ),x)) = (( diff ( tan ,( ln . x))) * ( diff ( ln ,x))) by A11, FDIFF_2: 13

        .= ((1 / (( cos . ( ln . x)) ^2 )) * ( diff ( ln ,x))) by A12, FDIFF_7: 46

        .= ((1 / x) / (( cos . ( ln . x)) ^2 )) by A4, A10

        .= (1 / (x * (( cos . ( ln . x)) ^2 ))) by XCMPLX_1: 78;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:15

    Z c= ( dom ( cot * ln )) implies ( cot * ln ) is_differentiable_on Z & for x st x in Z holds ((( cot * ln ) `| Z) . x) = ( - (1 / (x * (( sin . ( ln . x)) ^2 ))))

    proof

      assume

       A1: Z c= ( dom ( cot * ln ));

      ( dom ( cot * ln )) c= ( dom ln ) by RELAT_1: 25;

      then

       A2: Z c= ( dom ln ) by A1, XBOOLE_1: 1;

      

       A3: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A2, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by Lm1;

        hence thesis;

      end;

      

       A4: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A3;

        then x in ( right_open_halfline 0 ) by Lm1;

        hence thesis by TAYLOR_1: 18;

      end;

      

       A5: for x st x in Z holds ( sin . ( ln . x)) <> 0

      proof

        let x;

        assume x in Z;

        then ( ln . x) in ( dom ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by Th2;

      end;

      

       A6: for x st x in Z holds ( cot * ln ) is_differentiable_in x

      proof

        let x;

        assume

         A7: x in Z;

        then ( sin . ( ln . x)) <> 0 by A5;

        then

         A8: cot is_differentiable_in ( ln . x) by FDIFF_7: 47;

         ln is_differentiable_in x by A3, A7, TAYLOR_1: 18;

        hence thesis by A8, FDIFF_2: 13;

      end;

      then

       A9: ( cot * ln ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: ln is_differentiable_in x by A3, TAYLOR_1: 18;

        

         A12: ( sin . ( ln . x)) <> 0 by A5, A10;

        then cot is_differentiable_in ( ln . x) by FDIFF_7: 47;

        

        then ( diff (( cot * ln ),x)) = (( diff ( cot ,( ln . x))) * ( diff ( ln ,x))) by A11, FDIFF_2: 13

        .= (( - (1 / (( sin . ( ln . x)) ^2 ))) * ( diff ( ln ,x))) by A12, FDIFF_7: 47

        .= ( - (( diff ( ln ,x)) / (( sin . ( ln . x)) ^2 )))

        .= ( - ((1 / x) / (( sin . ( ln . x)) ^2 ))) by A4, A10

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

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:16

    Z c= ( dom ( exp_R * tan )) implies ( exp_R * tan ) is_differentiable_on Z & for x st x in Z holds ((( exp_R * tan ) `| Z) . x) = (( exp_R . ( tan . x)) / (( cos . x) ^2 ))

    proof

      assume

       A1: Z c= ( dom ( exp_R * tan ));

      

       A2: for x st x in Z holds ( cos . x) <> 0

      proof

        let x;

        assume x in Z;

        then x in ( dom ( sin / cos )) by A1, FUNCT_1: 11;

        hence thesis by Th1;

      end;

      

       A3: for x st x in Z holds ( exp_R * tan ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A2;

        then

         A4: tan is_differentiable_in x by FDIFF_7: 46;

         exp_R is_differentiable_in ( tan . x) by SIN_COS: 65;

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( exp_R * tan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R * tan ) `| Z) . x) = (( exp_R . ( tan . x)) / (( cos . x) ^2 ))

      proof

        let x;

        

         A6: exp_R is_differentiable_in ( tan . x) by SIN_COS: 65;

        assume

         A7: x in Z;

        then

         A8: ( cos . x) <> 0 by A2;

        then tan is_differentiable_in x by FDIFF_7: 46;

        

        then ( diff (( exp_R * tan ),x)) = (( diff ( exp_R ,( tan . x))) * ( diff ( tan ,x))) by A6, FDIFF_2: 13

        .= (( diff ( exp_R ,( tan . x))) * (1 / (( cos . x) ^2 ))) by A8, FDIFF_7: 46

        .= (( exp_R . ( tan . x)) / (( cos . x) ^2 )) by SIN_COS: 65;

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:17

    Z c= ( dom ( exp_R * cot )) implies ( exp_R * cot ) is_differentiable_on Z & for x st x in Z holds ((( exp_R * cot ) `| Z) . x) = ( - (( exp_R . ( cot . x)) / (( sin . x) ^2 )))

    proof

      assume

       A1: Z c= ( dom ( exp_R * cot ));

      

       A2: for x st x in Z holds ( sin . x) <> 0

      proof

        let x;

        assume x in Z;

        then x in ( dom ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by Th2;

      end;

      

       A3: for x st x in Z holds ( exp_R * cot ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A2;

        then

         A4: cot is_differentiable_in x by FDIFF_7: 47;

         exp_R is_differentiable_in ( cot . x) by SIN_COS: 65;

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( exp_R * cot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R * cot ) `| Z) . x) = ( - (( exp_R . ( cot . x)) / (( sin . x) ^2 )))

      proof

        let x;

        

         A6: exp_R is_differentiable_in ( cot . x) by SIN_COS: 65;

        assume

         A7: x in Z;

        then

         A8: ( sin . x) <> 0 by A2;

        then cot is_differentiable_in x by FDIFF_7: 47;

        

        then ( diff (( exp_R * cot ),x)) = (( diff ( exp_R ,( cot . x))) * ( diff ( cot ,x))) by A6, FDIFF_2: 13

        .= (( diff ( exp_R ,( cot . x))) * ( - (1 / (( sin . x) ^2 )))) by A8, FDIFF_7: 47

        .= (( exp_R . ( cot . x)) * ( - (1 / (( sin . x) ^2 )))) by SIN_COS: 65

        .= ( - (( exp_R . ( cot . x)) / (( sin . x) ^2 )));

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:18

    Z c= ( dom ( ln * tan )) implies ( ln * tan ) is_differentiable_on Z & for x st x in Z holds ((( ln * tan ) `| Z) . x) = (1 / (( cos . x) * ( sin . x)))

    proof

      assume

       A1: Z c= ( dom ( ln * tan ));

      

       A2: for x st x in Z holds ( tan . x) > 0

      proof

        let x;

        assume x in Z;

        then ( tan . x) in ( right_open_halfline 0 ) by A1, FUNCT_1: 11, TAYLOR_1: 18;

        then ex g be Real st ( tan . x) = g & 0 < g by Lm1;

        hence thesis;

      end;

      ( dom ( ln * tan )) c= ( dom tan ) by RELAT_1: 25;

      then

       A3: Z c= ( dom tan ) by A1, XBOOLE_1: 1;

      

       A4: for x st x in Z holds ( cos . x) <> 0

      proof

        let x;

        assume x in Z;

        then x in ( dom ( sin / cos )) by A1, FUNCT_1: 11;

        hence thesis by Th1;

      end;

      

       A5: for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4;

        hence thesis by FDIFF_7: 46;

      end;

      

       A6: for x st x in Z holds ( ln * tan ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then tan is_differentiable_in x & ( tan . x) > 0 by A2, A5;

        hence thesis by TAYLOR_1: 20;

      end;

      then

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

      for x st x in Z holds ((( ln * tan ) `| Z) . x) = (1 / (( cos . x) * ( sin . x)))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( cos . x) <> 0 by A4;

         tan is_differentiable_in x & ( tan . x) > 0 by A2, A5, A8;

        

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

        .= ((1 / (( cos . x) ^2 )) / ( tan . x)) by A9, FDIFF_7: 46

        .= (1 / ((( cos . x) ^2 ) * ( tan . x))) by XCMPLX_1: 78

        .= (1 / ((( cos . x) ^2 ) * (( sin . x) / ( cos . x)))) by A3, A8, RFUNCT_1:def 1

        .= (1 / (((( cos . x) ^2 ) * ( sin . x)) / ( cos . x)))

        .= (( cos . x) / ((( cos . x) ^2 ) * ( sin . x))) by XCMPLX_1: 57

        .= ((( cos . x) / (( cos . x) ^2 )) / ( sin . x)) by XCMPLX_1: 78

        .= (((( cos . x) / ( cos . x)) / ( cos . x)) / ( sin . x)) by XCMPLX_1: 78

        .= ((1 / ( cos . x)) / ( sin . x)) by A4, A8, XCMPLX_1: 60

        .= (1 / (( cos . x) * ( sin . x))) by XCMPLX_1: 78;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:19

    Z c= ( dom ( ln * cot )) implies ( ln * cot ) is_differentiable_on Z & for x st x in Z holds ((( ln * cot ) `| Z) . x) = ( - (1 / (( sin . x) * ( cos . x))))

    proof

      assume

       A1: Z c= ( dom ( ln * cot ));

      

       A2: for x st x in Z holds ( cot . x) > 0

      proof

        let x;

        assume x in Z;

        then ( cot . x) in ( right_open_halfline 0 ) by A1, FUNCT_1: 11, TAYLOR_1: 18;

        then ex g be Real st ( cot . x) = g & 0 < g by Lm1;

        hence thesis;

      end;

      ( dom ( ln * cot )) c= ( dom cot ) by RELAT_1: 25;

      then

       A3: Z c= ( dom cot ) by A1, XBOOLE_1: 1;

      

       A4: for x st x in Z holds ( sin . x) <> 0

      proof

        let x;

        assume x in Z;

        then x in ( dom ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by Th2;

      end;

      

       A5: for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A4;

        hence thesis by FDIFF_7: 47;

      end;

      

       A6: for x st x in Z holds ( ln * cot ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then cot is_differentiable_in x & ( cot . x) > 0 by A2, A5;

        hence thesis by TAYLOR_1: 20;

      end;

      then

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

      for x st x in Z holds ((( ln * cot ) `| Z) . x) = ( - (1 / (( sin . x) * ( cos . x))))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( sin . x) <> 0 by A4;

         cot is_differentiable_in x & ( cot . x) > 0 by A2, A5, A8;

        

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

        .= (( - (1 / (( sin . x) ^2 ))) / ( cot . x)) by A9, FDIFF_7: 47

        .= ( - ((1 / (( sin . x) ^2 )) / ( cot . x)))

        .= ( - (1 / ((( sin . x) ^2 ) * ( cot . x)))) by XCMPLX_1: 78

        .= ( - (1 / ((( sin . x) ^2 ) * (( cos . x) / ( sin . x))))) by A3, A8, RFUNCT_1:def 1

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

        .= ( - (( sin . x) / ((( sin . x) ^2 ) * ( cos . x)))) by XCMPLX_1: 57

        .= ( - ((( sin . x) / (( sin . x) ^2 )) / ( cos . x))) by XCMPLX_1: 78

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

        .= ( - ((1 / ( sin . x)) / ( cos . x))) by A4, A8, XCMPLX_1: 60

        .= ( - (1 / (( sin . x) * ( cos . x)))) by XCMPLX_1: 78;

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

      end;

      hence thesis by A1, A6, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:20

    Z c= ( dom (( #Z n) * tan )) & 1 <= n implies (( #Z n) * tan ) is_differentiable_on Z & for x st x in Z holds (((( #Z n) * tan ) `| Z) . x) = ((n * (( sin . x) #Z (n - 1))) / (( cos . x) #Z (n + 1)))

    proof

      assume that

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

       A2: 1 <= n;

      

       A3: ( dom (( #Z n) * tan )) c= ( dom tan ) by RELAT_1: 25;

      

       A4: for x st x in Z holds ( cos . x) <> 0

      proof

        let x;

        assume x in Z;

        then x in ( dom ( sin / cos )) by A1, FUNCT_1: 11;

        hence thesis by Th1;

      end;

      

       A5: for x st x in Z holds (( #Z n) * tan ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4;

        then tan is_differentiable_in x by FDIFF_7: 46;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A6: (( #Z n) * tan ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #Z n) * tan ) `| Z) . x) = ((n * (( sin . x) #Z (n - 1))) / (( cos . x) #Z (n + 1)))

      proof

        set m = (n - 1);

        let x;

        

         A7: ex m be Nat st n = (m + 1) by A2, NAT_1: 6;

        assume

         A8: x in Z;

        then

         A9: ( cos . x) <> 0 by A4;

        then

         A10: tan is_differentiable_in x by FDIFF_7: 46;

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

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

        .= ((n * (( tan . x) #Z (n - 1))) * (1 / (( cos . x) ^2 ))) by A9, FDIFF_7: 46

        .= ((n * ((( sin . x) #Z m) / (( cos . x) #Z m))) / (( cos . x) ^2 )) by A1, A3, A8, A7, Th3, XBOOLE_1: 1

        .= (((n * (( sin . x) #Z (n - 1))) / (( cos . x) #Z (n - 1))) / (( cos . x) ^2 ))

        .= ((n * (( sin . x) #Z (n - 1))) / ((( cos . x) #Z (n - 1)) * (( cos . x) ^2 ))) by XCMPLX_1: 78

        .= ((n * (( sin . x) #Z (n - 1))) / ((( cos . x) #Z (n - 1)) * (( cos . x) #Z 2))) by FDIFF_7: 1

        .= ((n * (( sin . x) #Z (n - 1))) / (( cos . x) #Z ((n - 1) + 2))) by A4, A8, PREPOWER: 44

        .= ((n * (( sin . x) #Z (n - 1))) / (( cos . x) #Z (n + 1)));

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:21

    Z c= ( dom (( #Z n) * cot )) & 1 <= n implies (( #Z n) * cot ) is_differentiable_on Z & for x st x in Z holds (((( #Z n) * cot ) `| Z) . x) = ( - ((n * (( cos . x) #Z (n - 1))) / (( sin . x) #Z (n + 1))))

    proof

      assume that

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

       A2: 1 <= n;

      

       A3: ( dom (( #Z n) * cot )) c= ( dom cot ) by RELAT_1: 25;

      

       A4: for x st x in Z holds ( sin . x) <> 0

      proof

        let x;

        assume x in Z;

        then x in ( dom ( cos / sin )) by A1, FUNCT_1: 11;

        hence thesis by Th2;

      end;

      

       A5: for x st x in Z holds (( #Z n) * cot ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A4;

        then cot is_differentiable_in x by FDIFF_7: 47;

        hence thesis by TAYLOR_1: 3;

      end;

      then

       A6: (( #Z n) * cot ) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (((( #Z n) * cot ) `| Z) . x) = ( - ((n * (( cos . x) #Z (n - 1))) / (( sin . x) #Z (n + 1))))

      proof

        set m = (n - 1);

        let x;

        

         A7: ex m be Nat st n = (m + 1) by A2, NAT_1: 6;

        assume

         A8: x in Z;

        then

         A9: ( sin . x) <> 0 by A4;

        then

         A10: cot is_differentiable_in x by FDIFF_7: 47;

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

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

        .= ((n * (( cot . x) #Z (n - 1))) * ( - (1 / (( sin . x) ^2 )))) by A9, FDIFF_7: 47

        .= ( - ((n * (( cot . x) #Z (n - 1))) / (( sin . x) ^2 )))

        .= ( - ((n * ((( cos . x) #Z m) / (( sin . x) #Z m))) / (( sin . x) ^2 ))) by A1, A3, A8, A7, Th3, XBOOLE_1: 1

        .= ( - (((n * (( cos . x) #Z (n - 1))) / (( sin . x) #Z (n - 1))) / (( sin . x) ^2 )))

        .= ( - ((n * (( cos . x) #Z (n - 1))) / ((( sin . x) #Z (n - 1)) * (( sin . x) ^2 )))) by XCMPLX_1: 78

        .= ( - ((n * (( cos . x) #Z (n - 1))) / ((( sin . x) #Z (n - 1)) * (( sin . x) #Z 2)))) by FDIFF_7: 1

        .= ( - ((n * (( cos . x) #Z (n - 1))) / (( sin . x) #Z ((n - 1) + 2)))) by A4, A8, PREPOWER: 44

        .= ( - ((n * (( cos . x) #Z (n - 1))) / (( sin . x) #Z (n + 1))));

        hence thesis;

      end;

      hence thesis by A1, A5, FDIFF_1: 9;

    end;

    theorem :: FDIFF_8:22

    (Z c= ( dom ( tan + ( cos ^ ))) & for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 ) implies ( tan + ( cos ^ )) is_differentiable_on Z & for x st x in Z holds ((( tan + ( cos ^ )) `| Z) . x) = (1 / (1 - ( sin . x)))

    proof

      assume that

       A1: Z c= ( dom ( tan + ( cos ^ ))) and

       A2: for x st x in Z holds (1 + ( sin . x)) <> 0 & (1 - ( sin . x)) <> 0 ;

      Z c= (( dom tan ) /\ ( dom ( cos ^ ))) by A1, VALUED_1:def 1;

      then

       A3: Z c= ( dom tan ) by XBOOLE_1: 18;

      then

       A4: for x st x in Z holds ( cos . x) <> 0 by Th1;

      then

       A5: ( cos ^ ) is_differentiable_on Z by FDIFF_4: 39;

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A3, Th1;

        hence thesis by FDIFF_7: 46;

      end;

      then

       A6: tan is_differentiable_on Z by A3, FDIFF_1: 9;

      for x st x in Z holds ((( tan + ( cos ^ )) `| Z) . x) = (1 / (1 - ( sin . x)))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: (1 + ( sin . x)) <> 0 by A2;

        

         A9: ( cos . x) <> 0 by A3, A7, Th1;

        ((( tan + ( cos ^ )) `| Z) . x) = (( diff ( tan ,x)) + ( diff (( cos ^ ),x))) by A1, A5, A6, A7, FDIFF_1: 18

        .= ((1 / (( cos . x) ^2 )) + ( diff (( cos ^ ),x))) by A9, FDIFF_7: 46

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

        .= ((1 / (( cos . x) ^2 )) + (( sin . x) / (( cos . x) ^2 ))) by A4, A7, FDIFF_4: 39

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

        .= ((1 + ( sin . x)) / (1 - (( sin . x) ^2 ))) by SIN_COS: 28

        .= ((1 + ( sin . x)) / ((1 + ( sin . x)) * (1 - ( sin . x))))

        .= (((1 + ( sin . x)) / (1 + ( sin . x))) / (1 - ( sin . x))) by XCMPLX_1: 78

        .= (1 / (1 - ( sin . x))) by A8, XCMPLX_1: 60;

        hence thesis;

      end;

      hence thesis by A1, A5, A6, FDIFF_1: 18;

    end;

    theorem :: FDIFF_8:23

    (Z c= ( dom ( tan - ( cos ^ ))) & for x st x in Z holds (1 - ( sin . x)) <> 0 & (1 + ( sin . x)) <> 0 ) implies ( tan - ( cos ^ )) is_differentiable_on Z & for x st x in Z holds ((( tan - ( cos ^ )) `| Z) . x) = (1 / (1 + ( sin . x)))

    proof

      assume that

       A1: Z c= ( dom ( tan - ( cos ^ ))) and

       A2: for x st x in Z holds (1 - ( sin . x)) <> 0 & (1 + ( sin . x)) <> 0 ;

      Z c= (( dom tan ) /\ ( dom ( cos ^ ))) by A1, VALUED_1: 12;

      then

       A3: Z c= ( dom tan ) by XBOOLE_1: 18;

      then

       A4: for x st x in Z holds ( cos . x) <> 0 by Th1;

      then

       A5: ( cos ^ ) is_differentiable_on Z by FDIFF_4: 39;

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A3, Th1;

        hence thesis by FDIFF_7: 46;

      end;

      then

       A6: tan is_differentiable_on Z by A3, FDIFF_1: 9;

      for x st x in Z holds ((( tan - ( cos ^ )) `| Z) . x) = (1 / (1 + ( sin . x)))

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: (1 - ( sin . x)) <> 0 by A2;

        

         A9: ( cos . x) <> 0 by A3, A7, Th1;

        ((( tan - ( cos ^ )) `| Z) . x) = (( diff ( tan ,x)) - ( diff (( cos ^ ),x))) by A1, A5, A6, A7, FDIFF_1: 19

        .= ((1 / (( cos . x) ^2 )) - ( diff (( cos ^ ),x))) by A9, FDIFF_7: 46

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

        .= ((1 / (( cos . x) ^2 )) - (( sin . x) / (( cos . x) ^2 ))) by A4, A7, FDIFF_4: 39

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

        .= ((1 - ( sin . x)) / (1 - (( sin . x) ^2 ))) by SIN_COS: 28

        .= ((1 - ( sin . x)) / ((1 - ( sin . x)) * (1 + ( sin . x))))

        .= (((1 - ( sin . x)) / (1 - ( sin . x))) / (1 + ( sin . x))) by XCMPLX_1: 78

        .= (1 / (1 + ( sin . x))) by A8, XCMPLX_1: 60;

        hence thesis;

      end;

      hence thesis by A1, A5, A6, FDIFF_1: 19;

    end;

    theorem :: FDIFF_8:24

    Z c= ( dom ( tan - ( id Z))) implies ( tan - ( id Z)) is_differentiable_on Z & for x st x in Z holds ((( tan - ( id Z)) `| Z) . x) = ((( sin . x) ^2 ) / (( cos . x) ^2 ))

    proof

      

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

      assume

       A2: Z c= ( dom ( tan - ( id Z)));

      then

       A3: Z c= (( dom tan ) /\ ( dom ( id Z))) by VALUED_1: 12;

      then

       A4: Z c= ( dom tan ) by XBOOLE_1: 18;

      

       A5: Z c= ( dom ( id Z)) by A3, XBOOLE_1: 18;

      then

       A6: ( id Z) is_differentiable_on Z by A1, FDIFF_1: 23;

      for x st x in Z holds tan is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4, Th1;

        hence thesis by FDIFF_7: 46;

      end;

      then

       A7: tan is_differentiable_on Z by A4, FDIFF_1: 9;

      for x st x in Z holds ((( tan - ( id Z)) `| Z) . x) = ((( sin . x) ^2 ) / (( cos . x) ^2 ))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: ( cos . x) <> 0 by A4, Th1;

        then

         A10: (( cos . x) ^2 ) > 0 by SQUARE_1: 12;

        ((( tan - ( id Z)) `| Z) . x) = (( diff ( tan ,x)) - ( diff (( id Z),x))) by A2, A6, A7, A8, FDIFF_1: 19

        .= ((1 / (( cos . x) ^2 )) - ( diff (( id Z),x))) by A9, FDIFF_7: 46

        .= ((1 / (( cos . x) ^2 )) - ((( id Z) `| Z) . x)) by A6, A8, FDIFF_1:def 7

        .= ((1 / (( cos . x) ^2 )) - 1) by A5, A1, A8, FDIFF_1: 23

        .= ((1 / (( cos . x) ^2 )) - ((( cos . x) ^2 ) / (( cos . x) ^2 ))) by A10, XCMPLX_1: 60

        .= ((1 - (( cos . x) ^2 )) / (( cos . x) ^2 ))

        .= ((((( sin . x) ^2 ) + (( cos . x) ^2 )) - (( cos . x) ^2 )) / (( cos . x) ^2 )) by SIN_COS: 28

        .= ((( sin . x) ^2 ) / (( cos . x) ^2 ));

        hence thesis;

      end;

      hence thesis by A2, A6, A7, FDIFF_1: 19;

    end;

    theorem :: FDIFF_8:25

    Z c= ( dom (( - cot ) - ( id Z))) implies (( - cot ) - ( id Z)) is_differentiable_on Z & for x st x in Z holds (((( - cot ) - ( id Z)) `| Z) . x) = ((( cos . x) ^2 ) / (( sin . x) ^2 ))

    proof

      set f = ( - cot );

      

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

      assume

       A2: Z c= ( dom (( - cot ) - ( id Z)));

      then

       A3: Z c= (( dom ( - cot )) /\ ( dom ( id Z))) by VALUED_1: 12;

      then

       A4: Z c= ( dom ( - cot )) by XBOOLE_1: 18;

      then

       A5: Z c= ( dom cot ) by VALUED_1: 8;

      for x st x in Z holds cot is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A5, Th2;

        hence thesis by FDIFF_7: 47;

      end;

      then

       A6: cot is_differentiable_on Z by A5, FDIFF_1: 9;

      then

       A7: (( - 1) (#) cot ) is_differentiable_on Z by A4, FDIFF_1: 20;

      

       A8: Z c= ( dom ( id Z)) by A3, XBOOLE_1: 18;

      then

       A9: ( id Z) is_differentiable_on Z by A1, FDIFF_1: 23;

      for x st x in Z holds (((( - cot ) - ( id Z)) `| Z) . x) = ((( cos . x) ^2 ) / (( sin . x) ^2 ))

      proof

        let x;

        assume

         A10: x in Z;

        then

         A11: ( sin . x) <> 0 by A5, Th2;

        then

         A12: (( sin . x) ^2 ) > 0 by SQUARE_1: 12;

        (((f - ( id Z)) `| Z) . x) = (( diff (f,x)) - ( diff (( id Z),x))) by A2, A9, A7, A10, FDIFF_1: 19

        .= ((((( - 1) (#) cot ) `| Z) . x) - ( diff (( id Z),x))) by A7, A10, FDIFF_1:def 7

        .= ((( - 1) * ( diff ( cot ,x))) - ( diff (( id Z),x))) by A4, A6, A10, FDIFF_1: 20

        .= ((( - 1) * ( - (1 / (( sin . x) ^2 )))) - ( diff (( id Z),x))) by A11, FDIFF_7: 47

        .= ((1 / (( sin . x) ^2 )) - ((( id Z) `| Z) . x)) by A9, A10, FDIFF_1:def 7

        .= ((1 / (( sin . x) ^2 )) - 1) by A8, A1, A10, FDIFF_1: 23

        .= ((1 / (( sin . x) ^2 )) - ((( sin . x) ^2 ) / (( sin . x) ^2 ))) by A12, XCMPLX_1: 60

        .= ((1 - (( sin . x) ^2 )) / (( sin . x) ^2 ))

        .= ((((( cos . x) ^2 ) + (( sin . x) ^2 )) - (( sin . x) ^2 )) / (( sin . x) ^2 )) by SIN_COS: 28

        .= ((( cos . x) ^2 ) / (( sin . x) ^2 ));

        hence thesis;

      end;

      hence thesis by A2, A9, A7, FDIFF_1: 19;

    end;

    theorem :: FDIFF_8:26

    (Z c= ( dom (((1 / a) (#) ( tan * f)) - ( id Z))) & for x st x in Z holds (f . x) = (a * x) & a <> 0 ) implies (((1 / a) (#) ( tan * f)) - ( id Z)) is_differentiable_on Z & for x st x in Z holds (((((1 / a) (#) ( tan * f)) - ( id Z)) `| Z) . x) = ((( sin . (a * x)) ^2 ) / (( cos . (a * x)) ^2 ))

    proof

      assume that

       A1: Z c= ( dom (((1 / a) (#) ( tan * f)) - ( id Z))) and

       A2: for x st x in Z holds (f . x) = (a * x) & a <> 0 ;

      

       A3: Z c= (( dom ((1 / a) (#) ( tan * f))) /\ ( dom ( id Z))) by A1, VALUED_1: 12;

      then

       A4: Z c= ( dom ((1 / a) (#) ( tan * f))) by XBOOLE_1: 18;

      then

       A5: Z c= ( dom ( tan * f)) by VALUED_1:def 5;

      

       A6: for x st x in Z holds (f . x) = ((a * x) + 0 ) by A2;

      then

       A7: ( tan * f) is_differentiable_on Z by A5, Th6;

      then

       A8: ((1 / a) (#) ( tan * f)) is_differentiable_on Z by A4, FDIFF_1: 20;

      set g = ((1 / a) (#) ( tan * f));

      

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

      

       A10: Z c= ( dom ( id Z)) by A3, XBOOLE_1: 18;

      then

       A11: ( id Z) is_differentiable_on Z by A9, FDIFF_1: 23;

      

       A12: for x st x in Z holds ( cos . (f . x)) <> 0

      proof

        let x;

        assume x in Z;

        then (f . x) in ( dom ( sin / cos )) by A5, FUNCT_1: 11;

        hence thesis by Th1;

      end;

      for x st x in Z holds (((((1 / a) (#) ( tan * f)) - ( id Z)) `| Z) . x) = ((( sin . (a * x)) ^2 ) / (( cos . (a * x)) ^2 ))

      proof

        let x;

        assume

         A13: x in Z;

        then

         A14: (f . x) = ((a * x) + 0 ) by A2;

        ( cos . (f . x)) <> 0 by A12, A13;

        then

         A15: (( cos . (a * x)) ^2 ) > 0 by A14, SQUARE_1: 12;

        (((g - ( id Z)) `| Z) . x) = (( diff (g,x)) - ( diff (( id Z),x))) by A1, A8, A11, A13, FDIFF_1: 19

        .= (((g `| Z) . x) - ( diff (( id Z),x))) by A8, A13, FDIFF_1:def 7

        .= (((1 / a) * ( diff (( tan * f),x))) - ( diff (( id Z),x))) by A4, A7, A13, FDIFF_1: 20

        .= (((1 / a) * ((( tan * f) `| Z) . x)) - ( diff (( id Z),x))) by A7, A13, FDIFF_1:def 7

        .= (((1 / a) * ((( tan * f) `| Z) . x)) - ((( id Z) `| Z) . x)) by A11, A13, FDIFF_1:def 7

        .= (((1 / a) * (a / (( cos . (a * x)) ^2 ))) - ((( id Z) `| Z) . x)) by A5, A6, A13, A14, Th6

        .= (((1 / (( cos . (a * x)) ^2 )) * (a / a)) - 1) by A10, A9, A13, FDIFF_1: 23

        .= (((1 / (( cos . (a * x)) ^2 )) * 1) - 1) by A2, A13, XCMPLX_1: 60

        .= ((1 / (( cos . (a * x)) ^2 )) - ((( cos . (a * x)) ^2 ) / (( cos . (a * x)) ^2 ))) by A15, XCMPLX_1: 60

        .= ((1 - (( cos . (a * x)) ^2 )) / (( cos . (a * x)) ^2 ))

        .= ((((( sin . (a * x)) ^2 ) + (( cos . (a * x)) ^2 )) - (( cos . (a * x)) ^2 )) / (( cos . (a * x)) ^2 )) by SIN_COS: 28

        .= ((( sin . (a * x)) ^2 ) / (( cos . (a * x)) ^2 ));

        hence thesis;

      end;

      hence thesis by A1, A8, A11, FDIFF_1: 19;

    end;

    theorem :: FDIFF_8:27

    (Z c= ( dom ((( - (1 / a)) (#) ( cot * f)) - ( id Z))) & for x st x in Z holds (f . x) = (a * x) & a <> 0 ) implies ((( - (1 / a)) (#) ( cot * f)) - ( id Z)) is_differentiable_on Z & for x st x in Z holds ((((( - (1 / a)) (#) ( cot * f)) - ( id Z)) `| Z) . x) = ((( cos . (a * x)) ^2 ) / (( sin . (a * x)) ^2 ))

    proof

      assume that

       A1: Z c= ( dom ((( - (1 / a)) (#) ( cot * f)) - ( id Z))) and

       A2: for x st x in Z holds (f . x) = (a * x) & a <> 0 ;

      

       A3: Z c= (( dom (( - (1 / a)) (#) ( cot * f))) /\ ( dom ( id Z))) by A1, VALUED_1: 12;

      then

       A4: Z c= ( dom (( - (1 / a)) (#) ( cot * f))) by XBOOLE_1: 18;

      then

       A5: Z c= ( dom ( cot * f)) by VALUED_1:def 5;

      

       A6: for x st x in Z holds (f . x) = ((a * x) + 0 ) by A2;

      then

       A7: ( cot * f) is_differentiable_on Z by A5, Th7;

      then

       A8: (( - (1 / a)) (#) ( cot * f)) is_differentiable_on Z by A4, FDIFF_1: 20;

      set g = (( - (1 / a)) (#) ( cot * f));

      

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

      

       A10: Z c= ( dom ( id Z)) by A3, XBOOLE_1: 18;

      then

       A11: ( id Z) is_differentiable_on Z by A9, FDIFF_1: 23;

      

       A12: for x st x in Z holds ( sin . (f . x)) <> 0

      proof

        let x;

        assume x in Z;

        then (f . x) in ( dom ( cos / sin )) by A5, FUNCT_1: 11;

        hence thesis by Th2;

      end;

      for x st x in Z holds ((((( - (1 / a)) (#) ( cot * f)) - ( id Z)) `| Z) . x) = ((( cos . (a * x)) ^2 ) / (( sin . (a * x)) ^2 ))

      proof

        let x;

        assume

         A13: x in Z;

        then

         A14: (f . x) = ((a * x) + 0 ) by A2;

        ( sin . (f . x)) <> 0 by A12, A13;

        then

         A15: (( sin . (a * x)) ^2 ) > 0 by A14, SQUARE_1: 12;

        (((g - ( id Z)) `| Z) . x) = (( diff (g,x)) - ( diff (( id Z),x))) by A1, A8, A11, A13, FDIFF_1: 19

        .= (((g `| Z) . x) - ( diff (( id Z),x))) by A8, A13, FDIFF_1:def 7

        .= ((( - (1 / a)) * ( diff (( cot * f),x))) - ( diff (( id Z),x))) by A4, A7, A13, FDIFF_1: 20

        .= ((( - (1 / a)) * ((( cot * f) `| Z) . x)) - ( diff (( id Z),x))) by A7, A13, FDIFF_1:def 7

        .= ((( - (1 / a)) * ((( cot * f) `| Z) . x)) - ((( id Z) `| Z) . x)) by A11, A13, FDIFF_1:def 7

        .= ((( - (1 / a)) * ( - (a / (( sin . (a * x)) ^2 )))) - ((( id Z) `| Z) . x)) by A5, A6, A13, A14, Th7

        .= (((1 / (( sin . (a * x)) ^2 )) * (a / a)) - 1) by A10, A9, A13, FDIFF_1: 23

        .= (((1 / (( sin . (a * x)) ^2 )) * 1) - 1) by A2, A13, XCMPLX_1: 60

        .= ((1 / (( sin . (a * x)) ^2 )) - ((( sin . (a * x)) ^2 ) / (( sin . (a * x)) ^2 ))) by A15, XCMPLX_1: 60

        .= ((1 - (( sin . (a * x)) ^2 )) / (( sin . (a * x)) ^2 ))

        .= ((((( cos . (a * x)) ^2 ) + (( sin . (a * x)) ^2 )) - (( sin . (a * x)) ^2 )) / (( sin . (a * x)) ^2 )) by SIN_COS: 28

        .= ((( cos . (a * x)) ^2 ) / (( sin . (a * x)) ^2 ));

        hence thesis;

      end;

      hence thesis by A1, A8, A11, FDIFF_1: 19;

    end;

    theorem :: FDIFF_8:28

    (Z c= ( dom (f (#) tan )) & for x st x in Z holds (f . x) = ((a * x) + b)) implies (f (#) tan ) is_differentiable_on Z & for x st x in Z holds (((f (#) tan ) `| Z) . x) = (((a * ( sin . x)) / ( cos . x)) + (((a * x) + b) / (( cos . x) ^2 )))

    proof

      assume that

       A1: Z c= ( dom (f (#) tan )) and

       A2: for x st x in Z holds (f . x) = ((a * x) + b);

      

       A3: Z c= (( dom f) /\ ( dom tan )) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom tan ) by XBOOLE_1: 18;

      

       A5: Z c= ( dom f) by A3, XBOOLE_1: 18;

      then

       A6: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A7: for x st x in Z holds tan is_differentiable_in x & ( diff ( tan ,x)) = (1 / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4, Th1;

        hence thesis by FDIFF_7: 46;

      end;

      then for x st x in Z holds tan is_differentiable_in x;

      then

       A8: tan is_differentiable_on Z by A4, FDIFF_1: 9;

      for x st x in Z holds (((f (#) tan ) `| Z) . x) = (((a * ( sin . x)) / ( cos . x)) + (((a * x) + b) / (( cos . x) ^2 )))

      proof

        let x;

        assume

         A9: x in Z;

        

        then (((f (#) tan ) `| Z) . x) = ((( tan . x) * ( diff (f,x))) + ((f . x) * ( diff ( tan ,x)))) by A1, A6, A8, FDIFF_1: 21

        .= ((( tan . x) * ((f `| Z) . x)) + ((f . x) * ( diff ( tan ,x)))) by A6, A9, FDIFF_1:def 7

        .= ((( tan . x) * a) + ((f . x) * ( diff ( tan ,x)))) by A2, A5, A9, FDIFF_1: 23

        .= ((( tan . x) * a) + (((a * x) + b) * ( diff ( tan ,x)))) by A2, A9

        .= ((( tan . x) * a) + (((a * x) + b) * (1 / (( cos . x) ^2 )))) by A7, A9

        .= (((( sin . x) / ( cos . x)) * (a / 1)) + (((a * x) + b) / (( cos . x) ^2 ))) by A4, A9, RFUNCT_1:def 1

        .= (((a * ( sin . x)) / ( cos . x)) + (((a * x) + b) / (( cos . x) ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A6, A8, FDIFF_1: 21;

    end;

    theorem :: FDIFF_8:29

    (Z c= ( dom (f (#) cot )) & for x st x in Z holds (f . x) = ((a * x) + b)) implies (f (#) cot ) is_differentiable_on Z & for x st x in Z holds (((f (#) cot ) `| Z) . x) = (((a * ( cos . x)) / ( sin . x)) - (((a * x) + b) / (( sin . x) ^2 )))

    proof

      assume that

       A1: Z c= ( dom (f (#) cot )) and

       A2: for x st x in Z holds (f . x) = ((a * x) + b);

      

       A3: Z c= (( dom f) /\ ( dom cot )) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom cot ) by XBOOLE_1: 18;

      

       A5: Z c= ( dom f) by A3, XBOOLE_1: 18;

      then

       A6: f is_differentiable_on Z by A2, FDIFF_1: 23;

      

       A7: for x st x in Z holds cot is_differentiable_in x & ( diff ( cot ,x)) = ( - (1 / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A4, Th2;

        hence thesis by FDIFF_7: 47;

      end;

      then for x st x in Z holds cot is_differentiable_in x;

      then

       A8: cot is_differentiable_on Z by A4, FDIFF_1: 9;

      for x st x in Z holds (((f (#) cot ) `| Z) . x) = (((a * ( cos . x)) / ( sin . x)) - (((a * x) + b) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A9: x in Z;

        

        then (((f (#) cot ) `| Z) . x) = ((( cot . x) * ( diff (f,x))) + ((f . x) * ( diff ( cot ,x)))) by A1, A6, A8, FDIFF_1: 21

        .= ((( cot . x) * ((f `| Z) . x)) + ((f . x) * ( diff ( cot ,x)))) by A6, A9, FDIFF_1:def 7

        .= ((( cot . x) * a) + ((f . x) * ( diff ( cot ,x)))) by A2, A5, A9, FDIFF_1: 23

        .= ((( cot . x) * a) + (((a * x) + b) * ( diff ( cot ,x)))) by A2, A9

        .= ((( cot . x) * a) + (((a * x) + b) * ( - (1 / (( sin . x) ^2 ))))) by A7, A9

        .= (((( cos . x) / ( sin . x)) * (a / 1)) - (((a * x) + b) / (( sin . x) ^2 ))) by A4, A9, RFUNCT_1:def 1

        .= (((a * ( cos . x)) / ( sin . x)) - (((a * x) + b) / (( sin . x) ^2 )));

        hence thesis;

      end;

      hence thesis by A1, A6, A8, FDIFF_1: 21;

    end;

    theorem :: FDIFF_8:30

    Z c= ( dom ( exp_R (#) tan )) implies ( exp_R (#) tan ) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) tan ) `| Z) . x) = (((( exp_R . x) * ( sin . x)) / ( cos . x)) + (( exp_R . x) / (( cos . x) ^2 )))

    proof

      

       A1: for x st x in Z holds exp_R is_differentiable_in x by SIN_COS: 65;

      assume

       A2: Z c= ( dom ( exp_R (#) tan ));

      then

       A3: Z c= (( dom exp_R ) /\ ( dom tan )) by VALUED_1:def 4;

      then

       A4: Z c= ( dom tan ) by XBOOLE_1: 18;

      Z c= ( dom exp_R ) by A3, XBOOLE_1: 18;

      then

       A5: exp_R is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A6: for x st x in Z holds tan is_differentiable_in x & ( diff ( tan ,x)) = (1 / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4, Th1;

        hence thesis by FDIFF_7: 46;

      end;

      then for x st x in Z holds tan is_differentiable_in x;

      then

       A7: tan is_differentiable_on Z by A4, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R (#) tan ) `| Z) . x) = (((( exp_R . x) * ( sin . x)) / ( cos . x)) + (( exp_R . x) / (( cos . x) ^2 )))

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( exp_R (#) tan ) `| Z) . x) = ((( tan . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff ( tan ,x)))) by A2, A5, A7, FDIFF_1: 21

        .= ((( tan . x) * ( exp_R . x)) + (( exp_R . x) * ( diff ( tan ,x)))) by SIN_COS: 65

        .= ((( tan . x) * ( exp_R . x)) + (( exp_R . x) * (1 / (( cos . x) ^2 )))) by A6, A8

        .= (((( sin . x) / ( cos . x)) * (( exp_R . x) / 1)) + (( exp_R . x) / (( cos . x) ^2 ))) by A4, A8, RFUNCT_1:def 1

        .= (((( exp_R . x) * ( sin . x)) / ( cos . x)) + (( exp_R . x) / (( cos . x) ^2 )));

        hence thesis;

      end;

      hence thesis by A2, A5, A7, FDIFF_1: 21;

    end;

    theorem :: FDIFF_8:31

    Z c= ( dom ( exp_R (#) cot )) implies ( exp_R (#) cot ) is_differentiable_on Z & for x st x in Z holds ((( exp_R (#) cot ) `| Z) . x) = (((( exp_R . x) * ( cos . x)) / ( sin . x)) - (( exp_R . x) / (( sin . x) ^2 )))

    proof

      

       A1: for x st x in Z holds exp_R is_differentiable_in x by SIN_COS: 65;

      assume

       A2: Z c= ( dom ( exp_R (#) cot ));

      then

       A3: Z c= (( dom exp_R ) /\ ( dom cot )) by VALUED_1:def 4;

      then

       A4: Z c= ( dom cot ) by XBOOLE_1: 18;

      Z c= ( dom exp_R ) by A3, XBOOLE_1: 18;

      then

       A5: exp_R is_differentiable_on Z by A1, FDIFF_1: 9;

      

       A6: for x st x in Z holds cot is_differentiable_in x & ( diff ( cot ,x)) = ( - (1 / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A4, Th2;

        hence thesis by FDIFF_7: 47;

      end;

      then for x st x in Z holds cot is_differentiable_in x;

      then

       A7: cot is_differentiable_on Z by A4, FDIFF_1: 9;

      for x st x in Z holds ((( exp_R (#) cot ) `| Z) . x) = (((( exp_R . x) * ( cos . x)) / ( sin . x)) - (( exp_R . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A8: x in Z;

        

        then ((( exp_R (#) cot ) `| Z) . x) = ((( cot . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff ( cot ,x)))) by A2, A5, A7, FDIFF_1: 21

        .= ((( cot . x) * ( exp_R . x)) + (( exp_R . x) * ( diff ( cot ,x)))) by SIN_COS: 65

        .= ((( cot . x) * ( exp_R . x)) + (( exp_R . x) * ( - (1 / (( sin . x) ^2 ))))) by A6, A8

        .= (((( cos . x) / ( sin . x)) * (( exp_R . x) / 1)) - (( exp_R . x) / (( sin . x) ^2 ))) by A4, A8, RFUNCT_1:def 1

        .= (((( exp_R . x) * ( cos . x)) / ( sin . x)) - (( exp_R . x) / (( sin . x) ^2 )));

        hence thesis;

      end;

      hence thesis by A2, A5, A7, FDIFF_1: 21;

    end;

    theorem :: FDIFF_8:32

    Z c= ( dom ( ln (#) tan )) implies ( ln (#) tan ) is_differentiable_on Z & for x st x in Z holds ((( ln (#) tan ) `| Z) . x) = (((( sin . x) / ( cos . x)) / x) + (( ln . x) / (( cos . x) ^2 )))

    proof

      assume

       A1: Z c= ( dom ( ln (#) tan ));

      then

       A2: Z c= (( dom ln ) /\ ( dom tan )) by VALUED_1:def 4;

      then

       A3: Z c= ( dom tan ) by XBOOLE_1: 18;

      

       A4: for x st x in Z holds tan is_differentiable_in x & ( diff ( tan ,x)) = (1 / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A3, Th1;

        hence thesis by FDIFF_7: 46;

      end;

      then for x st x in Z holds tan is_differentiable_in x;

      then

       A5: tan is_differentiable_on Z by A3, FDIFF_1: 9;

      

       A6: Z c= ( dom ln ) by A2, XBOOLE_1: 18;

      

       A7: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A6, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by Lm1;

        hence thesis;

      end;

      then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1: 18;

      then

       A8: ln is_differentiable_on Z by A6, FDIFF_1: 9;

      

       A9: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A7;

        then x in ( right_open_halfline 0 ) by Lm1;

        hence thesis by TAYLOR_1: 18;

      end;

      for x st x in Z holds ((( ln (#) tan ) `| Z) . x) = (((( sin . x) / ( cos . x)) / x) + (( ln . x) / (( cos . x) ^2 )))

      proof

        let x;

        assume

         A10: x in Z;

        

        then ((( ln (#) tan ) `| Z) . x) = ((( tan . x) * ( diff ( ln ,x))) + (( ln . x) * ( diff ( tan ,x)))) by A1, A8, A5, FDIFF_1: 21

        .= ((( tan . x) * (1 / x)) + (( ln . x) * ( diff ( tan ,x)))) by A9, A10

        .= ((( tan . x) * (1 / x)) + (( ln . x) * (1 / (( cos . x) ^2 )))) by A4, A10

        .= (((( sin . x) / ( cos . x)) / x) + (( ln . x) / (( cos . x) ^2 ))) by A3, A10, RFUNCT_1:def 1;

        hence thesis;

      end;

      hence thesis by A1, A8, A5, FDIFF_1: 21;

    end;

    theorem :: FDIFF_8:33

    Z c= ( dom ( ln (#) cot )) implies ( ln (#) cot ) is_differentiable_on Z & for x st x in Z holds ((( ln (#) cot ) `| Z) . x) = (((( cos . x) / ( sin . x)) / x) - (( ln . x) / (( sin . x) ^2 )))

    proof

      assume

       A1: Z c= ( dom ( ln (#) cot ));

      then

       A2: Z c= (( dom ln ) /\ ( dom cot )) by VALUED_1:def 4;

      then

       A3: Z c= ( dom cot ) by XBOOLE_1: 18;

      

       A4: for x st x in Z holds cot is_differentiable_in x & ( diff ( cot ,x)) = ( - (1 / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A3, Th2;

        hence thesis by FDIFF_7: 47;

      end;

      then for x st x in Z holds cot is_differentiable_in x;

      then

       A5: cot is_differentiable_on Z by A3, FDIFF_1: 9;

      

       A6: Z c= ( dom ln ) by A2, XBOOLE_1: 18;

      

       A7: for x st x in Z holds x > 0

      proof

        let x;

        assume x in Z;

        then x in ( right_open_halfline 0 ) by A6, TAYLOR_1: 18;

        then ex g be Real st x = g & 0 < g by Lm1;

        hence thesis;

      end;

      then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1: 18;

      then

       A8: ln is_differentiable_on Z by A6, FDIFF_1: 9;

      

       A9: for x st x in Z holds ( diff ( ln ,x)) = (1 / x)

      proof

        let x;

        assume x in Z;

        then x > 0 by A7;

        then x in ( right_open_halfline 0 ) by Lm1;

        hence thesis by TAYLOR_1: 18;

      end;

      for x st x in Z holds ((( ln (#) cot ) `| Z) . x) = (((( cos . x) / ( sin . x)) / x) - (( ln . x) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A10: x in Z;

        

        then ((( ln (#) cot ) `| Z) . x) = ((( cot . x) * ( diff ( ln ,x))) + (( ln . x) * ( diff ( cot ,x)))) by A1, A8, A5, FDIFF_1: 21

        .= ((( cot . x) * (1 / x)) + (( ln . x) * ( diff ( cot ,x)))) by A9, A10

        .= ((( cot . x) * (1 / x)) + (( ln . x) * ( - (1 / (( sin . x) ^2 ))))) by A4, A10

        .= (((( cos . x) / ( sin . x)) / x) - (( ln . x) / (( sin . x) ^2 ))) by A3, A10, RFUNCT_1:def 1;

        hence thesis;

      end;

      hence thesis by A1, A8, A5, FDIFF_1: 21;

    end;

    theorem :: FDIFF_8:34

     not 0 in Z & Z c= ( dom ((( id Z) ^ ) (#) tan )) implies ((( id Z) ^ ) (#) tan ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) ^ ) (#) tan ) `| Z) . x) = (( - ((( sin . x) / ( cos . x)) / (x ^2 ))) + ((1 / x) / (( cos . x) ^2 )))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ((f ^ ) (#) tan ));

      

       A3: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

       A4: Z c= (( dom (f ^ )) /\ ( dom tan )) by A2, VALUED_1:def 4;

      then

       A5: Z c= ( dom tan ) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds tan is_differentiable_in x & ( diff ( tan ,x)) = (1 / (( cos . x) ^2 ))

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A5, Th1;

        hence thesis by FDIFF_7: 46;

      end;

      then for x st x in Z holds tan is_differentiable_in x;

      then

       A7: tan is_differentiable_on Z by A5, FDIFF_1: 9;

      

       A8: Z c= ( dom (f ^ )) by A4, XBOOLE_1: 18;

      for x st x in Z holds ((((f ^ ) (#) tan ) `| Z) . x) = (( - ((( sin . x) / ( cos . x)) / (x ^2 ))) + ((1 / x) / (( cos . x) ^2 )))

      proof

        let x;

        assume

         A9: x in Z;

        

        then ((((f ^ ) (#) tan ) `| Z) . x) = ((( tan . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( tan ,x)))) by A2, A3, A7, FDIFF_1: 21

        .= ((( tan . x) * (((f ^ ) `| Z) . x)) + (((f ^ ) . x) * ( diff ( tan ,x)))) by A3, A9, FDIFF_1:def 7

        .= ((( tan . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( tan ,x)))) by A1, A9, FDIFF_5: 4

        .= (( - (( tan . x) * (1 / (x ^2 )))) + (((f ^ ) . x) * (1 / (( cos . x) ^2 )))) by A6, A9

        .= (( - ((( sin . x) / ( cos . x)) * (1 / (x ^2 )))) + (((f ^ ) . x) / (( cos . x) ^2 ))) by A5, A9, RFUNCT_1:def 1

        .= (( - ((( sin . x) / ( cos . x)) / (x ^2 ))) + (((f . x) " ) / (( cos . x) ^2 ))) by A8, A9, RFUNCT_1:def 2

        .= (( - ((( sin . x) / ( cos . x)) / (x ^2 ))) + ((1 / x) / (( cos . x) ^2 ))) by A9, FUNCT_1: 18;

        hence thesis;

      end;

      hence thesis by A2, A3, A7, FDIFF_1: 21;

    end;

    theorem :: FDIFF_8:35

     not 0 in Z & Z c= ( dom ((( id Z) ^ ) (#) cot )) implies ((( id Z) ^ ) (#) cot ) is_differentiable_on Z & for x st x in Z holds ((((( id Z) ^ ) (#) cot ) `| Z) . x) = (( - ((( cos . x) / ( sin . x)) / (x ^2 ))) - ((1 / x) / (( sin . x) ^2 )))

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ((f ^ ) (#) cot ));

      

       A3: (f ^ ) is_differentiable_on Z by A1, FDIFF_5: 4;

      

       A4: Z c= (( dom (f ^ )) /\ ( dom cot )) by A2, VALUED_1:def 4;

      then

       A5: Z c= ( dom cot ) by XBOOLE_1: 18;

      

       A6: for x st x in Z holds cot is_differentiable_in x & ( diff ( cot ,x)) = ( - (1 / (( sin . x) ^2 )))

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A5, Th2;

        hence thesis by FDIFF_7: 47;

      end;

      then for x st x in Z holds cot is_differentiable_in x;

      then

       A7: cot is_differentiable_on Z by A5, FDIFF_1: 9;

      

       A8: Z c= ( dom (f ^ )) by A4, XBOOLE_1: 18;

      for x st x in Z holds ((((f ^ ) (#) cot ) `| Z) . x) = (( - ((( cos . x) / ( sin . x)) / (x ^2 ))) - ((1 / x) / (( sin . x) ^2 )))

      proof

        let x;

        assume

         A9: x in Z;

        

        then ((((f ^ ) (#) cot ) `| Z) . x) = ((( cot . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( cot ,x)))) by A2, A3, A7, FDIFF_1: 21

        .= ((( cot . x) * (((f ^ ) `| Z) . x)) + (((f ^ ) . x) * ( diff ( cot ,x)))) by A3, A9, FDIFF_1:def 7

        .= ((( cot . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( cot ,x)))) by A1, A9, FDIFF_5: 4

        .= (( - (( cot . x) * (1 / (x ^2 )))) + (((f ^ ) . x) * ( - (1 / (( sin . x) ^2 ))))) by A6, A9

        .= (( - ((( cos . x) / ( sin . x)) * (1 / (x ^2 )))) - (((f ^ ) . x) / (( sin . x) ^2 ))) by A5, A9, RFUNCT_1:def 1

        .= (( - ((( cos . x) / ( sin . x)) / (x ^2 ))) - (((f . x) " ) / (( sin . x) ^2 ))) by A8, A9, RFUNCT_1:def 2

        .= (( - ((( cos . x) / ( sin . x)) / (x ^2 ))) - ((1 / x) / (( sin . x) ^2 ))) by A9, FUNCT_1: 18;

        hence thesis;

      end;

      hence thesis by A2, A3, A7, FDIFF_1: 21;

    end;