fdiff_5.miz



    begin

    reserve y for set,

x,a,b for Real,

n for Element of NAT ,

Z for open Subset of REAL ,

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

    

     Lm1: Z c= ( dom (f1 + f2)) & (for x st x in Z holds (f1 . x) = a) & 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) = a 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) + a) 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 #Z (2 - 1)))

      proof

        let x;

        assume

         A11: x in Z;

        ( diff (f2,x)) = (2 * (x #Z (2 - 1))) by A3, TAYLOR_1: 2;

        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;

        

        hence (((f1 + f2) `| Z) . x) = (((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 #Z (2 - 1))) by A10, A12

        .= (2 * (x |^ 1)) by PREPOWER: 36

        .= (2 * x);

      end;

      hence thesis by A1, A8, A9, FDIFF_1: 18;

    end;

    

     Lm2: Z c= ( dom (f1 - f2)) & (for x st x in Z holds (f1 . x) = a) & 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) = a 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: 12;

      then

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

      

       A7: for x st x in Z holds (f1 . x) = (( 0 * x) + a) 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 #Z (2 - 1)))

      proof

        let x;

        assume

         A11: x in Z;

        ( diff (f2,x)) = (2 * (x #Z (2 - 1))) by A3, TAYLOR_1: 2;

        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: 19;

        

        hence (((f1 - f2) `| Z) . x) = (((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

        .= ( 0 - (2 * (x #Z (2 - 1)))) by A10, A12

        .= ( 0 - (2 * (x |^ 1))) by PREPOWER: 36

        .= ( - (2 * (x |^ 1)))

        .= ( - (2 * x));

      end;

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

    end;

    

     Lm3: Z c= ( dom ( #R (1 / 2))) implies ( #R (1 / 2)) is_differentiable_on Z & for x st x in Z holds ((( #R (1 / 2)) `| Z) . x) = ((1 / 2) * (x #R ( - (1 / 2))))

    proof

      assume

       A1: Z c= ( dom ( #R (1 / 2)));

      

       A2: for x st x in Z holds ( #R (1 / 2)) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then x in ( dom ( #R (1 / 2))) by A1;

        then x in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

        then x > 0 by XXREAL_1: 4;

        hence thesis by TAYLOR_1: 21;

      end;

      then

       A3: ( #R (1 / 2)) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A4: x in Z;

        then x in ( dom ( #R (1 / 2))) by A1;

        then x in ( right_open_halfline 0 ) by TAYLOR_1:def 4;

        then x > 0 by XXREAL_1: 4;

        

        then ( diff (( #R (1 / 2)),x)) = ((1 / 2) * (x #R ((1 / 2) - 1))) by TAYLOR_1: 21

        .= ((1 / 2) * (x #R ( - (1 / 2))));

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

      end;

      hence thesis by A1, A2, FDIFF_1: 9;

    end;

    theorem :: FDIFF_5:1

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

    proof

      assume that

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

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

      

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

      then

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

      

       A5: for x st x in Z holds (f1 . x) = ((1 * x) + a) by A2;

      then

       A6: f1 is_differentiable_on Z by A4, FDIFF_1: 23;

      

       A7: for x st x in Z holds (f2 . x) = ((( - 1) * x) + a)

      proof

        let x;

        assume x in Z;

        then (f2 . x) = (a - x) by A2;

        hence thesis;

      end;

      

       A8: Z c= ( dom f2) by A3, XBOOLE_1: 1;

      then

       A9: f2 is_differentiable_on Z by A7, FDIFF_1: 23;

      

       A10: for x st x in Z holds (f2 . x) <> 0 by A2;

      then

       A11: (f1 / f2) is_differentiable_on Z by A6, A9, FDIFF_2: 21;

      for x st x in Z holds (((f1 / f2) `| Z) . x) = ((2 * a) / ((a - x) ^2 ))

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: (f2 . x) <> 0 by A2;

        

         A14: (f1 . x) = (a + x) & (f2 . x) = (a - x) by A2, A12;

        f1 is_differentiable_in x & f2 is_differentiable_in x by A6, A9, A12, FDIFF_1: 9;

        

        then ( diff ((f1 / f2),x)) = (((( diff (f1,x)) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A13, FDIFF_2: 14

        .= (((((f1 `| Z) . x) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A6, A12, FDIFF_1:def 7

        .= (((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A9, A12, FDIFF_1:def 7

        .= (((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A4, A5, A12, FDIFF_1: 23

        .= (((1 * (f2 . x)) - (( - 1) * (f1 . x))) / ((f2 . x) ^2 )) by A8, A7, A12, FDIFF_1: 23

        .= ((2 * a) / ((a - x) ^2 )) by A14;

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

      end;

      hence thesis by A6, A9, A10, FDIFF_2: 21;

    end;

    theorem :: FDIFF_5:2

    Z c= ( dom (f1 / f2)) & (for x st x in Z holds (f1 . x) = (x - a) & (f2 . x) = (x + a) & (f2 . x) <> 0 ) implies (f1 / f2) is_differentiable_on Z & for x st x in Z holds (((f1 / f2) `| Z) . x) = ((2 * a) / ((x + a) ^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 + a) & (f2 . x) <> 0 ;

      

       A3: for x st x in Z holds (f2 . x) = ((1 * x) + a) by A2;

      

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

      then

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

      

       A6: Z c= ( dom f2) by A4, XBOOLE_1: 1;

      then

       A7: f2 is_differentiable_on Z by A3, FDIFF_1: 23;

      

       A8: for x st x in Z holds (f1 . x) = ((1 * x) + ( - a))

      proof

        let x;

        

         A9: ((1 * x) + ( - a)) = ((1 * x) - a);

        assume x in Z;

        hence thesis by A2, A9;

      end;

      then

       A10: f1 is_differentiable_on Z by A5, FDIFF_1: 23;

      

       A11: for x st x in Z holds (f2 . x) <> 0 by A2;

      then

       A12: (f1 / f2) is_differentiable_on Z by A10, A7, FDIFF_2: 21;

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

      proof

        let x;

        assume

         A13: x in Z;

        then

         A14: (f2 . x) <> 0 by A2;

        

         A15: (f1 . x) = (x - a) & (f2 . x) = (x + a) by A2, A13;

        f1 is_differentiable_in x & f2 is_differentiable_in x by A10, A7, A13, FDIFF_1: 9;

        

        then ( diff ((f1 / f2),x)) = (((( diff (f1,x)) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A14, FDIFF_2: 14

        .= (((((f1 `| Z) . x) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A10, A13, FDIFF_1:def 7

        .= (((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A7, A13, FDIFF_1:def 7

        .= (((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A5, A8, A13, FDIFF_1: 23

        .= (((1 * (f2 . x)) - (1 * (f1 . x))) / ((f2 . x) ^2 )) by A6, A3, A13, FDIFF_1: 23

        .= ((2 * a) / ((x + a) ^2 )) by A15;

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

      end;

      hence thesis by A10, A7, A11, FDIFF_2: 21;

    end;

    theorem :: FDIFF_5:3

    Z c= ( dom (f1 / f2)) & (for x st x in Z holds (f1 . x) = (x - a) & (f2 . x) = (x - b) & (f2 . x) <> 0 ) 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) & (f2 . x) <> 0 ;

      

       A3: for x st x in Z holds (f1 . x) = ((1 * x) + ( - a)) & (f2 . x) = ((1 * x) + ( - b))

      proof

        let x;

        

         A4: ((1 * x) + ( - a)) = ((1 * x) - a) & ((1 * x) + ( - b)) = ((1 * x) - b);

        assume x in Z;

        hence thesis by A2, A4;

      end;

      then

       A5: for x st x in Z holds (f1 . x) = ((1 * x) + ( - a));

      

       A6: Z c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by A1, RFUNCT_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 (f2 . x) = ((1 * x) + ( - b)) by A3;

      

       A10: Z c= ( dom f2) by A6, XBOOLE_1: 1;

      then

       A11: f2 is_differentiable_on Z by A9, FDIFF_1: 23;

      

       A12: for x st x in Z holds (f2 . x) <> 0 by A2;

      then

       A13: (f1 / f2) is_differentiable_on Z by A8, A11, FDIFF_2: 21;

      for x st x in Z holds (((f1 / f2) `| Z) . x) = ((a - b) / ((x - b) ^2 ))

      proof

        let x;

        assume

         A14: x in Z;

        then

         A15: (f2 . x) <> 0 by A2;

        

         A16: (f1 . x) = (x - a) & (f2 . x) = (x - b) by A2, A14;

        f1 is_differentiable_in x & f2 is_differentiable_in x by A8, A11, A14, FDIFF_1: 9;

        

        then ( diff ((f1 / f2),x)) = (((( diff (f1,x)) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A15, FDIFF_2: 14

        .= (((((f1 `| Z) . x) * (f2 . x)) - (( diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2 )) by A8, A14, FDIFF_1:def 7

        .= (((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A11, A14, FDIFF_1:def 7

        .= (((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2 )) by A7, A5, A14, FDIFF_1: 23

        .= (((1 * (f2 . x)) - (1 * (f1 . x))) / ((f2 . x) ^2 )) by A10, A9, A14, FDIFF_1: 23

        .= ((a - b) / ((x - b) ^2 )) by A16;

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

      end;

      hence thesis by A8, A11, A12, FDIFF_2: 21;

    end;

    theorem :: FDIFF_5:4

    

     Th4: not 0 in Z implies (( id Z) ^ ) is_differentiable_on Z & for x st x in Z holds (((( id Z) ^ ) `| Z) . x) = ( - (1 / (x ^2 )))

    proof

      set f = ( id Z);

      

       A1: Z c= ( dom f) & for x st x in Z holds (f . x) = ((1 * x) + 0 ) by FUNCT_1: 17;

      then

       A2: f is_differentiable_on Z by FDIFF_1: 23;

      assume

       A3: not 0 in Z;

      then

       A4: for x st x in Z holds (f . x) <> 0 by FUNCT_1: 18;

      then

       A5: (f ^ ) is_differentiable_on Z by A2, FDIFF_2: 22;

      now

        let x;

        assume

         A6: x in Z;

        then

         A7: (f . x) <> 0 & f is_differentiable_in x by A3, A2, FDIFF_1: 9, FUNCT_1: 18;

        (((f ^ ) `| Z) . x) = ( diff ((f ^ ),x)) by A5, A6, FDIFF_1:def 7

        .= ( - (( diff (f,x)) / ((f . x) ^2 ))) by A7, FDIFF_2: 15

        .= ( - (((f `| Z) . x) / ((f . x) ^2 ))) by A2, A6, FDIFF_1:def 7

        .= ( - (1 / ((f . x) ^2 ))) by A1, A6, FDIFF_1: 23

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

        hence (((f ^ ) `| Z) . x) = ( - (1 / (x ^2 )));

      end;

      hence thesis by A2, A4, FDIFF_2: 22;

    end;

    

     Lm4: not 0 in Z implies ( dom ( sin * (( id Z) ^ ))) = Z

    proof

      

       A1: ( rng (( id Z) ^ )) c= REAL by RELAT_1:def 19;

      assume

       A2: not 0 in Z;

      (( id Z) " { 0 }) c= {}

      proof

        let x be object;

        assume

         A3: x in (( id Z) " { 0 });

        then x in ( dom ( id Z)) by FUNCT_1:def 7;

        then

         A4: x in Z by FUNCT_1: 17;

        (( id Z) . x) in { 0 } by A3, FUNCT_1:def 7;

        then x in { 0 } by A4, FUNCT_1: 18;

        hence thesis by A2, A4, TARSKI:def 1;

      end;

      then

       A5: (( id Z) " { 0 }) = {} by XBOOLE_1: 3;

      ( dom (( id Z) ^ )) = (( dom ( id Z)) \ (( id Z) " { 0 })) by RFUNCT_1:def 2

      .= Z by A5, FUNCT_1: 17;

      hence thesis by A1, RELAT_1: 27, SIN_COS: 24;

    end;

    theorem :: FDIFF_5:5

    

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

    proof

      set f = ( id Z);

      assume

       A1: not 0 in Z;

      then

       A2: Z c= ( dom ( sin * (f ^ ))) by Lm4;

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

      then

       A3: Z c= ( dom (f ^ ));

      

       A4: (f ^ ) is_differentiable_on Z by A1, Th4;

      

       A5: for x st x in Z holds ( sin * (f ^ )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A6: (f ^ ) is_differentiable_in x by A4, FDIFF_1: 9;

         sin is_differentiable_in ((f ^ ) . x) by SIN_COS: 64;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

       A7: ( sin * (f ^ )) is_differentiable_on Z by A2, FDIFF_1: 9;

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

      proof

        let x;

        

         A8: sin is_differentiable_in ((f ^ ) . x) by SIN_COS: 64;

        assume

         A9: x in Z;

        then (f ^ ) is_differentiable_in x by A4, FDIFF_1: 9;

        

        then ( diff (( sin * (f ^ )),x)) = (( diff ( sin ,((f ^ ) . x))) * ( diff ((f ^ ),x))) by A8, FDIFF_2: 13

        .= (( cos . ((f ^ ) . x)) * ( diff ((f ^ ),x))) by SIN_COS: 64

        .= (( cos . ((f . x) " )) * ( diff ((f ^ ),x))) by A3, A9, RFUNCT_1:def 2

        .= (( cos . ((f . x) " )) * (((f ^ ) `| Z) . x)) by A4, A9, FDIFF_1:def 7

        .= (( cos . ((f . x) " )) * ( - (1 / (x ^2 )))) by A1, A9, Th4

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

        .= (( cos . (1 / x)) * ( - (1 / (x ^2 )))) by XCMPLX_0:def 9;

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

      end;

      hence thesis by A2, A5, FDIFF_1: 9;

    end;

    theorem :: FDIFF_5:6

    

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

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

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

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

      then

       A3: Z c= ( dom (f ^ ));

      

       A4: (f ^ ) is_differentiable_on Z by A1, Th4;

      

       A5: for x st x in Z holds ( cos * (f ^ )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A6: (f ^ ) is_differentiable_in x by A4, FDIFF_1: 9;

         cos is_differentiable_in ((f ^ ) . x) by SIN_COS: 63;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

       A7: ( cos * (f ^ )) is_differentiable_on Z by A2, FDIFF_1: 9;

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

      proof

        let x;

        

         A8: ( diff ( cos ,((f ^ ) . x))) = ( - ( sin . ((f ^ ) . x))) by SIN_COS: 63;

        

         A9: cos is_differentiable_in ((f ^ ) . x) by SIN_COS: 63;

        assume

         A10: x in Z;

        then (f ^ ) is_differentiable_in x by A4, FDIFF_1: 9;

        

        then ( diff (( cos * (f ^ )),x)) = (( diff ( cos ,((f ^ ) . x))) * ( diff ((f ^ ),x))) by A9, FDIFF_2: 13

        .= ( - (( sin . ((f ^ ) . x)) * ( diff ((f ^ ),x)))) by A8

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

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

        .= ( - (( sin . ((f . x) " )) * ( - (1 / (x ^2 ))))) by A1, A10, Th4

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

        .= ( - (( sin . (1 / x)) * ( - (1 / (x ^2 ))))) by XCMPLX_0:def 9

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

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

      end;

      hence thesis by A2, A5, FDIFF_1: 9;

    end;

    theorem :: FDIFF_5:7

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

    proof

      set f = ( id Z);

      assume that

       A1: Z c= ( dom (( id Z) (#) ( sin * (f ^ )))) and

       A2: not 0 in Z;

      

       A3: ( sin * (f ^ )) is_differentiable_on Z by A2, Th5;

      

       A4: Z c= (( dom ( id Z)) /\ ( dom ( sin * (f ^ )))) by A1, VALUED_1:def 4;

      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 ( sin * (f ^ ))) by A4, XBOOLE_1: 18;

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

      then

       A9: Z c= ( dom (f ^ ));

      now

        let x;

        assume

         A10: x in Z;

        

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

        .= (((( sin * (f ^ )) . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff (( sin * (f ^ )),x)))) by A7, A10, FDIFF_1:def 7

        .= (((( sin * (f ^ )) . x) * 1) + ((( id Z) . x) * ( diff (( sin * (f ^ )),x)))) by A5, A6, A10, FDIFF_1: 23

        .= ((( sin * (f ^ )) . x) + (x * ( diff (( sin * (f ^ )),x)))) by A10, FUNCT_1: 18

        .= ((( sin * (f ^ )) . x) + (x * ((( sin * (f ^ )) `| Z) . x))) by A3, A10, FDIFF_1:def 7

        .= ((( sin * (f ^ )) . x) + (x * ( - ((1 / (x ^2 )) * ( cos . (1 / x)))))) by A2, A10, Th5

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

        .= ((( sin * (f ^ )) . x) - ((x * ((1 / x) * (1 / x))) * ( cos . (1 / x)))) by XCMPLX_1: 102

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

        .= ((( sin * (f ^ )) . x) - ((1 * (1 / x)) * ( cos . (1 / x)))) by A2, A10, XCMPLX_1: 106

        .= (( sin . ((f ^ ) . x)) - ((1 / x) * ( cos . (1 / x)))) by A8, A10, FUNCT_1: 12

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

        .= (( sin . (1 * (x " ))) - ((1 / x) * ( cos . (1 / x)))) by A10, FUNCT_1: 18

        .= (( sin . (1 / x)) - ((1 / x) * ( cos . (1 / x)))) by XCMPLX_0:def 9;

        hence (((( id Z) (#) ( sin * (f ^ ))) `| Z) . x) = (( sin . (1 / x)) - ((1 / x) * ( cos . (1 / x))));

      end;

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

    end;

    theorem :: FDIFF_5:8

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

    proof

      set f = ( id Z);

      assume that

       A1: Z c= ( dom (( id Z) (#) ( cos * (f ^ )))) and

       A2: not 0 in Z;

      

       A3: Z c= (( dom ( id Z)) /\ ( dom ( cos * (f ^ )))) by A1, VALUED_1:def 4;

      then

       A4: Z c= ( dom ( cos * (f ^ ))) by XBOOLE_1: 18;

      then

       A5: ( cos * (f ^ )) is_differentiable_on Z by A2, Th6;

      

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

      

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

      then

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

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

      then

       A9: Z c= ( dom (f ^ ));

      now

        let x;

        assume

         A10: x in Z;

        

        then (((( id Z) (#) ( cos * (f ^ ))) `| Z) . x) = (((( cos * (f ^ )) . x) * ( diff (( id Z),x))) + ((( id Z) . x) * ( diff (( cos * (f ^ )),x)))) by A1, A5, A8, FDIFF_1: 21

        .= (((( cos * (f ^ )) . x) * ((( id Z) `| Z) . x)) + ((( id Z) . x) * ( diff (( cos * (f ^ )),x)))) by A8, A10, FDIFF_1:def 7

        .= (((( cos * (f ^ )) . x) * 1) + ((( id Z) . x) * ( diff (( cos * (f ^ )),x)))) by A7, A6, A10, FDIFF_1: 23

        .= ((( cos * (f ^ )) . x) + (x * ( diff (( cos * (f ^ )),x)))) by A10, FUNCT_1: 18

        .= ((( cos * (f ^ )) . x) + (x * ((( cos * (f ^ )) `| Z) . x))) by A5, A10, FDIFF_1:def 7

        .= ((( cos * (f ^ )) . x) + (x * ((1 / (x ^2 )) * ( sin . (1 / x))))) by A2, A4, A10, Th6

        .= ((( cos * (f ^ )) . x) + ((x * (1 / (x * x))) * ( sin . (1 / x))))

        .= ((( cos * (f ^ )) . x) + ((x * ((1 / x) * (1 / x))) * ( sin . (1 / x)))) by XCMPLX_1: 102

        .= ((( cos * (f ^ )) . x) + (((x * (1 / x)) * (1 / x)) * ( sin . (1 / x))))

        .= ((( cos * (f ^ )) . x) + ((1 * (1 / x)) * ( sin . (1 / x)))) by A2, A10, XCMPLX_1: 106

        .= (( cos . ((f ^ ) . x)) + ((1 / x) * ( sin . (1 / x)))) by A4, A10, FUNCT_1: 12

        .= (( cos . ((f . x) " )) + ((1 / x) * ( sin . (1 / x)))) by A9, A10, RFUNCT_1:def 2

        .= (( cos . (1 * (x " ))) + ((1 / x) * ( sin . (1 / x)))) by A10, FUNCT_1: 18

        .= (( cos . (1 / x)) + ((1 / x) * ( sin . (1 / x)))) by XCMPLX_0:def 9;

        hence (((( id Z) (#) ( cos * (f ^ ))) `| Z) . x) = (( cos . (1 / x)) + ((1 / x) * ( sin . (1 / x))));

      end;

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

    end;

    theorem :: FDIFF_5:9

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

    proof

      set f = ( id Z);

      assume that

       A1: Z c= ( dom (( sin * (f ^ )) (#) ( cos * (f ^ )))) and

       A2: not 0 in Z;

      

       A3: ( sin * (f ^ )) is_differentiable_on Z by A2, Th5;

      

       A4: Z c= (( dom ( sin * (f ^ ))) /\ ( dom ( cos * (f ^ )))) by A1, VALUED_1:def 4;

      then

       A5: Z c= ( dom ( cos * (f ^ ))) by XBOOLE_1: 18;

      then

       A6: ( cos * (f ^ )) is_differentiable_on Z by A2, Th6;

      

       A7: Z c= ( dom ( sin * (f ^ ))) by A4, XBOOLE_1: 18;

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

      then

       A8: Z c= ( dom (f ^ ));

      now

        let x;

        assume

         A9: x in Z;

        

        then (((( sin * (f ^ )) (#) ( cos * (f ^ ))) `| Z) . x) = (((( cos * (f ^ )) . x) * ( diff (( sin * (f ^ )),x))) + ((( sin * (f ^ )) . x) * ( diff (( cos * (f ^ )),x)))) by A1, A6, A3, FDIFF_1: 21

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

        .= (((( cos * (f ^ )) . x) * ( - ((1 / (x ^2 )) * ( cos . (1 / x))))) + ((( sin * (f ^ )) . x) * ( diff (( cos * (f ^ )),x)))) by A2, A9, Th5

        .= (((( cos * (f ^ )) . x) * ( - ((1 / (x ^2 )) * ( cos . (1 / x))))) + ((( sin * (f ^ )) . x) * ((( cos * (f ^ )) `| Z) . x))) by A6, A9, FDIFF_1:def 7

        .= (((( cos * (f ^ )) . x) * ( - ((1 / (x ^2 )) * ( cos . (1 / x))))) + ((( sin * (f ^ )) . x) * ((1 / (x ^2 )) * ( sin . (1 / x))))) by A2, A5, A9, Th6

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

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

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

        .= ((( cos . (1 / x)) * ( - ((1 / (x ^2 )) * ( cos . (1 / x))))) + ((( sin * (f ^ )) . x) * ((1 / (x ^2 )) * ( sin . (1 / x))))) by XCMPLX_0:def 9

        .= ((( cos . (1 / x)) * ( - ((1 / (x ^2 )) * ( cos . (1 / x))))) + (( sin . ((f ^ ) . x)) * ((1 / (x ^2 )) * ( sin . (1 / x))))) by A7, A9, FUNCT_1: 12

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

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

        .= (( - ((( cos . (1 / x)) * (1 / (x ^2 ))) * ( cos . (1 / x)))) + (( sin . (1 / x)) * ((1 / (x ^2 )) * ( sin . (1 / x))))) by XCMPLX_0:def 9

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

        hence (((( sin * (f ^ )) (#) ( cos * (f ^ ))) `| Z) . x) = ((1 / (x ^2 )) * ((( sin . (1 / x)) ^2 ) - (( cos . (1 / x)) ^2 )));

      end;

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

    end;

    theorem :: FDIFF_5:10

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

    proof

      assume that

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

       A2: n >= 1 and

       A3: for x st x in Z holds (f . x) = (n * x);

      

       A4: for x st x in Z holds (f . x) = ((n * x) + 0 ) by A3;

      

       A5: Z c= (( dom ( sin * f)) /\ ( dom (( #Z n) * sin ))) by A1, VALUED_1:def 4;

      then

       A6: Z c= ( dom ( sin * f)) by XBOOLE_1: 18;

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

      then

       A7: Z c= ( dom f);

      then

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

      for x st x in Z holds ( sin * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A9: f is_differentiable_in x by A8, FDIFF_1: 9;

         sin is_differentiable_in (f . x) by SIN_COS: 64;

        hence thesis by A9, FDIFF_2: 13;

      end;

      then

       A10: ( sin * f) is_differentiable_on Z by A6, FDIFF_1: 9;

      

       A11: for x st x in Z holds ((( sin * f) `| Z) . x) = (n * ( cos . (n * x)))

      proof

        let x;

        

         A12: sin is_differentiable_in (f . x) by SIN_COS: 64;

        assume

         A13: x in Z;

        then f is_differentiable_in x by A8, FDIFF_1: 9;

        

        then ( diff (( sin * f),x)) = (( diff ( sin ,(f . x))) * ( diff (f,x))) by A12, FDIFF_2: 13

        .= (( cos . (f . x)) * ( diff (f,x))) by SIN_COS: 64

        .= (( cos . (n * x)) * ( diff (f,x))) by A3, A13

        .= (( cos . (n * x)) * ((f `| Z) . x)) by A8, A13, FDIFF_1:def 7

        .= (n * ( cos . (n * x))) by A7, A4, A13, FDIFF_1: 23;

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

      end;

      

       A14: Z c= ( dom (( #Z n) * sin )) by A5, XBOOLE_1: 18;

      now

        let x;

        assume x in Z;

         sin is_differentiable_in x by SIN_COS: 64;

        hence (( #Z n) * sin ) is_differentiable_in x by TAYLOR_1: 3;

      end;

      then

       A15: (( #Z n) * sin ) is_differentiable_on Z by A14, FDIFF_1: 9;

      

       A16: for x st x in Z holds (((( #Z n) * sin ) `| Z) . x) = ((n * (( sin . x) #Z (n - 1))) * ( cos . x))

      proof

        let x;

         sin is_differentiable_in x by SIN_COS: 64;

        

        then

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

        .= ((n * (( sin . x) #Z (n - 1))) * ( cos . x)) by SIN_COS: 64;

        assume x in Z;

        hence thesis by A15, A17, FDIFF_1:def 7;

      end;

      now

        let x;

        

         A18: (n - 1) is Element of NAT by A2, NAT_1: 21;

        assume

         A19: x in Z;

        

        then (((( sin * f) (#) (( #Z n) * sin )) `| Z) . x) = ((((( #Z n) * sin ) . x) * ( diff (( sin * f),x))) + ((( sin * f) . x) * ( diff ((( #Z n) * sin ),x)))) by A1, A10, A15, FDIFF_1: 21

        .= (((( #Z n) . ( sin . x)) * ( diff (( sin * f),x))) + ((( sin * f) . x) * ( diff ((( #Z n) * sin ),x)))) by A14, A19, FUNCT_1: 12

        .= (((( sin . x) #Z n) * ( diff (( sin * f),x))) + ((( sin * f) . x) * ( diff ((( #Z n) * sin ),x)))) by TAYLOR_1:def 1

        .= (((( sin . x) #Z n) * ((( sin * f) `| Z) . x)) + ((( sin * f) . x) * ( diff ((( #Z n) * sin ),x)))) by A10, A19, FDIFF_1:def 7

        .= (((( sin . x) #Z n) * (n * ( cos . (n * x)))) + ((( sin * f) . x) * ( diff ((( #Z n) * sin ),x)))) by A11, A19

        .= (((( sin . x) #Z n) * (n * ( cos . (n * x)))) + (( sin . (f . x)) * ( diff ((( #Z n) * sin ),x)))) by A6, A19, FUNCT_1: 12

        .= (((( sin . x) #Z n) * (n * ( cos . (n * x)))) + (( sin . (n * x)) * ( diff ((( #Z n) * sin ),x)))) by A3, A19

        .= (((( sin . x) #Z n) * (n * ( cos . (n * x)))) + (( sin . (n * x)) * (((( #Z n) * sin ) `| Z) . x))) by A15, A19, FDIFF_1:def 7

        .= (((( sin . x) #Z n) * (n * ( cos . (n * x)))) + (( sin . (n * x)) * ((n * (( sin . x) #Z (n - 1))) * ( cos . x)))) by A16, A19

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

        .= ((((( sin . x) #Z (n - 1)) * (( sin . x) #Z 1)) * (n * ( cos . (n * x)))) + (((( sin . (n * x)) * n) * (( sin . x) #Z (n - 1))) * ( cos . x))) by A18, TAYLOR_1: 1

        .= ((((( sin . x) #Z (n - 1)) * ( sin . x)) * (n * ( cos . (n * x)))) + (((( sin . (n * x)) * n) * (( sin . x) #Z (n - 1))) * ( cos . x))) by PREPOWER: 35

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

        .= ((n * (( sin . x) #Z (n - 1))) * ( sin . (x + (n * x)))) by SIN_COS: 74

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

        hence (((( sin * f) (#) (( #Z n) * sin )) `| Z) . x) = ((n * (( sin . x) #Z (n - 1))) * ( sin . ((n + 1) * x)));

      end;

      hence thesis by A1, A10, A15, FDIFF_1: 21;

    end;

    theorem :: FDIFF_5:11

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

    proof

      assume that

       A1: Z c= ( dom (( cos * f) (#) (( #Z n) * sin ))) and

       A2: n >= 1 and

       A3: for x st x in Z holds (f . x) = (n * x);

      

       A4: for x st x in Z holds (f . x) = ((n * x) + 0 ) by A3;

      

       A5: Z c= (( dom ( cos * f)) /\ ( dom (( #Z n) * sin ))) by A1, VALUED_1:def 4;

      then

       A6: Z c= ( dom ( cos * f)) by XBOOLE_1: 18;

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

      then

       A7: Z c= ( dom f);

      then

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

      for x st x in Z holds ( cos * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A9: f is_differentiable_in x by A8, FDIFF_1: 9;

         cos is_differentiable_in (f . x) by SIN_COS: 63;

        hence thesis by A9, FDIFF_2: 13;

      end;

      then

       A10: ( cos * f) is_differentiable_on Z by A6, FDIFF_1: 9;

      

       A11: for x st x in Z holds ((( cos * f) `| Z) . x) = ( - (n * ( sin . (n * x))))

      proof

        let x;

        

         A12: cos is_differentiable_in (f . x) by SIN_COS: 63;

        assume

         A13: x in Z;

        then f is_differentiable_in x by A8, FDIFF_1: 9;

        

        then ( diff (( cos * f),x)) = (( diff ( cos ,(f . x))) * ( diff (f,x))) by A12, FDIFF_2: 13

        .= (( - ( sin . (f . x))) * ( diff (f,x))) by SIN_COS: 63

        .= (( - ( sin . (n * x))) * ( diff (f,x))) by A3, A13

        .= (( - ( sin . (n * x))) * ((f `| Z) . x)) by A8, A13, FDIFF_1:def 7

        .= (( - ( sin . (n * x))) * n) by A7, A4, A13, FDIFF_1: 23

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

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

      end;

      

       A14: Z c= ( dom (( #Z n) * sin )) by A5, XBOOLE_1: 18;

      now

        let x;

        assume x in Z;

         sin is_differentiable_in x by SIN_COS: 64;

        hence (( #Z n) * sin ) is_differentiable_in x by TAYLOR_1: 3;

      end;

      then

       A15: (( #Z n) * sin ) is_differentiable_on Z by A14, FDIFF_1: 9;

      

       A16: for x st x in Z holds (((( #Z n) * sin ) `| Z) . x) = ((n * (( sin . x) #Z (n - 1))) * ( cos . x))

      proof

        let x;

         sin is_differentiable_in x by SIN_COS: 64;

        

        then

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

        .= ((n * (( sin . x) #Z (n - 1))) * ( cos . x)) by SIN_COS: 64;

        assume x in Z;

        hence thesis by A15, A17, FDIFF_1:def 7;

      end;

      now

        let x;

        

         A18: (n - 1) is Element of NAT by A2, NAT_1: 21;

        assume

         A19: x in Z;

        

        then (((( cos * f) (#) (( #Z n) * sin )) `| Z) . x) = ((((( #Z n) * sin ) . x) * ( diff (( cos * f),x))) + ((( cos * f) . x) * ( diff ((( #Z n) * sin ),x)))) by A1, A10, A15, FDIFF_1: 21

        .= (((( #Z n) . ( sin . x)) * ( diff (( cos * f),x))) + ((( cos * f) . x) * ( diff ((( #Z n) * sin ),x)))) by A14, A19, FUNCT_1: 12

        .= (((( sin . x) #Z n) * ( diff (( cos * f),x))) + ((( cos * f) . x) * ( diff ((( #Z n) * sin ),x)))) by TAYLOR_1:def 1

        .= (((( sin . x) #Z n) * ((( cos * f) `| Z) . x)) + ((( cos * f) . x) * ( diff ((( #Z n) * sin ),x)))) by A10, A19, FDIFF_1:def 7

        .= (((( sin . x) #Z n) * ( - (n * ( sin . (n * x))))) + ((( cos * f) . x) * ( diff ((( #Z n) * sin ),x)))) by A11, A19

        .= (((( sin . x) #Z n) * ( - (n * ( sin . (n * x))))) + (( cos . (f . x)) * ( diff ((( #Z n) * sin ),x)))) by A6, A19, FUNCT_1: 12

        .= (((( sin . x) #Z n) * ( - (n * ( sin . (n * x))))) + (( cos . (n * x)) * ( diff ((( #Z n) * sin ),x)))) by A3, A19

        .= (((( sin . x) #Z n) * ( - (n * ( sin . (n * x))))) + (( cos . (n * x)) * (((( #Z n) * sin ) `| Z) . x))) by A15, A19, FDIFF_1:def 7

        .= (((( sin . x) #Z n) * ( - (n * ( sin . (n * x))))) + (( cos . (n * x)) * ((n * (( sin . x) #Z (n - 1))) * ( cos . x)))) by A16, A19

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

        .= ((((( sin . x) #Z (n - 1)) * (( sin . x) #Z 1)) * ( - (n * ( sin . (n * x))))) + (((( cos . (n * x)) * n) * (( sin . x) #Z (n - 1))) * ( cos . x))) by A18, TAYLOR_1: 1

        .= ((((( sin . x) #Z (n - 1)) * ( sin . x)) * ( - (n * ( sin . (n * x))))) + (((( cos . (n * x)) * n) * (( sin . x) #Z (n - 1))) * ( cos . x))) by PREPOWER: 35

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

        .= ((n * (( sin . x) #Z (n - 1))) * ( cos . (x + (n * x)))) by SIN_COS: 74

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

        hence (((( cos * f) (#) (( #Z n) * sin )) `| Z) . x) = ((n * (( sin . x) #Z (n - 1))) * ( cos . ((n + 1) * x)));

      end;

      hence thesis by A1, A10, A15, FDIFF_1: 21;

    end;

    theorem :: FDIFF_5:12

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

    proof

      assume that

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

       A2: n >= 1 and

       A3: for x st x in Z holds (f . x) = (n * x);

      

       A4: for x st x in Z holds (f . x) = ((n * x) + 0 ) by A3;

      

       A5: Z c= (( dom ( cos * f)) /\ ( dom (( #Z n) * cos ))) by A1, VALUED_1:def 4;

      then

       A6: Z c= ( dom ( cos * f)) by XBOOLE_1: 18;

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

      then

       A7: Z c= ( dom f);

      then

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

      for x st x in Z holds ( cos * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A9: f is_differentiable_in x by A8, FDIFF_1: 9;

         cos is_differentiable_in (f . x) by SIN_COS: 63;

        hence thesis by A9, FDIFF_2: 13;

      end;

      then

       A10: ( cos * f) is_differentiable_on Z by A6, FDIFF_1: 9;

      

       A11: for x st x in Z holds ((( cos * f) `| Z) . x) = ( - (n * ( sin . (n * x))))

      proof

        let x;

        

         A12: cos is_differentiable_in (f . x) by SIN_COS: 63;

        assume

         A13: x in Z;

        then f is_differentiable_in x by A8, FDIFF_1: 9;

        

        then ( diff (( cos * f),x)) = (( diff ( cos ,(f . x))) * ( diff (f,x))) by A12, FDIFF_2: 13

        .= (( - ( sin . (f . x))) * ( diff (f,x))) by SIN_COS: 63

        .= ( - (( sin . (f . x)) * ( diff (f,x))))

        .= ( - (( sin . (n * x)) * ( diff (f,x)))) by A3, A13

        .= ( - (( sin . (n * x)) * ((f `| Z) . x))) by A8, A13, FDIFF_1:def 7

        .= ( - (n * ( sin . (n * x)))) by A7, A4, A13, FDIFF_1: 23;

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

      end;

      

       A14: Z c= ( dom (( #Z n) * cos )) by A5, XBOOLE_1: 18;

      now

        let x;

        assume x in Z;

         cos is_differentiable_in x by SIN_COS: 63;

        hence (( #Z n) * cos ) is_differentiable_in x by TAYLOR_1: 3;

      end;

      then

       A15: (( #Z n) * cos ) is_differentiable_on Z by A14, FDIFF_1: 9;

      

       A16: for x st x in Z holds (((( #Z n) * cos ) `| Z) . x) = ( - ((n * (( cos . x) #Z (n - 1))) * ( sin . x)))

      proof

        let x;

         cos is_differentiable_in x by SIN_COS: 63;

        

        then

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

        .= ((n * (( cos . x) #Z (n - 1))) * ( - ( sin . x))) by SIN_COS: 63

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

        assume x in Z;

        hence thesis by A15, A17, FDIFF_1:def 7;

      end;

      now

        let x;

        

         A18: (n - 1) is Element of NAT by A2, NAT_1: 21;

        assume

         A19: x in Z;

        

        then (((( cos * f) (#) (( #Z n) * cos )) `| Z) . x) = ((((( #Z n) * cos ) . x) * ( diff (( cos * f),x))) + ((( cos * f) . x) * ( diff ((( #Z n) * cos ),x)))) by A1, A10, A15, FDIFF_1: 21

        .= (((( #Z n) . ( cos . x)) * ( diff (( cos * f),x))) + ((( cos * f) . x) * ( diff ((( #Z n) * cos ),x)))) by A14, A19, FUNCT_1: 12

        .= (((( cos . x) #Z n) * ( diff (( cos * f),x))) + ((( cos * f) . x) * ( diff ((( #Z n) * cos ),x)))) by TAYLOR_1:def 1

        .= (((( cos . x) #Z n) * ((( cos * f) `| Z) . x)) + ((( cos * f) . x) * ( diff ((( #Z n) * cos ),x)))) by A10, A19, FDIFF_1:def 7

        .= (((( cos . x) #Z n) * ( - (n * ( sin . (n * x))))) + ((( cos * f) . x) * ( diff ((( #Z n) * cos ),x)))) by A11, A19

        .= (((( cos . x) #Z n) * ( - (n * ( sin . (n * x))))) + (( cos . (f . x)) * ( diff ((( #Z n) * cos ),x)))) by A6, A19, FUNCT_1: 12

        .= (((( cos . x) #Z n) * ( - (n * ( sin . (n * x))))) + (( cos . (n * x)) * ( diff ((( #Z n) * cos ),x)))) by A3, A19

        .= (((( cos . x) #Z n) * ( - (n * ( sin . (n * x))))) + (( cos . (n * x)) * (((( #Z n) * cos ) `| Z) . x))) by A15, A19, FDIFF_1:def 7

        .= (((( cos . x) #Z ((n - 1) + 1)) * ( - (n * ( sin . (n * x))))) + (( cos . (n * x)) * ( - ((n * (( cos . x) #Z (n - 1))) * ( sin . x))))) by A16, A19

        .= ((((( cos . x) #Z (n - 1)) * (( cos . x) #Z 1)) * ( - (n * ( sin . (n * x))))) + (( cos . (n * x)) * ( - ((n * (( cos . x) #Z (n - 1))) * ( sin . x))))) by A18, TAYLOR_1: 1

        .= ((((( cos . x) #Z (n - 1)) * ( cos . x)) * ( - (n * ( sin . (n * x))))) + (( cos . (n * x)) * ( - ((n * (( cos . x) #Z (n - 1))) * ( sin . x))))) by PREPOWER: 35

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

        .= ( - ((n * (( cos . x) #Z (n - 1))) * ( sin . (x + (n * x))))) by SIN_COS: 74

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

        hence (((( cos * f) (#) (( #Z n) * cos )) `| Z) . x) = ( - ((n * (( cos . x) #Z (n - 1))) * ( sin . ((n + 1) * x))));

      end;

      hence thesis by A1, A10, A15, FDIFF_1: 21;

    end;

    theorem :: FDIFF_5:13

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

    proof

      assume that

       A1: Z c= ( dom (( sin * f) (#) (( #Z n) * cos ))) and

       A2: n >= 1 and

       A3: for x st x in Z holds (f . x) = (n * x);

      

       A4: for x st x in Z holds (f . x) = ((n * x) + 0 ) by A3;

      

       A5: Z c= (( dom ( sin * f)) /\ ( dom (( #Z n) * cos ))) by A1, VALUED_1:def 4;

      then

       A6: Z c= ( dom ( sin * f)) by XBOOLE_1: 18;

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

      then

       A7: Z c= ( dom f);

      then

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

      for x st x in Z holds ( sin * f) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A9: f is_differentiable_in x by A8, FDIFF_1: 9;

         sin is_differentiable_in (f . x) by SIN_COS: 64;

        hence thesis by A9, FDIFF_2: 13;

      end;

      then

       A10: ( sin * f) is_differentiable_on Z by A6, FDIFF_1: 9;

      

       A11: for x st x in Z holds ((( sin * f) `| Z) . x) = (n * ( cos . (n * x)))

      proof

        let x;

        

         A12: sin is_differentiable_in (f . x) by SIN_COS: 64;

        assume

         A13: x in Z;

        then f is_differentiable_in x by A8, FDIFF_1: 9;

        

        then ( diff (( sin * f),x)) = (( diff ( sin ,(f . x))) * ( diff (f,x))) by A12, FDIFF_2: 13

        .= (( cos . (f . x)) * ( diff (f,x))) by SIN_COS: 64

        .= (( cos . (n * x)) * ( diff (f,x))) by A3, A13

        .= (( cos . (n * x)) * ((f `| Z) . x)) by A8, A13, FDIFF_1:def 7

        .= (n * ( cos . (n * x))) by A7, A4, A13, FDIFF_1: 23;

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

      end;

      

       A14: Z c= ( dom (( #Z n) * cos )) by A5, XBOOLE_1: 18;

      now

        let x;

        assume x in Z;

         cos is_differentiable_in x by SIN_COS: 63;

        hence (( #Z n) * cos ) is_differentiable_in x by TAYLOR_1: 3;

      end;

      then

       A15: (( #Z n) * cos ) is_differentiable_on Z by A14, FDIFF_1: 9;

      

       A16: for x st x in Z holds (((( #Z n) * cos ) `| Z) . x) = ( - ((n * (( cos . x) #Z (n - 1))) * ( sin . x)))

      proof

        let x;

         cos is_differentiable_in x by SIN_COS: 63;

        

        then

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

        .= ((n * (( cos . x) #Z (n - 1))) * ( - ( sin . x))) by SIN_COS: 63

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

        assume x in Z;

        hence thesis by A15, A17, FDIFF_1:def 7;

      end;

      now

        let x;

        

         A18: (n - 1) is Element of NAT by A2, NAT_1: 21;

        assume

         A19: x in Z;

        

        then (((( sin * f) (#) (( #Z n) * cos )) `| Z) . x) = ((((( #Z n) * cos ) . x) * ( diff (( sin * f),x))) + ((( sin * f) . x) * ( diff ((( #Z n) * cos ),x)))) by A1, A10, A15, FDIFF_1: 21

        .= (((( #Z n) . ( cos . x)) * ( diff (( sin * f),x))) + ((( sin * f) . x) * ( diff ((( #Z n) * cos ),x)))) by A14, A19, FUNCT_1: 12

        .= (((( cos . x) #Z n) * ( diff (( sin * f),x))) + ((( sin * f) . x) * ( diff ((( #Z n) * cos ),x)))) by TAYLOR_1:def 1

        .= (((( cos . x) #Z n) * ((( sin * f) `| Z) . x)) + ((( sin * f) . x) * ( diff ((( #Z n) * cos ),x)))) by A10, A19, FDIFF_1:def 7

        .= (((( cos . x) #Z n) * (n * ( cos . (n * x)))) + ((( sin * f) . x) * ( diff ((( #Z n) * cos ),x)))) by A11, A19

        .= (((( cos . x) #Z n) * (n * ( cos . (n * x)))) + (( sin . (f . x)) * ( diff ((( #Z n) * cos ),x)))) by A6, A19, FUNCT_1: 12

        .= (((( cos . x) #Z n) * (n * ( cos . (n * x)))) + (( sin . (n * x)) * ( diff ((( #Z n) * cos ),x)))) by A3, A19

        .= (((( cos . x) #Z n) * (n * ( cos . (n * x)))) + (( sin . (n * x)) * (((( #Z n) * cos ) `| Z) . x))) by A15, A19, FDIFF_1:def 7

        .= (((( cos . x) #Z ((n - 1) + 1)) * (n * ( cos . (n * x)))) + (( sin . (n * x)) * ( - ((n * (( cos . x) #Z (n - 1))) * ( sin . x))))) by A16, A19

        .= ((((( cos . x) #Z (n - 1)) * (( cos . x) #Z 1)) * (n * ( cos . (n * x)))) + (( sin . (n * x)) * ( - ((n * (( cos . x) #Z (n - 1))) * ( sin . x))))) by A18, TAYLOR_1: 1

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

        .= ((((( cos . x) #Z (n - 1)) * ( cos . x)) * (n * ( cos . (n * x)))) - (((( sin . (n * x)) * n) * (( cos . x) #Z (n - 1))) * ( sin . x))) by PREPOWER: 35

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

        .= ((n * (( cos . x) #Z (n - 1))) * ( cos . (x + (n * x)))) by SIN_COS: 74

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

        hence (((( sin * f) (#) (( #Z n) * cos )) `| Z) . x) = ((n * (( cos . x) #Z (n - 1))) * ( cos . ((n + 1) * x)));

      end;

      hence thesis by A1, A10, A15, FDIFF_1: 21;

    end;

    theorem :: FDIFF_5:14

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

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

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

      

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

      

       A4: sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

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

      then

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

      now

        let x;

        assume

         A6: x in Z;

        

        hence ((((f ^ ) (#) sin ) `| Z) . x) = ((( sin . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( sin ,x)))) by A2, A3, A4, FDIFF_1: 21

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

        .= ((( sin . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( sin ,x)))) by A1, A6, Th4

        .= ((( sin . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( cos . x))) by SIN_COS: 64

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

        .= ((( sin . x) * ( - (1 / (x ^2 )))) + ((1 * (x " )) * ( cos . x))) by A6, FUNCT_1: 18

        .= (( - ((1 / (x ^2 )) * ( sin . x))) + ((1 / x) * ( cos . x))) by XCMPLX_0:def 9

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

      end;

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

    end;

    theorem :: FDIFF_5:15

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

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom ((( id Z) ^ ) (#) cos ));

      

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

      

       A4: cos is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 67;

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

      then

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

      now

        let x;

        assume

         A6: x in Z;

        

        hence ((((f ^ ) (#) cos ) `| Z) . x) = ((( cos . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff ( cos ,x)))) by A2, A3, A4, FDIFF_1: 21

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

        .= ((( cos . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff ( cos ,x)))) by A1, A6, Th4

        .= ((( cos . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( - ( sin . x)))) by SIN_COS: 63

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

        .= ((( cos . x) * ( - (1 / (x ^2 )))) + ((1 * (x " )) * ( - ( sin . x)))) by A6, FUNCT_1: 18

        .= (( - ((1 / (x ^2 )) * ( cos . x))) + ((1 / x) * ( - ( sin . x)))) by XCMPLX_0:def 9

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

      end;

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

    end;

    theorem :: FDIFF_5:16

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

    proof

      assume

       A1: Z c= ( dom ( sin + ( #R (1 / 2))));

      then Z c= (( dom ( #R (1 / 2))) /\ ( dom sin )) by VALUED_1:def 1;

      then

       A2: Z c= ( dom ( #R (1 / 2))) by XBOOLE_1: 18;

      then

       A3: ( #R (1 / 2)) is_differentiable_on Z by Lm3;

      

       A4: sin is_differentiable_on Z by FDIFF_1: 26, SIN_COS: 68;

      now

        let x;

        assume

         A5: x in Z;

        

        then ((( sin + ( #R (1 / 2))) `| Z) . x) = (( diff ( sin ,x)) + ( diff (( #R (1 / 2)),x))) by A1, A3, A4, FDIFF_1: 18

        .= (( cos . x) + ( diff (( #R (1 / 2)),x))) by SIN_COS: 64

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

        .= (( cos . x) + ((1 / 2) * (x #R ( - (1 / 2))))) by A2, A5, Lm3;

        hence ((( sin + ( #R (1 / 2))) `| Z) . x) = (( cos . x) + ((1 / 2) * (x #R ( - (1 / 2)))));

      end;

      hence thesis by A1, A3, A4, FDIFF_1: 18;

    end;

    theorem :: FDIFF_5:17

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

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom (g (#) ( sin * (f ^ )))) and

       A3: g = ( #Z 2);

      

       A4: for x st x in Z holds g is_differentiable_in x by A3, TAYLOR_1: 2;

      

       A5: Z c= (( dom g) /\ ( dom ( sin * (f ^ )))) by A2, VALUED_1:def 4;

      then Z c= ( dom g) by XBOOLE_1: 18;

      then

       A6: g is_differentiable_on Z by A4, FDIFF_1: 9;

      

       A7: for x st x in Z holds ((g `| Z) . x) = (2 * x)

      proof

        let x;

        assume

         A8: x in Z;

        ( diff (g,x)) = (2 * (x #Z (2 - 1))) by A3, TAYLOR_1: 2

        .= (2 * x) by PREPOWER: 35;

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

      end;

      

       A9: ( sin * (f ^ )) is_differentiable_on Z by A1, Th5;

      

       A10: Z c= ( dom ( sin * (f ^ ))) by A5, XBOOLE_1: 18;

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

      then

       A11: Z c= ( dom (f ^ ));

      now

        let x;

        assume

         A12: x in Z;

        

        then (((g (#) ( sin * (f ^ ))) `| Z) . x) = (((( sin * (f ^ )) . x) * ( diff (g,x))) + ((g . x) * ( diff (( sin * (f ^ )),x)))) by A2, A9, A6, FDIFF_1: 21

        .= (((( sin * (f ^ )) . x) * ((g `| Z) . x)) + ((g . x) * ( diff (( sin * (f ^ )),x)))) by A6, A12, FDIFF_1:def 7

        .= (((( sin * (f ^ )) . x) * (2 * x)) + ((g . x) * ( diff (( sin * (f ^ )),x)))) by A7, A12

        .= (((( sin * (f ^ )) . x) * (2 * x)) + ((x #Z 2) * ( diff (( sin * (f ^ )),x)))) by A3, TAYLOR_1:def 1

        .= (((( sin * (f ^ )) . x) * (2 * x)) + ((x #Z 2) * ((( sin * (f ^ )) `| Z) . x))) by A9, A12, FDIFF_1:def 7

        .= (((( sin * (f ^ )) . x) * (2 * x)) + ((x #Z 2) * ( - ((1 / (x ^2 )) * ( cos . (1 / x)))))) by A1, A12, Th5

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

        .= (((( sin * (f ^ )) . x) * (2 * x)) - (((x #Z 1) * (x #Z 1)) * ((1 / (x ^2 )) * ( cos . (1 / x))))) by TAYLOR_1: 1

        .= (((( sin * (f ^ )) . x) * (2 * x)) - ((x * (x #Z 1)) * ((1 / (x ^2 )) * ( cos . (1 / x))))) by PREPOWER: 35

        .= (((( sin * (f ^ )) . x) * (2 * x)) - ((x * x) * (((1 * 1) / (x * x)) * ( cos . (1 / x))))) by PREPOWER: 35

        .= (((( sin * (f ^ )) . x) * (2 * x)) - ((x * x) * (((1 / x) * (1 / x)) * ( cos . (1 / x))))) by XCMPLX_1: 102

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

        .= (((( sin * (f ^ )) . x) * (2 * x)) - (((x * (1 / x)) * 1) * ( cos . (1 / x)))) by A1, A12, XCMPLX_1: 106

        .= (((( sin * (f ^ )) . x) * (2 * x)) - ((1 * 1) * ( cos . (1 / x)))) by A1, A12, XCMPLX_1: 106

        .= ((( sin . ((f ^ ) . x)) * (2 * x)) - ( cos . (1 / x))) by A10, A12, FUNCT_1: 12

        .= ((( sin . ((f . x) " )) * (2 * x)) - ( cos . (1 / x))) by A11, A12, RFUNCT_1:def 2

        .= ((( sin . (1 * (x " ))) * (2 * x)) - ( cos . (1 / x))) by A12, FUNCT_1: 18

        .= (((2 * x) * ( sin . (1 / x))) - ( cos . (1 / x))) by XCMPLX_0:def 9;

        hence (((g (#) ( sin * (f ^ ))) `| Z) . x) = (((2 * x) * ( sin . (1 / x))) - ( cos . (1 / x)));

      end;

      hence thesis by A2, A9, A6, FDIFF_1: 21;

    end;

    theorem :: FDIFF_5:18

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

    proof

      set f = ( id Z);

      assume that

       A1: not 0 in Z and

       A2: Z c= ( dom (g (#) ( cos * (f ^ )))) and

       A3: g = ( #Z 2);

      

       A4: for x st x in Z holds g is_differentiable_in x by A3, TAYLOR_1: 2;

      

       A5: Z c= (( dom g) /\ ( dom ( cos * (f ^ )))) by A2, VALUED_1:def 4;

      then

       A6: Z c= ( dom ( cos * (f ^ ))) by XBOOLE_1: 18;

      then

       A7: ( cos * (f ^ )) is_differentiable_on Z by A1, Th6;

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

      then

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

      

       A9: for x st x in Z holds ((g `| Z) . x) = (2 * x)

      proof

        let x;

        assume

         A10: x in Z;

        ( diff (g,x)) = (2 * (x #Z (2 - 1))) by A3, TAYLOR_1: 2

        .= (2 * x) by PREPOWER: 35;

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

      end;

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

      then

       A11: Z c= ( dom (f ^ ));

      now

        let x;

        assume

         A12: x in Z;

        

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

        .= (((( cos * (f ^ )) . x) * ((g `| Z) . x)) + ((g . x) * ( diff (( cos * (f ^ )),x)))) by A8, A12, FDIFF_1:def 7

        .= (((( cos * (f ^ )) . x) * (2 * x)) + ((g . x) * ( diff (( cos * (f ^ )),x)))) by A9, A12

        .= (((( cos * (f ^ )) . x) * (2 * x)) + ((x #Z 2) * ( diff (( cos * (f ^ )),x)))) by A3, TAYLOR_1:def 1

        .= (((( cos * (f ^ )) . x) * (2 * x)) + ((x #Z 2) * ((( cos * (f ^ )) `| Z) . x))) by A7, A12, FDIFF_1:def 7

        .= (((( cos * (f ^ )) . x) * (2 * x)) + ((x #Z (1 + 1)) * ((1 / (x ^2 )) * ( sin . (1 / x))))) by A1, A6, A12, Th6

        .= (((( cos * (f ^ )) . x) * (2 * x)) + (((x #Z 1) * (x #Z 1)) * ((1 / (x ^2 )) * ( sin . (1 / x))))) by TAYLOR_1: 1

        .= (((( cos * (f ^ )) . x) * (2 * x)) + ((x * (x #Z 1)) * ((1 / (x ^2 )) * ( sin . (1 / x))))) by PREPOWER: 35

        .= (((( cos * (f ^ )) . x) * (2 * x)) + ((x * x) * (((1 * 1) / (x * x)) * ( sin . (1 / x))))) by PREPOWER: 35

        .= (((( cos * (f ^ )) . x) * (2 * x)) + ((x * x) * (((1 / x) * (1 / x)) * ( sin . (1 / x))))) by XCMPLX_1: 102

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

        .= (((( cos * (f ^ )) . x) * (2 * x)) + (((x * (1 / x)) * 1) * ( sin . (1 / x)))) by A1, A12, XCMPLX_1: 106

        .= (((( cos * (f ^ )) . x) * (2 * x)) + ((1 * 1) * ( sin . (1 / x)))) by A1, A12, XCMPLX_1: 106

        .= ((( cos . ((f ^ ) . x)) * (2 * x)) + ( sin . (1 / x))) by A6, A12, FUNCT_1: 12

        .= ((( cos . ((f . x) " )) * (2 * x)) + ( sin . (1 / x))) by A11, A12, RFUNCT_1:def 2

        .= ((( cos . (1 * (x " ))) * (2 * x)) + ( sin . (1 / x))) by A12, FUNCT_1: 18

        .= (((2 * x) * ( cos . (1 / x))) + ( sin . (1 / x))) by XCMPLX_0:def 9;

        hence (((g (#) ( cos * (f ^ ))) `| Z) . x) = (((2 * x) * ( cos . (1 / x))) + ( sin . (1 / x)));

      end;

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

    end;

    

     Lm5: x in ( dom ln ) implies x > 0 by TAYLOR_1: 18, XXREAL_1: 4;

    theorem :: FDIFF_5:19

    

     Th19: Z c= ( dom ln ) implies ln is_differentiable_on Z & for x st x in Z holds (( ln `| Z) . x) = (1 / x)

    proof

      assume

       A1: Z c= ( dom ln );

      then

       A2: for x st x in Z holds ln is_differentiable_in x by Lm5, TAYLOR_1: 18;

      then

       A3: ln is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds (( ln `| Z) . x) = (1 / x)

      proof

        let x;

        assume

         A4: x in Z;

        then ( diff ( ln ,x)) = (1 / x) by A1, TAYLOR_1: 18;

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

      end;

      hence thesis by A1, A2, FDIFF_1: 9;

    end;

    theorem :: FDIFF_5:20

    Z c= ( dom (( id Z) (#) ln )) implies (( id Z) (#) ln ) is_differentiable_on Z & for x st x in Z holds (((( id Z) (#) ln ) `| Z) . x) = (1 + ( ln . x))

    proof

      set f = ln ;

      assume

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

      then

       A2: Z c= (( dom ( id Z)) /\ ( dom f)) by VALUED_1:def 4;

      then

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

      

       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 A3, FDIFF_1: 23;

      

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

      then

       A7: f is_differentiable_on Z by Th19;

      for x st x in Z holds (((( id Z) (#) f) `| Z) . x) = (1 + ( ln . x))

      proof

        let x;

        assume

         A8: x in Z;

        then

         A9: x <> 0 by A6, TAYLOR_1: 18, XXREAL_1: 4;

        (((( id Z) (#) f) `| Z) . x) = (((( id Z) . x) * ( diff (f,x))) + ((f . x) * ( diff (( id Z),x)))) by A1, A5, A7, A8, FDIFF_1: 21

        .= (((( id Z) . x) * ((f `| Z) . x)) + ((f . x) * ( diff (( id Z),x)))) by A7, A8, FDIFF_1:def 7

        .= (((( id Z) . x) * (1 / x)) + ((f . x) * ( diff (( id Z),x)))) by A6, A8, Th19

        .= ((x * (1 / x)) + ((f . x) * ( diff (( id Z),x)))) by A8, FUNCT_1: 18

        .= ((x * (1 / x)) + ((f . x) * ((( id Z) `| Z) . x))) by A5, A8, FDIFF_1:def 7

        .= ((x * (1 / x)) + ((f . x) * 1)) by A3, A4, A8, FDIFF_1: 23

        .= (1 + ( ln . x)) by A9, XCMPLX_1: 106;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_5:21

    Z c= ( dom (g (#) ln )) & g = ( #Z 2) & (for x st x in Z holds x > 0 ) implies (g (#) ln ) is_differentiable_on Z & for x st x in Z holds (((g (#) ln ) `| Z) . x) = (x + ((2 * x) * ( ln . x)))

    proof

      set f = ln ;

      assume that

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

       A2: g = ( #Z 2) and

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

      

       A4: for x st x in Z holds g is_differentiable_in x by A2, TAYLOR_1: 2;

      

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

      then

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

      then

       A7: f is_differentiable_on Z by Th19;

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

      then

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

      

       A9: for x st x in Z holds ((g `| Z) . x) = (2 * x)

      proof

        let x;

        assume

         A10: x in Z;

        ( diff (g,x)) = (2 * (x #Z (2 - 1))) by A2, TAYLOR_1: 2

        .= (2 * x) by PREPOWER: 35;

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

      end;

      now

        let x;

        assume

         A11: x in Z;

        then

         A12: x <> 0 by A3;

        (((g (#) f) `| Z) . x) = (((g . x) * ( diff (f,x))) + ((f . x) * ( diff (g,x)))) by A1, A8, A7, A11, FDIFF_1: 21

        .= (((g . x) * ((f `| Z) . x)) + ((f . x) * ( diff (g,x)))) by A7, A11, FDIFF_1:def 7

        .= (((g . x) * (1 / x)) + ((f . x) * ( diff (g,x)))) by A6, A11, Th19

        .= (((x #Z 2) * (1 / x)) + ((f . x) * ( diff (g,x)))) by A2, TAYLOR_1:def 1

        .= (((x #Z 2) * (1 / x)) + ((f . x) * ((g `| Z) . x))) by A8, A11, FDIFF_1:def 7

        .= (((x #Z (1 + 1)) * (1 / x)) + ((2 * x) * ( ln . x))) by A9, A11

        .= ((((x #Z 1) * (x #Z 1)) * (1 / x)) + ((2 * x) * ( ln . x))) by TAYLOR_1: 1

        .= ((((x #Z 1) * x) * (1 / x)) + ((2 * x) * ( ln . x))) by PREPOWER: 35

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

        .= ((x * (x * (1 / x))) + ((2 * x) * ( ln . x)))

        .= ((x * 1) + ((2 * x) * ( ln . x))) by A12, XCMPLX_1: 106

        .= (x + ((2 * x) * ( ln . x)));

        hence (((g (#) f) `| Z) . x) = (x + ((2 * x) * ( ln . x)));

      end;

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

    end;

    theorem :: FDIFF_5:22

    

     Th22: Z c= ( dom ((f1 + f2) / (f1 - f2))) & (for x st x in Z holds (f1 . x) = a) & f2 = ( #Z 2) & (for x st x in Z holds ((f1 - f2) . x) > 0 ) implies ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & for x st x in Z holds ((((f1 + f2) / (f1 - f2)) `| Z) . x) = (((4 * a) * x) / ((a - (x |^ 2)) |^ 2))

    proof

      assume that

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

       A2: for x st x in Z holds (f1 . x) = a and

       A3: f2 = ( #Z 2) and

       A4: for x st x in Z holds ((f1 - f2) . x) > 0 ;

      

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

      then

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

      then

       A7: (f1 + f2) is_differentiable_on Z by A2, A3, Lm1;

      

       A8: Z c= ( dom (f1 - f2)) by A5, XBOOLE_1: 1;

      then

       A9: (f1 - f2) is_differentiable_on Z by A2, A3, Lm2;

      

       A10: for x st x in Z holds ((f1 - f2) . x) <> 0 by A4;

      then

       A11: ((f1 + f2) / (f1 - f2)) is_differentiable_on Z by A7, A9, FDIFF_2: 21;

      for x st x in Z holds ((((f1 + f2) / (f1 - f2)) `| Z) . x) = (((4 * a) * x) / ((a - (x |^ 2)) |^ 2))

      proof

        let x;

        assume

         A12: x in Z;

        then

         A13: (f1 . x) = a by A2;

        

         A14: ((f1 - f2) . x) <> 0 by A4, A12;

        (f1 + f2) is_differentiable_in x & (f1 - f2) is_differentiable_in x by A7, A9, A12, FDIFF_1: 9;

        

        then ( diff (((f1 + f2) / (f1 - f2)),x)) = (((( diff ((f1 + f2),x)) * ((f1 - f2) . x)) - (( diff ((f1 - f2),x)) * ((f1 + f2) . x))) / (((f1 - f2) . x) ^2 )) by A14, FDIFF_2: 14

        .= (((( diff ((f1 + f2),x)) * ((f1 . x) - (f2 . x))) - (( diff ((f1 - f2),x)) * ((f1 + f2) . x))) / (((f1 - f2) . x) ^2 )) by A8, A12, VALUED_1: 13

        .= (((( diff ((f1 + f2),x)) * ((f1 . x) - (f2 . x))) - (( diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 - f2) . x) ^2 )) by A6, A12, VALUED_1:def 1

        .= (((( diff ((f1 + f2),x)) * ((f1 . x) - (f2 . x))) - (( diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2 )) by A8, A12, VALUED_1: 13

        .= ((((((f1 + f2) `| Z) . x) * ((f1 . x) - (f2 . x))) - (( diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2 )) by A7, A12, FDIFF_1:def 7

        .= ((((2 * x) * ((f1 . x) - (f2 . x))) - (( diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2 )) by A2, A3, A6, A12, Lm1

        .= ((((2 * x) * ((f1 . x) - (f2 . x))) - ((((f1 - f2) `| Z) . x) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2 )) by A9, A12, FDIFF_1:def 7

        .= ((((2 * x) * ((f1 . x) - (f2 . x))) - (( - (2 * x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2 )) by A2, A3, A8, A12, Lm2

        .= (((4 * x) * a) / ((a - (x #Z 2)) ^2 )) by A3, A13, TAYLOR_1:def 1

        .= (((4 * x) * a) / ((a - (x |^ 2)) ^2 )) by PREPOWER: 36

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

        .= (((4 * x) * a) / ((a - (x |^ 2)) |^ (1 + 1))) by NEWTON: 6

        .= (((4 * a) * x) / ((a - (x |^ 2)) |^ 2));

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

      end;

      hence thesis by A7, A9, A10, FDIFF_2: 21;

    end;

    theorem :: FDIFF_5:23

    Z c= ( dom ( ln * ((f1 + f2) / (f1 - f2)))) & (for x st x in Z holds (f1 . x) = a) & f2 = ( #Z 2) & (for x st x in Z holds ((f1 - f2) . x) > 0 ) & (for x st x in Z holds ((f1 + f2) . x) > 0 ) implies ( ln * ((f1 + f2) / (f1 - f2))) is_differentiable_on Z & for x st x in Z holds ((( ln * ((f1 + f2) / (f1 - f2))) `| Z) . x) = (((4 * a) * x) / ((a |^ 2) - (x |^ 4)))

    proof

      assume that

       A1: Z c= ( dom ( ln * ((f1 + f2) / (f1 - f2)))) and

       A2: for x st x in Z holds (f1 . x) = a and

       A3: f2 = ( #Z 2) and

       A4: for x st x in Z holds ((f1 - f2) . x) > 0 and

       A5: for x st x in Z holds ((f1 + f2) . x) > 0 ;

      for y be object st y in Z holds y in ( dom ((f1 + f2) / (f1 - f2))) by A1, FUNCT_1: 11;

      then

       A6: Z c= ( dom ((f1 + f2) / (f1 - f2)));

      then

       A7: ((f1 + f2) / (f1 - f2)) is_differentiable_on Z by A2, A3, A4, Th22;

      

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

      then

       A9: Z c= ( dom (f1 + f2)) by XBOOLE_1: 18;

      

       A10: Z c= ( dom (f1 - f2)) by A8, XBOOLE_1: 1;

      

       A11: for x st x in Z holds (((f1 + f2) / (f1 - f2)) . x) > 0

      proof

        let x;

        assume

         A12: x in Z;

        then x in ( dom ((f1 + f2) / (f1 - f2))) by A1, FUNCT_1: 11;

        

        then

         A13: (((f1 + f2) / (f1 - f2)) . x) = (((f1 + f2) . x) * (((f1 - f2) . x) " )) by RFUNCT_1:def 1

        .= (((f1 + f2) . x) / ((f1 - f2) . x)) by XCMPLX_0:def 9;

        ((f1 + f2) . x) > 0 & ((f1 - f2) . x) > 0 by A4, A5, A12;

        hence thesis by A13, XREAL_1: 139;

      end;

      

       A14: for x st x in Z holds ( ln * ((f1 + f2) / (f1 - f2))) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ((f1 + f2) / (f1 - f2)) is_differentiable_in x & (((f1 + f2) / (f1 - f2)) . x) > 0 by A7, A11, FDIFF_1: 9;

        hence thesis by TAYLOR_1: 20;

      end;

      then

       A15: ( ln * ((f1 + f2) / (f1 - f2))) is_differentiable_on Z by A1, FDIFF_1: 9;

      for x st x in Z holds ((( ln * ((f1 + f2) / (f1 - f2))) `| Z) . x) = (((4 * a) * x) / ((a |^ 2) - (x |^ 4)))

      proof

        let x;

        assume

         A16: x in Z;

        then

         A17: x in ( dom ((f1 + f2) / (f1 - f2))) by A1, FUNCT_1: 11;

        

         A18: ((f1 - f2) . x) <> 0 by A4, A16;

        

         A19: (f1 . x) = a by A2, A16;

        ((f1 + f2) / (f1 - f2)) is_differentiable_in x & (((f1 + f2) / (f1 - f2)) . x) > 0 by A7, A11, A16, FDIFF_1: 9;

        

        then ( diff (( ln * ((f1 + f2) / (f1 - f2))),x)) = (( diff (((f1 + f2) / (f1 - f2)),x)) / (((f1 + f2) / (f1 - f2)) . x)) by TAYLOR_1: 20

        .= (((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) / (f1 - f2)) . x)) by A7, A16, FDIFF_1:def 7

        .= (((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))) by A17, RFUNCT_1:def 1

        .= ((((4 * a) * x) / (((f1 . x) - (x |^ 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))) by A2, A3, A4, A6, A16, A19, Th22

        .= ((((4 * a) * x) / (((f1 . x) - (x #Z 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))) by PREPOWER: 36

        .= ((((4 * a) * x) / (((f1 . x) - (f2 . x)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))) by A3, TAYLOR_1:def 1

        .= ((((4 * a) * x) / (((f1 - f2) . x) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) " ))) by A10, A16, VALUED_1: 13

        .= ((((4 * a) * x) / (((f1 - f2) . x) |^ (1 + 1))) / (((f1 + f2) . x) / ((f1 - f2) . x))) by XCMPLX_0:def 9

        .= ((((4 * a) * x) / ((((f1 - f2) . x) |^ 1) * ((f1 - f2) . x))) / (((f1 + f2) . x) / ((f1 - f2) . x))) by NEWTON: 6

        .= ((((4 * a) * x) / (((f1 - f2) . x) * ((f1 - f2) . x))) / (((f1 + f2) . x) / ((f1 - f2) . x)))

        .= (((((4 * a) * x) / ((f1 - f2) . x)) / ((f1 - f2) . x)) / (((f1 + f2) . x) / ((f1 - f2) . x))) by XCMPLX_1: 78

        .= (((((4 * a) * x) / ((f1 - f2) . x)) / (((f1 + f2) . x) / ((f1 - f2) . x))) / ((f1 - f2) . x)) by XCMPLX_1: 48

        .= ((((4 * a) * x) / ((f1 + f2) . x)) / ((f1 - f2) . x)) by A18, XCMPLX_1: 55

        .= (((4 * a) * x) / (((f1 + f2) . x) * ((f1 - f2) . x))) by XCMPLX_1: 78

        .= (((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 - f2) . x))) by A9, A16, VALUED_1:def 1

        .= (((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 . x) - (f2 . x)))) by A10, A16, VALUED_1: 13

        .= (((4 * a) * x) / ((a * a) - ((f2 . x) * (f2 . x)))) by A19

        .= (((4 * a) * x) / ((a * a) - ((x #Z 2) * (f2 . x)))) by A3, TAYLOR_1:def 1

        .= (((4 * a) * x) / ((a * a) - ((x #Z 2) * (x #Z 2)))) by A3, TAYLOR_1:def 1

        .= (((4 * a) * x) / (((a |^ 1) * a) - ((x #Z 2) * (x #Z 2))))

        .= (((4 * a) * x) / ((a |^ (1 + 1)) - ((x #Z 2) * (x #Z 2)))) by NEWTON: 6

        .= (((4 * a) * x) / ((a |^ (1 + 1)) - ((x |^ 2) * (x #Z 2)))) by PREPOWER: 36

        .= (((4 * a) * x) / ((a |^ 2) - ((x |^ 2) * (x |^ 2)))) by PREPOWER: 36

        .= (((4 * a) * x) / ((a |^ 2) - (x |^ (2 + 2)))) by NEWTON: 8

        .= (((4 * a) * x) / ((a |^ 2) - (x |^ 4)));

        hence thesis by A15, A16, FDIFF_1:def 7;

      end;

      hence thesis by A1, A14, FDIFF_1: 9;

    end;

    theorem :: FDIFF_5:24

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

    proof

      set f = ( id Z), g = ln ;

      assume that

       A1: Z c= ( dom ((f ^ ) (#) g)) and

       A2: for x st x in Z holds x > 0 ;

      

       A3: not 0 in Z by A2;

      then

       A4: (f ^ ) is_differentiable_on Z by Th4;

      

       A5: Z c= (( dom (f ^ )) /\ ( dom g)) by A1, VALUED_1:def 4;

      then

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

      then

       A7: g is_differentiable_on Z by Th19;

      

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

      now

        let x;

        assume

         A9: x in Z;

        

        then ((((f ^ ) (#) g) `| Z) . x) = (((g . x) * ( diff ((f ^ ),x))) + (((f ^ ) . x) * ( diff (g,x)))) by A1, A4, A7, FDIFF_1: 21

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

        .= (((g . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ( diff (g,x)))) by A3, A9, Th4

        .= (((g . x) * ( - (1 / (x ^2 )))) + (((f ^ ) . x) * ((g `| Z) . x))) by A7, A9, FDIFF_1:def 7

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

        .= (((g . x) * ( - (1 / (x ^2 )))) + (((f . x) " ) * (1 / x))) by A8, A9, RFUNCT_1:def 2

        .= (((g . x) * ( - (1 / (x ^2 )))) + ((1 * (x " )) * (1 / x))) by A9, FUNCT_1: 18

        .= (( - ((1 / (x ^2 )) * (g . x))) + ((1 / x) * (1 / x))) by XCMPLX_0:def 9

        .= (( - ((1 / (x ^2 )) * ( ln . x))) + (1 / (x ^2 ))) by XCMPLX_1: 102

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

        hence ((((f ^ ) (#) g) `| Z) . x) = ((1 / (x ^2 )) * (1 - ( ln . x)));

      end;

      hence thesis by A1, A4, A7, FDIFF_1: 21;

    end;

    theorem :: FDIFF_5:25

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

    proof

      set f = ln ;

      assume that

       A1: Z c= ( dom ( ln ^ )) and

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

      ( dom (f ^ )) c= ( dom f) by RFUNCT_1: 1;

      then

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

      then

       A4: f is_differentiable_on Z by Th19;

      then

       A5: (f ^ ) is_differentiable_on Z by A2, FDIFF_2: 22;

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

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: (f . x) <> 0 & f is_differentiable_in x by A2, A4, FDIFF_1: 9;

        (((f ^ ) `| Z) . x) = ( diff ((f ^ ),x)) by A5, A6, FDIFF_1:def 7

        .= ( - (( diff (f,x)) / ((f . x) ^2 ))) by A7, FDIFF_2: 15

        .= ( - (((f `| Z) . x) / ((f . x) ^2 ))) by A4, A6, FDIFF_1:def 7

        .= ( - ((1 / x) / (( ln . x) ^2 ))) by A3, A6, Th19

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

        hence thesis;

      end;

      hence thesis by A2, A4, FDIFF_2: 22;

    end;