fdiff_10.miz



    begin

    reserve x for Real,

Z for open Subset of REAL ;

    theorem :: FDIFF_10:1

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

    proof

      assume

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

      

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

      proof

        let x;

        assume x in Z;

        then ( cot . x) in ( dom tan ) by A1, FUNCT_1: 11;

        hence thesis by FDIFF_8: 1;

      end;

      

       A3: 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 FDIFF_8: 2;

      end;

      

       A4: for x st x in Z holds ( tan * cot ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

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

        then

         A6: tan is_differentiable_in ( cot . x) by FDIFF_7: 46;

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

        then cot is_differentiable_in x by FDIFF_7: 47;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        then

         A10: tan is_differentiable_in ( cot . x) by FDIFF_7: 46;

        

         A11: ( sin . x) <> 0 by A3, A8;

        then cot is_differentiable_in x by FDIFF_7: 47;

        

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

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

        .= ((1 / (( cos . ( cot . x)) ^2 )) * ( - (1 / (( sin . x) ^2 )))) by A11, FDIFF_7: 47;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:2

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

    proof

      assume

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

      

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

      proof

        let x;

        assume x in Z;

        then ( tan . x) in ( dom tan ) by A1, FUNCT_1: 11;

        hence thesis by FDIFF_8: 1;

      end;

      

       A3: 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 FDIFF_8: 1;

      end;

      

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

      proof

        let x;

        assume

         A5: x in Z;

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

        then

         A6: tan is_differentiable_in ( tan . x) by FDIFF_7: 46;

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

        then tan is_differentiable_in x by FDIFF_7: 46;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        then

         A10: tan is_differentiable_in ( tan . x) by FDIFF_7: 46;

        

         A11: ( cos . x) <> 0 by A3, A8;

        then tan is_differentiable_in x by FDIFF_7: 46;

        

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

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

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

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:3

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

    proof

      assume

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

      

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

      proof

        let x;

        assume x in Z;

        then ( cot . x) in ( dom cot ) by A1, FUNCT_1: 11;

        hence thesis by FDIFF_8: 2;

      end;

      

       A3: 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 FDIFF_8: 2;

      end;

      

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

      proof

        let x;

        assume

         A5: x in Z;

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

        then

         A6: cot is_differentiable_in ( cot . x) by FDIFF_7: 47;

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

        then cot is_differentiable_in x by FDIFF_7: 47;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        then

         A10: cot is_differentiable_in ( cot . x) by FDIFF_7: 47;

        

         A11: ( sin . x) <> 0 by A3, A8;

        then cot is_differentiable_in x by FDIFF_7: 47;

        

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

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

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

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:4

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

    proof

      assume

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

      

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

      proof

        let x;

        assume x in Z;

        then ( tan . x) in ( dom cot ) by A1, FUNCT_1: 11;

        hence thesis by FDIFF_8: 2;

      end;

      

       A3: 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 FDIFF_8: 1;

      end;

      

       A4: for x st x in Z holds ( cot * tan ) is_differentiable_in x

      proof

        let x;

        assume

         A5: x in Z;

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

        then

         A6: cot is_differentiable_in ( tan . x) by FDIFF_7: 47;

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

        then tan is_differentiable_in x by FDIFF_7: 46;

        hence thesis by A6, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        assume

         A8: x in Z;

        then

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

        then

         A10: cot is_differentiable_in ( tan . x) by FDIFF_7: 47;

        

         A11: ( cos . x) <> 0 by A3, A8;

        then tan is_differentiable_in x by FDIFF_7: 46;

        

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

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

        .= (( - (1 / (( sin . ( tan . x)) ^2 ))) * (1 / (( cos . x) ^2 ))) by A11, FDIFF_7: 46;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:5

    

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

    proof

      assume

       A1: Z c= ( dom ( tan - cot ));

      then

       A2: Z c= (( dom tan ) /\ ( dom cot )) by VALUED_1: 12;

      then

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

      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, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      

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

      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, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

      then

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

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

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( sin . x) <> 0 by A5, FDIFF_8: 2;

        

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

        ((( tan - cot ) `| Z) . x) = (( diff ( tan ,x)) - ( diff ( cot ,x))) by A1, A6, A4, A7, FDIFF_1: 19

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

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

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:6

    

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

    proof

      assume

       A1: Z c= ( dom ( tan + cot ));

      then

       A2: Z c= (( dom tan ) /\ ( dom cot )) by VALUED_1:def 1;

      then

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

      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, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

      then

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

      

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

      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, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

      then

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

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

      proof

        let x;

        assume

         A7: x in Z;

        then

         A8: ( sin . x) <> 0 by A5, FDIFF_8: 2;

        

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

        ((( tan + cot ) `| Z) . x) = (( diff ( tan ,x)) + ( diff ( cot ,x))) by A1, A6, A4, A7, FDIFF_1: 18

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

        .= ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))) by A8, FDIFF_7: 47;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:7

    ( sin * sin ) is_differentiable_on Z & for x st x in Z holds ((( sin * sin ) `| Z) . x) = (( cos . ( sin . x)) * ( cos . x))

    proof

      

       A1: for x st x in Z holds ( sin * sin ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        

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

         sin is_differentiable_in x by SIN_COS: 64;

        hence thesis by A2, FDIFF_2: 13;

      end;

      ( rng sin ) c= REAL ;

      then

       A3: ( dom ( sin * sin )) = REAL by RELAT_1: 27, SIN_COS: 24;

      then

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

      for x st x in Z holds ((( sin * sin ) `| Z) . x) = (( cos . ( sin . x)) * ( cos . x))

      proof

        let x;

        assume

         A5: x in Z;

        

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

         sin is_differentiable_in x by SIN_COS: 64;

        

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

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

        .= (( cos . ( sin . x)) * ( cos . x)) by SIN_COS: 64;

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

      end;

      hence thesis by A3, A1, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:8

    ( sin * cos ) is_differentiable_on Z & for x st x in Z holds ((( sin * cos ) `| Z) . x) = ( - (( cos . ( cos . x)) * ( sin . x)))

    proof

      

       A1: for x st x in Z holds ( sin * cos ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        

         A2: sin is_differentiable_in ( cos . x) by SIN_COS: 64;

         cos is_differentiable_in x by SIN_COS: 63;

        hence thesis by A2, FDIFF_2: 13;

      end;

      ( rng cos ) c= ( dom cos ) by SIN_COS: 24;

      then

       A3: ( dom ( sin * cos )) = REAL by RELAT_1: 27, SIN_COS: 24;

      then

       A4: ( sin * cos ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A5: x in Z;

        

         A6: sin is_differentiable_in ( cos . x) by SIN_COS: 64;

         cos is_differentiable_in x by SIN_COS: 63;

        

        then ( diff (( sin * cos ),x)) = (( diff ( sin ,( cos . x))) * ( diff ( cos ,x))) by A6, FDIFF_2: 13

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

        .= (( cos . ( cos . x)) * ( - ( sin . x))) by SIN_COS: 63;

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

      end;

      hence thesis by A3, A1, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:9

    ( cos * sin ) is_differentiable_on Z & for x st x in Z holds ((( cos * sin ) `| Z) . x) = ( - (( sin . ( sin . x)) * ( cos . x)))

    proof

      

       A1: for x st x in Z holds ( cos * sin ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        

         A2: cos is_differentiable_in ( sin . x) by SIN_COS: 63;

         sin is_differentiable_in x by SIN_COS: 64;

        hence thesis by A2, FDIFF_2: 13;

      end;

      ( rng sin ) c= ( dom sin ) by SIN_COS: 24;

      then

       A3: ( dom ( cos * sin )) = REAL by RELAT_1: 27, SIN_COS: 24;

      then

       A4: ( cos * sin ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A5: x in Z;

        

         A6: cos is_differentiable_in ( sin . x) by SIN_COS: 63;

         sin is_differentiable_in x by SIN_COS: 64;

        

        then ( diff (( cos * sin ),x)) = (( diff ( cos ,( sin . x))) * ( diff ( sin ,x))) by A6, FDIFF_2: 13

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

        .= (( - ( sin . ( sin . x))) * ( cos . x)) by SIN_COS: 64;

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

      end;

      hence thesis by A3, A1, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:10

    ( cos * cos ) is_differentiable_on Z & for x st x in Z holds ((( cos * cos ) `| Z) . x) = (( sin . ( cos . x)) * ( sin . x))

    proof

      

       A1: for x st x in Z holds ( cos * cos ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        

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

         cos is_differentiable_in x by SIN_COS: 63;

        hence thesis by A2, FDIFF_2: 13;

      end;

      ( rng cos ) c= REAL ;

      then

       A3: ( dom ( cos * cos )) = REAL by RELAT_1: 27, SIN_COS: 24;

      then

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

      for x st x in Z holds ((( cos * cos ) `| Z) . x) = (( sin . ( cos . x)) * ( sin . x))

      proof

        let x;

        assume

         A5: x in Z;

        

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

         cos is_differentiable_in x by SIN_COS: 63;

        

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

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

        .= (( - ( sin . ( cos . x))) * ( - ( sin . x))) by SIN_COS: 63;

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

      end;

      hence thesis by A3, A1, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:11

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

    proof

      

       A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      assume

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

      then

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

      then

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

      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, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

      then

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

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

      then

       A6: cos is_differentiable_on Z by A1, FDIFF_1: 9;

      

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

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A4, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

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

      proof

        let x;

        assume

         A8: x in Z;

        

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

        .= ((( cot . x) * ( - ( sin . x))) + (( cos . x) * ( diff ( cot ,x)))) by SIN_COS: 63

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

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

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

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

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:12

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

    proof

      

       A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      assume

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

      then

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

      then

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

      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, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

      then

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

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

      then

       A6: sin is_differentiable_on Z by A1, FDIFF_1: 9;

      

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

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

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

      proof

        let x;

        assume

         A8: x in Z;

        

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

        .= ((( cos . x) * ( tan . x)) + (( sin . x) * ( diff ( tan ,x)))) by SIN_COS: 64

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

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

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

        .= ((( sin . x) * 1) + (( sin . x) / (( cos . x) ^2 ))) by A4, A8, FDIFF_8: 1, XCMPLX_1: 60

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:13

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

    proof

      

       A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      assume

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

      then

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

      then

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

      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, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

      then

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

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

      then

       A6: sin is_differentiable_on Z by A1, FDIFF_1: 9;

      

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

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A4, FDIFF_8: 2;

        hence thesis by FDIFF_7: 47;

      end;

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

      proof

        let x;

        assume

         A8: x in Z;

        

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

        .= ((( cos . x) * ( cot . x)) + (( sin . x) * ( diff ( cot ,x)))) by SIN_COS: 64

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

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

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

        .= ((( cos . x) * ( cot . x)) - (1 / ( sin . x))) by A4, A8, FDIFF_8: 2, XCMPLX_1: 60;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:14

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

    proof

      

       A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      assume

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

      then

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

      then

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

      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, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

      then

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

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

      then

       A6: cos is_differentiable_on Z by A1, FDIFF_1: 9;

      

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

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A4, FDIFF_8: 1;

        hence thesis by FDIFF_7: 46;

      end;

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

      proof

        let x;

        assume

         A8: x in Z;

        

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

        .= ((( tan . x) * ( - ( sin . x))) + (( cos . x) * ( diff ( tan ,x)))) by SIN_COS: 63

        .= ((( tan . x) * ( - ( sin . x))) + (( cos . x) * (1 / (( cos . x) ^2 )))) by A7, A8

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

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

        .= (( - ((( sin . x) ^2 ) / ( cos . x))) + (1 / ( cos . x))) by A4, A8, FDIFF_8: 1, XCMPLX_1: 60;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:15

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

    proof

      

       A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      

       A2: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      assume

       A3: Z c= ( dom ( sin (#) cos ));

      then

       A4: Z c= (( dom sin ) /\ ( dom cos )) by VALUED_1:def 4;

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

      then

       A5: cos is_differentiable_on Z by A2, FDIFF_1: 9;

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

      then

       A6: sin is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume x in Z;

        

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

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

        .= ((( cos . x) * ( cos . x)) + (( sin . x) * ( - ( sin . x)))) by SIN_COS: 63

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

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:16

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

    proof

      

       A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      assume

       A2: Z c= ( dom ( ln (#) sin ));

      then

       A3: Z c= (( dom ln ) /\ ( dom sin )) by VALUED_1:def 4;

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

      then

       A4: sin is_differentiable_on Z by A1, FDIFF_1: 9;

      

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

      

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

      proof

        let x;

        assume x in Z;

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

        then x in { g where g be Real : 0 < g } by XXREAL_1: 230;

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

        hence thesis;

      end;

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

      then

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

      

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

      proof

        let x;

        assume x in Z;

        then x > 0 by A6;

        then x in { g where g be Real : 0 < g };

        then x in ( right_open_halfline 0 ) by XXREAL_1: 230;

        hence thesis by TAYLOR_1: 18;

      end;

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

      proof

        let x;

        assume

         A9: x in Z;

        

        then ((( ln (#) sin ) `| Z) . x) = ((( sin . x) * ( diff ( ln ,x))) + (( ln . x) * ( diff ( sin ,x)))) by A2, A7, A4, FDIFF_1: 21

        .= ((( sin . x) * (1 / x)) + (( ln . x) * ( diff ( sin ,x)))) by A8, A9

        .= ((( sin . x) / x) + (( ln . x) * ( cos . x))) by SIN_COS: 64;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:17

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

    proof

      

       A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      assume

       A2: Z c= ( dom ( ln (#) cos ));

      then

       A3: Z c= (( dom ln ) /\ ( dom cos )) by VALUED_1:def 4;

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

      then

       A4: cos is_differentiable_on Z by A1, FDIFF_1: 9;

      

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

      

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

      proof

        let x;

        assume x in Z;

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

        then x in { g where g be Real : 0 < g } by XXREAL_1: 230;

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

        hence thesis;

      end;

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

      then

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

      

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

      proof

        let x;

        assume x in Z;

        then x > 0 by A6;

        then x in { g where g be Real : 0 < g };

        then x in ( right_open_halfline 0 ) by XXREAL_1: 230;

        hence thesis by TAYLOR_1: 18;

      end;

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

      proof

        let x;

        assume

         A9: x in Z;

        

        then ((( ln (#) cos ) `| Z) . x) = ((( cos . x) * ( diff ( ln ,x))) + (( ln . x) * ( diff ( cos ,x)))) by A2, A7, A4, FDIFF_1: 21

        .= ((( cos . x) * (1 / x)) + (( ln . x) * ( diff ( cos ,x)))) by A8, A9

        .= ((( cos . x) / x) + (( ln . x) * ( - ( sin . x)))) by SIN_COS: 63;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:18

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

    proof

      

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

      assume

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

      then

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

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

      then

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

      

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

      

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

      proof

        let x;

        assume x in Z;

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

        then x in { g where g be Real : 0 < g } by XXREAL_1: 230;

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

        hence thesis;

      end;

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

      then

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

      

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

      proof

        let x;

        assume x in Z;

        then x > 0 by A6;

        then x in { g where g be Real : 0 < g };

        then x in ( right_open_halfline 0 ) by XXREAL_1: 230;

        hence thesis by TAYLOR_1: 18;

      end;

      for x st x in Z holds ((( ln (#) exp_R ) `| Z) . x) = ((( exp_R . x) / x) + (( ln . x) * ( exp_R . x)))

      proof

        let x;

        assume

         A9: x in Z;

        

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

        .= ((( exp_R . x) * (1 / x)) + (( ln . x) * ( diff ( exp_R ,x)))) by A8, A9

        .= ((( exp_R . x) * (1 / x)) + (( ln . x) * ( exp_R . x))) by SIN_COS: 65;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:19

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

    proof

      assume that

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

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

      

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

      proof

        let x;

        assume x in Z;

        then

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

         ]. 0 , +infty .[ = { g where g be Real : 0 < g } by XXREAL_1: 230;

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

        hence thesis;

      end;

      

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

      proof

        let x;

        assume

         A6: x in Z;

        then

         A7: ( ln . x) > 0 by A3;

         ln is_differentiable_in x by A2, A6, TAYLOR_1: 18;

        hence thesis by A7, TAYLOR_1: 20;

      end;

      then

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

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

      proof

        let x;

        

         A9: ]. 0 , +infty .[ = { g where g be Real : 0 < g } by XXREAL_1: 230;

        assume

         A10: x in Z;

        then

         A11: ( ln . x) > 0 by A3;

        x > 0 by A2, A10;

        then

         A12: x in ( right_open_halfline 0 ) by A9;

         ln is_differentiable_in x by A2, A10, TAYLOR_1: 18;

        

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

        .= ((1 / ( ln . x)) * (1 / x)) by A12, TAYLOR_1: 18

        .= (1 / (( ln . x) * x)) by XCMPLX_1: 102;

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

      end;

      hence thesis by A1, A5, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:20

    Z c= ( dom ( exp_R * exp_R )) implies ( exp_R * exp_R ) is_differentiable_on Z & for x st x in Z holds ((( exp_R * exp_R ) `| Z) . x) = (( exp_R . ( exp_R . x)) * ( exp_R . x))

    proof

      

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

      proof

        let x;

        assume x in Z;

        

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

         exp_R is_differentiable_in x by SIN_COS: 65;

        hence thesis by A2, FDIFF_2: 13;

      end;

      assume

       A3: Z c= ( dom ( exp_R * exp_R ));

      then

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

      for x st x in Z holds ((( exp_R * exp_R ) `| Z) . x) = (( exp_R . ( exp_R . x)) * ( exp_R . x))

      proof

        let x;

        assume

         A5: x in Z;

        

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

         exp_R is_differentiable_in x by SIN_COS: 65;

        

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

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

        .= (( exp_R . ( exp_R . x)) * ( exp_R . x)) by SIN_COS: 65;

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

      end;

      hence thesis by A3, A1, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:21

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

    proof

      assume

       A1: Z c= ( dom ( sin * 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 FDIFF_8: 1;

      end;

      

       A3: for x st x in Z holds ( sin * 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;

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

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        

         A6: sin is_differentiable_in ( tan . x) by SIN_COS: 64;

        assume

         A7: x in Z;

        then

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

        then tan is_differentiable_in x by FDIFF_7: 46;

        

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

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

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

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:22

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

    proof

      assume

       A1: Z c= ( dom ( sin * 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 FDIFF_8: 2;

      end;

      

       A3: for x st x in Z holds ( sin * 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;

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

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        

         A6: sin is_differentiable_in ( cot . x) by SIN_COS: 64;

        assume

         A7: x in Z;

        then

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

        then cot is_differentiable_in x by FDIFF_7: 47;

        

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

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

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

        .= ( - (( cos ( 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_10:23

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

    proof

      assume

       A1: Z c= ( dom ( cos * 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 FDIFF_8: 1;

      end;

      

       A3: for x st x in Z holds ( cos * 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;

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

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        

         A6: cos is_differentiable_in ( tan . x) by SIN_COS: 63;

        assume

         A7: x in Z;

        then

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

        then tan is_differentiable_in x by FDIFF_7: 46;

        

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

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

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

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:24

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

    proof

      assume

       A1: Z c= ( dom ( cos * 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 FDIFF_8: 2;

      end;

      

       A3: for x st x in Z holds ( cos * 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;

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

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

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

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

      proof

        let x;

        

         A6: cos is_differentiable_in ( cot . x) by SIN_COS: 63;

        assume

         A7: x in Z;

        then

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

        then cot is_differentiable_in x by FDIFF_7: 47;

        

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

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

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

        .= (( sin ( 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_10:25

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

    proof

      

       A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      assume

       A2: Z c= ( dom ( sin (#) ( tan + cot )));

      then

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

      then

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

      then

       A5: ( tan + cot ) is_differentiable_on Z by Th6;

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

      then

       A6: sin is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

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

        .= (((( tan . x) + ( cot . x)) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( tan + cot ),x)))) by A4, A7, VALUED_1:def 1

        .= (((( tan . x) + ( cot . x)) * ( cos . x)) + (( sin . x) * ( diff (( tan + cot ),x)))) by SIN_COS: 64

        .= (((( tan . x) + ( cot . x)) * ( cos . x)) + (( sin . x) * ((( tan + cot ) `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (((( tan . x) + ( cot . x)) * ( cos . x)) + (( sin . x) * ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))))) by A4, A7, Th6;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:26

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

    proof

      

       A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      assume

       A2: Z c= ( dom ( cos (#) ( tan + cot )));

      then

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

      then

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

      then

       A5: ( tan + cot ) is_differentiable_on Z by Th6;

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

      then

       A6: cos is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

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

        .= (((( tan . x) + ( cot . x)) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( tan + cot ),x)))) by A4, A7, VALUED_1:def 1

        .= (((( tan . x) + ( cot . x)) * ( - ( sin . x))) + (( cos . x) * ( diff (( tan + cot ),x)))) by SIN_COS: 63

        .= (((( tan . x) + ( cot . x)) * ( - ( sin . x))) + (( cos . x) * ((( tan + cot ) `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (((( tan . x) + ( cot . x)) * ( - ( sin . x))) + (( cos . x) * ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))))) by A4, A7, Th6;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:27

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

    proof

      

       A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      assume

       A2: Z c= ( dom ( sin (#) ( tan - cot )));

      then

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

      then

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

      then

       A5: ( tan - cot ) is_differentiable_on Z by Th5;

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

      then

       A6: sin is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((( sin (#) ( tan - cot )) `| Z) . x) = (((( tan - cot ) . x) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( tan - cot ),x)))) by A2, A5, A6, FDIFF_1: 21

        .= (((( tan . x) - ( cot . x)) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( tan - cot ),x)))) by A4, A7, VALUED_1: 13

        .= (((( tan . x) - ( cot . x)) * ( cos . x)) + (( sin . x) * ( diff (( tan - cot ),x)))) by SIN_COS: 64

        .= (((( tan . x) - ( cot . x)) * ( cos . x)) + (( sin . x) * ((( tan - cot ) `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (((( tan . x) - ( cot . x)) * ( cos . x)) + (( sin . x) * ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 ))))) by A4, A7, Th5;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:28

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

    proof

      

       A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      assume

       A2: Z c= ( dom ( cos (#) ( tan - cot )));

      then

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

      then

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

      then

       A5: ( tan - cot ) is_differentiable_on Z by Th5;

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

      then

       A6: cos is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((( cos (#) ( tan - cot )) `| Z) . x) = (((( tan - cot ) . x) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( tan - cot ),x)))) by A2, A5, A6, FDIFF_1: 21

        .= (((( tan . x) - ( cot . x)) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( tan - cot ),x)))) by A4, A7, VALUED_1: 13

        .= (((( tan . x) - ( cot . x)) * ( - ( sin . x))) + (( cos . x) * ( diff (( tan - cot ),x)))) by SIN_COS: 63

        .= (((( tan . x) - ( cot . x)) * ( - ( sin . x))) + (( cos . x) * ((( tan - cot ) `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (((( tan . x) - ( cot . x)) * ( - ( sin . x))) + (( cos . x) * ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 ))))) by A4, A7, Th5;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:29

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

    proof

      assume

       A1: Z c= ( dom ( exp_R (#) ( tan + cot )));

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

      then

       A2: Z c= ( dom ( tan + cot )) by XBOOLE_1: 18;

      then

       A3: ( tan + cot ) is_differentiable_on Z by Th6;

      

       A4: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

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

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((( exp_R (#) ( tan + cot )) `| Z) . x) = (((( tan + cot ) . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( tan + cot ),x)))) by A1, A3, A4, FDIFF_1: 21

        .= (((( tan . x) + ( cot . x)) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( tan + cot ),x)))) by A2, A5, VALUED_1:def 1

        .= ((( exp_R . x) * (( tan . x) + ( cot . x))) + (( exp_R . x) * ( diff (( tan + cot ),x)))) by TAYLOR_1: 16

        .= ((( exp_R . x) * (( tan . x) + ( cot . x))) + (( exp_R . x) * ((( tan + cot ) `| Z) . x))) by A3, A5, FDIFF_1:def 7

        .= ((( exp_R . x) * (( tan . x) + ( cot . x))) + (( exp_R . x) * ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))))) by A2, A5, Th6;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:30

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

    proof

      assume

       A1: Z c= ( dom ( exp_R (#) ( tan - cot )));

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

      then

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

      then

       A3: ( tan - cot ) is_differentiable_on Z by Th5;

      

       A4: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

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

      proof

        let x;

        assume

         A5: x in Z;

        

        then ((( exp_R (#) ( tan - cot )) `| Z) . x) = (((( tan - cot ) . x) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( tan - cot ),x)))) by A1, A3, A4, FDIFF_1: 21

        .= (((( tan . x) - ( cot . x)) * ( diff ( exp_R ,x))) + (( exp_R . x) * ( diff (( tan - cot ),x)))) by A2, A5, VALUED_1: 13

        .= ((( exp_R . x) * (( tan . x) - ( cot . x))) + (( exp_R . x) * ( diff (( tan - cot ),x)))) by TAYLOR_1: 16

        .= ((( exp_R . x) * (( tan . x) - ( cot . x))) + (( exp_R . x) * ((( tan - cot ) `| Z) . x))) by A3, A5, FDIFF_1:def 7

        .= ((( exp_R . x) * (( tan . x) - ( cot . x))) + (( exp_R . x) * ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 ))))) by A2, A5, Th5;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:31

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

    proof

      

       A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      assume

       A2: Z c= ( dom ( sin (#) ( sin + cos )));

      then

       A3: Z c= (( dom ( sin + cos )) /\ ( dom sin )) by VALUED_1:def 4;

      then

       A4: Z c= ( dom ( sin + cos )) by XBOOLE_1: 18;

      then

       A5: ( sin + cos ) is_differentiable_on Z by FDIFF_7: 38;

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

      then

       A6: sin is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        reconsider xx = x as Element of REAL by XREAL_0:def 1;

        assume

         A7: x in Z;

        

        then ((( sin (#) ( sin + cos )) `| Z) . x) = (((( sin + cos ) . x) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( sin + cos ),x)))) by A2, A5, A6, FDIFF_1: 21

        .= (((( sin . xx) + ( cos . xx)) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( sin + cos ),x)))) by VALUED_1: 1

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

        .= (((( sin . x) + ( cos . x)) * ( cos . x)) + (( sin . x) * ((( sin + cos ) `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (((( sin . x) + ( cos . x)) * ( cos . x)) + (( sin . x) * (( cos . x) - ( sin . x)))) by A4, A7, FDIFF_7: 38;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:32

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

    proof

      

       A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS: 64;

      assume

       A2: Z c= ( dom ( sin (#) ( sin - cos )));

      then

       A3: Z c= (( dom ( sin - cos )) /\ ( dom sin )) by VALUED_1:def 4;

      then

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

      then

       A5: ( sin - cos ) is_differentiable_on Z by FDIFF_7: 39;

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

      then

       A6: sin is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((( sin (#) ( sin - cos )) `| Z) . x) = (((( sin - cos ) . x) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( sin - cos ),x)))) by A2, A5, A6, FDIFF_1: 21

        .= (((( sin . x) - ( cos . x)) * ( diff ( sin ,x))) + (( sin . x) * ( diff (( sin - cos ),x)))) by A4, A7, VALUED_1: 13

        .= (((( sin . x) - ( cos . x)) * ( cos . x)) + (( sin . x) * ( diff (( sin - cos ),x)))) by SIN_COS: 64

        .= (((( sin . x) - ( cos . x)) * ( cos . x)) + (( sin . x) * ((( sin - cos ) `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (((( sin . x) - ( cos . x)) * ( cos . x)) + (( sin . x) * (( cos . x) + ( sin . x)))) by A4, A7, FDIFF_7: 39;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:33

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

    proof

      

       A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      assume

       A2: Z c= ( dom ( cos (#) ( sin - cos )));

      then

       A3: Z c= (( dom ( sin - cos )) /\ ( dom cos )) by VALUED_1:def 4;

      then

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

      then

       A5: ( sin - cos ) is_differentiable_on Z by FDIFF_7: 39;

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

      then

       A6: cos is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        assume

         A7: x in Z;

        

        then ((( cos (#) ( sin - cos )) `| Z) . x) = (((( sin - cos ) . x) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( sin - cos ),x)))) by A2, A5, A6, FDIFF_1: 21

        .= (((( sin . x) - ( cos . x)) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( sin - cos ),x)))) by A4, A7, VALUED_1: 13

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

        .= (((( sin . x) - ( cos . x)) * ( - ( sin . x))) + (( cos . x) * ((( sin - cos ) `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (((( sin . x) - ( cos . x)) * ( - ( sin . x))) + (( cos . x) * (( cos . x) + ( sin . x)))) by A4, A7, FDIFF_7: 39;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:34

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

    proof

      

       A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS: 63;

      assume

       A2: Z c= ( dom ( cos (#) ( sin + cos )));

      then

       A3: Z c= (( dom ( sin + cos )) /\ ( dom cos )) by VALUED_1:def 4;

      then

       A4: Z c= ( dom ( sin + cos )) by XBOOLE_1: 18;

      then

       A5: ( sin + cos ) is_differentiable_on Z by FDIFF_7: 38;

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

      then

       A6: cos is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        reconsider xx = x as Element of REAL by XREAL_0:def 1;

        assume

         A7: x in Z;

        

        then ((( cos (#) ( sin + cos )) `| Z) . x) = (((( sin + cos ) . x) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( sin + cos ),x)))) by A2, A5, A6, FDIFF_1: 21

        .= (((( sin . xx) + ( cos . xx)) * ( diff ( cos ,x))) + (( cos . x) * ( diff (( sin + cos ),x)))) by VALUED_1: 1

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

        .= (((( sin . x) + ( cos . x)) * ( - ( sin . x))) + (( cos . x) * ((( sin + cos ) `| Z) . x))) by A5, A7, FDIFF_1:def 7

        .= (((( sin . x) + ( cos . x)) * ( - ( sin . x))) + (( cos . x) * (( cos . x) - ( sin . x)))) by A4, A7, FDIFF_7: 38;

        hence thesis;

      end;

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

    end;

    theorem :: FDIFF_10:35

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

    proof

      assume that

       A1: Z c= ( dom ( sin * ( tan + cot )));

      ( dom ( sin * ( tan + cot ))) c= ( dom ( tan + cot )) by RELAT_1: 25;

      then

       A2: Z c= ( dom ( tan + cot )) by A1, XBOOLE_1: 1;

      then

       A3: ( tan + cot ) is_differentiable_on Z by Th6;

      

       A4: for x st x in Z holds ( sin * ( tan + cot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ( tan + cot ) is_differentiable_in x by A3, FDIFF_1: 9;

         sin is_differentiable_in (( tan + cot ) . x) by SIN_COS: 64;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( sin * ( tan + cot )) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A7: sin is_differentiable_in (( tan + cot ) . x) by SIN_COS: 64;

        assume

         A8: x in Z;

        then ( tan + cot ) is_differentiable_in x by A3, FDIFF_1: 9;

        

        then ( diff (( sin * ( tan + cot )),x)) = (( diff ( sin ,(( tan + cot ) . x))) * ( diff (( tan + cot ),x))) by A7, FDIFF_2: 13

        .= (( cos . (( tan + cot ) . x)) * ( diff (( tan + cot ),x))) by SIN_COS: 64

        .= (( cos . (( tan + cot ) . x)) * ((( tan + cot ) `| Z) . x)) by A3, A8, FDIFF_1:def 7

        .= (( cos . (( tan + cot ) . x)) * ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 )))) by A2, A8, Th6

        .= (( cos . (( tan . x) + ( cot . x))) * ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 )))) by A2, A8, VALUED_1:def 1;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:36

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

    proof

      assume that

       A1: Z c= ( dom ( sin * ( tan - cot )));

      ( dom ( sin * ( tan - cot ))) c= ( dom ( tan - cot )) by RELAT_1: 25;

      then

       A2: Z c= ( dom ( tan - cot )) by A1, XBOOLE_1: 1;

      then

       A3: ( tan - cot ) is_differentiable_on Z by Th5;

      

       A4: for x st x in Z holds ( sin * ( tan - cot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ( tan - cot ) is_differentiable_in x by A3, FDIFF_1: 9;

         sin is_differentiable_in (( tan - cot ) . x) by SIN_COS: 64;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( sin * ( tan - cot )) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A7: sin is_differentiable_in (( tan - cot ) . x) by SIN_COS: 64;

        assume

         A8: x in Z;

        then ( tan - cot ) is_differentiable_in x by A3, FDIFF_1: 9;

        

        then ( diff (( sin * ( tan - cot )),x)) = (( diff ( sin ,(( tan - cot ) . x))) * ( diff (( tan - cot ),x))) by A7, FDIFF_2: 13

        .= (( cos . (( tan - cot ) . x)) * ( diff (( tan - cot ),x))) by SIN_COS: 64

        .= (( cos . (( tan - cot ) . x)) * ((( tan - cot ) `| Z) . x)) by A3, A8, FDIFF_1:def 7

        .= (( cos . (( tan - cot ) . x)) * ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 )))) by A2, A8, Th5

        .= (( cos . (( tan . x) - ( cot . x))) * ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 )))) by A2, A8, VALUED_1: 13;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:37

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

    proof

      assume that

       A1: Z c= ( dom ( cos * ( tan - cot )));

      ( dom ( cos * ( tan - cot ))) c= ( dom ( tan - cot )) by RELAT_1: 25;

      then

       A2: Z c= ( dom ( tan - cot )) by A1, XBOOLE_1: 1;

      then

       A3: ( tan - cot ) is_differentiable_on Z by Th5;

      

       A4: for x st x in Z holds ( cos * ( tan - cot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ( tan - cot ) is_differentiable_in x by A3, FDIFF_1: 9;

         cos is_differentiable_in (( tan - cot ) . x) by SIN_COS: 63;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( cos * ( tan - cot )) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A7: cos is_differentiable_in (( tan - cot ) . x) by SIN_COS: 63;

        assume

         A8: x in Z;

        then ( tan - cot ) is_differentiable_in x by A3, FDIFF_1: 9;

        

        then ( diff (( cos * ( tan - cot )),x)) = (( diff ( cos ,(( tan - cot ) . x))) * ( diff (( tan - cot ),x))) by A7, FDIFF_2: 13

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

        .= (( - ( sin . (( tan - cot ) . x))) * ((( tan - cot ) `| Z) . x)) by A3, A8, FDIFF_1:def 7

        .= (( - ( sin . (( tan - cot ) . x))) * ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 )))) by A2, A8, Th5

        .= (( - ( sin . (( tan . x) - ( cot . x)))) * ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 )))) by A2, A8, VALUED_1: 13;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:38

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

    proof

      assume that

       A1: Z c= ( dom ( cos * ( tan + cot )));

      ( dom ( cos * ( tan + cot ))) c= ( dom ( tan + cot )) by RELAT_1: 25;

      then

       A2: Z c= ( dom ( tan + cot )) by A1, XBOOLE_1: 1;

      then

       A3: ( tan + cot ) is_differentiable_on Z by Th6;

      

       A4: for x st x in Z holds ( cos * ( tan + cot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ( tan + cot ) is_differentiable_in x by A3, FDIFF_1: 9;

         cos is_differentiable_in (( tan + cot ) . x) by SIN_COS: 63;

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( cos * ( tan + cot )) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A7: cos is_differentiable_in (( tan + cot ) . x) by SIN_COS: 63;

        assume

         A8: x in Z;

        then ( tan + cot ) is_differentiable_in x by A3, FDIFF_1: 9;

        

        then ( diff (( cos * ( tan + cot )),x)) = (( diff ( cos ,(( tan + cot ) . x))) * ( diff (( tan + cot ),x))) by A7, FDIFF_2: 13

        .= (( - ( sin . (( tan + cot ) . x))) * ( diff (( tan + cot ),x))) by SIN_COS: 63

        .= (( - ( sin . (( tan + cot ) . x))) * ((( tan + cot ) `| Z) . x)) by A3, A8, FDIFF_1:def 7

        .= (( - ( sin . (( tan + cot ) . x))) * ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 )))) by A2, A8, Th6

        .= (( - ( sin . (( tan . x) + ( cot . x)))) * ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 )))) by A2, A8, VALUED_1:def 1;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:39

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

    proof

      assume that

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

      ( dom ( exp_R * ( tan + cot ))) c= ( dom ( tan + cot )) by RELAT_1: 25;

      then

       A2: Z c= ( dom ( tan + cot )) by A1, XBOOLE_1: 1;

      then

       A3: ( tan + cot ) is_differentiable_on Z by Th6;

      

       A4: for x st x in Z holds ( exp_R * ( tan + cot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ( tan + cot ) is_differentiable_in x by A3, FDIFF_1: 9;

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

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( exp_R * ( tan + cot )) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

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

        assume

         A8: x in Z;

        then ( tan + cot ) is_differentiable_in x by A3, FDIFF_1: 9;

        

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

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

        .= (( exp_R . (( tan + cot ) . x)) * ((( tan + cot ) `| Z) . x)) by A3, A8, FDIFF_1:def 7

        .= (( exp_R . (( tan + cot ) . x)) * ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 )))) by A2, A8, Th6

        .= (( exp_R . (( tan . x) + ( cot . x))) * ((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 )))) by A2, A8, VALUED_1:def 1;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:40

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

    proof

      assume that

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

      ( dom ( exp_R * ( tan - cot ))) c= ( dom ( tan - cot )) by RELAT_1: 25;

      then

       A2: Z c= ( dom ( tan - cot )) by A1, XBOOLE_1: 1;

      then

       A3: ( tan - cot ) is_differentiable_on Z by Th5;

      

       A4: for x st x in Z holds ( exp_R * ( tan - cot )) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then

         A5: ( tan - cot ) is_differentiable_in x by A3, FDIFF_1: 9;

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

        hence thesis by A5, FDIFF_2: 13;

      end;

      then

       A6: ( exp_R * ( tan - cot )) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

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

        assume

         A8: x in Z;

        then ( tan - cot ) is_differentiable_in x by A3, FDIFF_1: 9;

        

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

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

        .= (( exp_R . (( tan - cot ) . x)) * ((( tan - cot ) `| Z) . x)) by A3, A8, FDIFF_1:def 7

        .= (( exp_R . (( tan - cot ) . x)) * ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 )))) by A2, A8, Th5

        .= (( exp_R . (( tan . x) - ( cot . x))) * ((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 )))) by A2, A8, VALUED_1: 13;

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

      end;

      hence thesis by A1, A4, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:41

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

    proof

      

       A1: for x st x in Z holds ( exp_R . x) <> 0 by SIN_COS: 54;

      assume Z c= ( dom (( tan - cot ) / exp_R ));

      then Z c= (( dom ( tan - cot )) /\ (( dom exp_R ) \ ( exp_R " { 0 }))) by RFUNCT_1:def 1;

      then

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

      then

       A3: ( tan - cot ) is_differentiable_on Z by Th5;

      

       A4: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      then

       A5: (( tan - cot ) / exp_R ) is_differentiable_on Z by A3, A1, FDIFF_2: 21;

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

      proof

        let x;

        

         A6: exp_R is_differentiable_in x by SIN_COS: 65;

        

         A7: ( exp_R . x) <> 0 by SIN_COS: 54;

        assume

         A8: x in Z;

        then

         A9: (( tan - cot ) . x) = (( tan . x) - ( cot . x)) by A2, VALUED_1: 13;

        ( tan - cot ) is_differentiable_in x by A3, A8, FDIFF_1: 9;

        

        then ( diff ((( tan - cot ) / exp_R ),x)) = (((( diff (( tan - cot ),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( tan - cot ) . x))) / (( exp_R . x) ^2 )) by A6, A7, FDIFF_2: 14

        .= (((((( tan - cot ) `| Z) . x) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( tan - cot ) . x))) / (( exp_R . x) ^2 )) by A3, A8, FDIFF_1:def 7

        .= (((((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 ))) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( tan - cot ) . x))) / (( exp_R . x) ^2 )) by A2, A8, Th5

        .= (((((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 ))) * ( exp_R . x)) - (( exp_R . x) * (( tan . x) - ( cot . x)))) / (( exp_R . x) * ( exp_R . x))) by A9, SIN_COS: 65

        .= ((((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 ))) - (( tan . x) - ( cot . x))) * (( exp_R . x) / (( exp_R . x) * ( exp_R . x))))

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

        .= ((((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 ))) - (( tan . x) - ( cot . x))) * (1 / ( exp_R . x))) by A7, XCMPLX_1: 60

        .= ((((1 / (( cos . x) ^2 )) + (1 / (( sin . x) ^2 ))) - (( tan . x) - ( cot . x))) / ( exp_R . x));

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

      end;

      hence thesis by A3, A4, A1, FDIFF_2: 21;

    end;

    theorem :: FDIFF_10:42

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

    proof

      

       A1: for x st x in Z holds ( exp_R . x) <> 0 by SIN_COS: 54;

      assume Z c= ( dom (( tan + cot ) / exp_R ));

      then Z c= (( dom ( tan + cot )) /\ (( dom exp_R ) \ ( exp_R " { 0 }))) by RFUNCT_1:def 1;

      then

       A2: Z c= ( dom ( tan + cot )) by XBOOLE_1: 18;

      then

       A3: ( tan + cot ) is_differentiable_on Z by Th6;

      

       A4: exp_R is_differentiable_on Z by FDIFF_1: 26, TAYLOR_1: 16;

      then

       A5: (( tan + cot ) / exp_R ) is_differentiable_on Z by A3, A1, FDIFF_2: 21;

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

      proof

        let x;

        

         A6: exp_R is_differentiable_in x by SIN_COS: 65;

        

         A7: ( exp_R . x) <> 0 by SIN_COS: 54;

        assume

         A8: x in Z;

        then

         A9: (( tan + cot ) . x) = (( tan . x) + ( cot . x)) by A2, VALUED_1:def 1;

        ( tan + cot ) is_differentiable_in x by A3, A8, FDIFF_1: 9;

        

        then ( diff ((( tan + cot ) / exp_R ),x)) = (((( diff (( tan + cot ),x)) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( tan + cot ) . x))) / (( exp_R . x) ^2 )) by A6, A7, FDIFF_2: 14

        .= (((((( tan + cot ) `| Z) . x) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( tan + cot ) . x))) / (( exp_R . x) ^2 )) by A3, A8, FDIFF_1:def 7

        .= (((((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))) * ( exp_R . x)) - (( diff ( exp_R ,x)) * (( tan + cot ) . x))) / (( exp_R . x) ^2 )) by A2, A8, Th6

        .= (((((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))) * ( exp_R . x)) - (( exp_R . x) * (( tan . x) + ( cot . x)))) / (( exp_R . x) * ( exp_R . x))) by A9, SIN_COS: 65

        .= ((((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))) - (( tan . x) + ( cot . x))) * (( exp_R . x) / (( exp_R . x) * ( exp_R . x))))

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

        .= ((((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))) - (( tan . x) + ( cot . x))) * (1 / ( exp_R . x))) by A7, XCMPLX_1: 60

        .= ((((1 / (( cos . x) ^2 )) - (1 / (( sin . x) ^2 ))) - (( tan . x) + ( cot . x))) / ( exp_R . x));

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

      end;

      hence thesis by A3, A4, A1, FDIFF_2: 21;

    end;

    theorem :: FDIFF_10:43

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

    proof

      assume

       A1: Z c= ( dom ( sin * sec ));

      ( dom ( sin * sec )) c= ( dom sec ) by RELAT_1: 25;

      then

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

      

       A3: for x st x in Z holds ( sin * sec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A2, RFUNCT_1: 3;

        then

         A4: sec is_differentiable_in x by FDIFF_9: 1;

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

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( sin * sec ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A6: sin is_differentiable_in ( sec . x) by SIN_COS: 64;

        assume

         A7: x in Z;

        then

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

        then sec is_differentiable_in x by FDIFF_9: 1;

        

        then ( diff (( sin * sec ),x)) = (( diff ( sin ,( sec . x))) * ( diff ( sec ,x))) by A6, FDIFF_2: 13

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

        .= (( cos ( sec . x)) * (( sin . x) / (( cos . x) ^2 ))) by A8, FDIFF_9: 1

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:44

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

    proof

      assume

       A1: Z c= ( dom ( cos * sec ));

      ( dom ( cos * sec )) c= ( dom sec ) by RELAT_1: 25;

      then

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

      

       A3: for x st x in Z holds ( cos * sec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( cos . x) <> 0 by A2, RFUNCT_1: 3;

        then

         A4: sec is_differentiable_in x by FDIFF_9: 1;

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

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( cos * sec ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A6: cos is_differentiable_in ( sec . x) by SIN_COS: 63;

        assume

         A7: x in Z;

        then

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

        then sec is_differentiable_in x by FDIFF_9: 1;

        

        then ( diff (( cos * sec ),x)) = (( diff ( cos ,( sec . x))) * ( diff ( sec ,x))) by A6, FDIFF_2: 13

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

        .= (( - ( sin ( sec . x))) * (( sin . x) / (( cos . x) ^2 ))) by A8, FDIFF_9: 1

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

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;

    theorem :: FDIFF_10:45

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

    proof

      assume

       A1: Z c= ( dom ( sin * cosec ));

      ( dom ( sin * cosec )) c= ( dom cosec ) by RELAT_1: 25;

      then

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

      

       A3: for x st x in Z holds ( sin * cosec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A2, RFUNCT_1: 3;

        then

         A4: cosec is_differentiable_in x by FDIFF_9: 2;

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

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( sin * cosec ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A6: sin is_differentiable_in ( cosec . x) by SIN_COS: 64;

        assume

         A7: x in Z;

        then

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

        then cosec is_differentiable_in x by FDIFF_9: 2;

        

        then ( diff (( sin * cosec ),x)) = (( diff ( sin ,( cosec . x))) * ( diff ( cosec ,x))) by A6, FDIFF_2: 13

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

        .= (( cos ( cosec . x)) * ( - (( cos . x) / (( sin . x) ^2 )))) by A8, FDIFF_9: 2

        .= ( - ((( cos . ( cosec . x)) * ( cos . 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_10:46

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

    proof

      assume

       A1: Z c= ( dom ( cos * cosec ));

      ( dom ( cos * cosec )) c= ( dom cosec ) by RELAT_1: 25;

      then

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

      

       A3: for x st x in Z holds ( cos * cosec ) is_differentiable_in x

      proof

        let x;

        assume x in Z;

        then ( sin . x) <> 0 by A2, RFUNCT_1: 3;

        then

         A4: cosec is_differentiable_in x by FDIFF_9: 2;

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

        hence thesis by A4, FDIFF_2: 13;

      end;

      then

       A5: ( cos * cosec ) is_differentiable_on Z by A1, FDIFF_1: 9;

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

      proof

        let x;

        

         A6: cos is_differentiable_in ( cosec . x) by SIN_COS: 63;

        assume

         A7: x in Z;

        then

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

        then cosec is_differentiable_in x by FDIFF_9: 2;

        

        then ( diff (( cos * cosec ),x)) = (( diff ( cos ,( cosec . x))) * ( diff ( cosec ,x))) by A6, FDIFF_2: 13

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

        .= (( - ( sin ( cosec . x))) * ( - (( cos . x) / (( sin . x) ^2 )))) by A8, FDIFF_9: 2;

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

      end;

      hence thesis by A1, A3, FDIFF_1: 9;

    end;