:: Several Differentiation Formulas of Special Functions -- Part {VII} :: by Fuguo Ge and Bing Xie :: :: Received September 23, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin ::f.x=arctan.(sin.x) theorem :: FDIFF_11:1 for Z being open Subset of REAL st Z c= dom (arctan * sin) & ( for x being Real st x in Z holds ( sin . x > - 1 & sin . x < 1 ) ) holds ( arctan * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * sin) `| Z) . x = (cos . x) / (1 + ((sin . x) ^2)) ) ) proofend; ::f.x=arccot.(sin.x) theorem :: FDIFF_11:2 for Z being open Subset of REAL st Z c= dom (arccot * sin) & ( for x being Real st x in Z holds ( sin . x > - 1 & sin . x < 1 ) ) holds ( arccot * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * sin) `| Z) . x = - ((cos . x) / (1 + ((sin . x) ^2))) ) ) proofend; ::f.x=arctan.(cos.x) theorem :: FDIFF_11:3 for Z being open Subset of REAL st Z c= dom (arctan * cos) & ( for x being Real st x in Z holds ( cos . x > - 1 & cos . x < 1 ) ) holds ( arctan * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * cos) `| Z) . x = - ((sin . x) / (1 + ((cos . x) ^2))) ) ) proofend; ::f.x=arccot.(cos.x) theorem :: FDIFF_11:4 for Z being open Subset of REAL st Z c= dom (arccot * cos) & ( for x being Real st x in Z holds ( cos . x > - 1 & cos . x < 1 ) ) holds ( arccot * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * cos) `| Z) . x = (sin . x) / (1 + ((cos . x) ^2)) ) ) proofend; ::f.x=arctan.(tan.x) theorem :: FDIFF_11:5 for Z being open Subset of REAL st Z c= dom (arctan * tan) & ( for x being Real st x in Z holds ( tan . x > - 1 & tan . x < 1 ) ) holds ( arctan * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * tan) `| Z) . x = 1 ) ) proofend; ::f.x=arccot.(tan.x) theorem :: FDIFF_11:6 for Z being open Subset of REAL st Z c= dom (arccot * tan) & ( for x being Real st x in Z holds ( tan . x > - 1 & tan . x < 1 ) ) holds ( arccot * tan is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * tan) `| Z) . x = - 1 ) ) proofend; ::f.x=arctan.(cot.x) theorem :: FDIFF_11:7 for Z being open Subset of REAL st Z c= dom (arctan * cot) & ( for x being Real st x in Z holds ( cot . x > - 1 & cot . x < 1 ) ) holds ( arctan * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * cot) `| Z) . x = - 1 ) ) proofend; ::f.x=arccot.(cot.x) theorem :: FDIFF_11:8 for Z being open Subset of REAL st Z c= dom (arccot * cot) & ( for x being Real st x in Z holds ( cot . x > - 1 & cot . x < 1 ) ) holds ( arccot * cot is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * cot) `| Z) . x = 1 ) ) proofend; ::f.x=arctan.(arctan.x) theorem :: FDIFF_11:9 for Z being open Subset of REAL st Z c= dom (arctan * arctan) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds ( arctan . x > - 1 & arctan . x < 1 ) ) holds ( arctan * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * arctan) `| Z) . x = 1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2))) ) ) proofend; ::f.x=arccot.(arctan.x) theorem :: FDIFF_11:10 for Z being open Subset of REAL st Z c= dom (arccot * arctan) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds ( arctan . x > - 1 & arctan . x < 1 ) ) holds ( arccot * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * arctan) `| Z) . x = - (1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2)))) ) ) proofend; ::f.x=arctan.(arccot.x) theorem :: FDIFF_11:11 for Z being open Subset of REAL st Z c= dom (arctan * arccot) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds ( arccot . x > - 1 & arccot . x < 1 ) ) holds ( arctan * arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * arccot) `| Z) . x = - (1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2)))) ) ) proofend; ::f.x=arccot.(arccot.x) theorem :: FDIFF_11:12 for Z being open Subset of REAL st Z c= dom (arccot * arccot) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds ( arccot . x > - 1 & arccot . x < 1 ) ) holds ( arccot * arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * arccot) `| Z) . x = 1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2))) ) ) proofend; ::f.x=sin.(arctan.x) theorem :: FDIFF_11:13 for Z being open Subset of REAL st Z c= dom (sin * arctan) & Z c= ].(- 1),1.[ holds ( sin * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * arctan) `| Z) . x = (cos . (arctan . x)) / (1 + (x ^2)) ) ) proofend; ::f.x=sin.(arccot.x) theorem :: FDIFF_11:14 for Z being open Subset of REAL st Z c= dom (sin * arccot) & Z c= ].(- 1),1.[ holds ( sin * arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * arccot) `| Z) . x = - ((cos . (arccot . x)) / (1 + (x ^2))) ) ) proofend; ::f.x=cos.(arctan.x) theorem :: FDIFF_11:15 for Z being open Subset of REAL st Z c= dom (cos * arctan) & Z c= ].(- 1),1.[ holds ( cos * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * arctan) `| Z) . x = - ((sin . (arctan . x)) / (1 + (x ^2))) ) ) proofend; ::f.x=cos.(arccot.x) theorem :: FDIFF_11:16 for Z being open Subset of REAL st Z c= dom (cos * arccot) & Z c= ].(- 1),1.[ holds ( cos * arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * arccot) `| Z) . x = (sin . (arccot . x)) / (1 + (x ^2)) ) ) proofend; ::f.x=tan.(arctan.x) theorem :: FDIFF_11:17 for Z being open Subset of REAL st Z c= dom (tan * arctan) & Z c= ].(- 1),1.[ holds ( tan * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * arctan) `| Z) . x = 1 / (((cos . (arctan . x)) ^2) * (1 + (x ^2))) ) ) proofend; ::f.x=tan.(arccot.x) theorem :: FDIFF_11:18 for Z being open Subset of REAL st Z c= dom (tan * arccot) & Z c= ].(- 1),1.[ holds ( tan * arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan * arccot) `| Z) . x = - (1 / (((cos . (arccot . x)) ^2) * (1 + (x ^2)))) ) ) proofend; ::f.x=cot.(arctan.x) theorem :: FDIFF_11:19 for Z being open Subset of REAL st Z c= dom (cot * arctan) & Z c= ].(- 1),1.[ holds ( cot * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * arctan) `| Z) . x = - (1 / (((sin . (arctan . x)) ^2) * (1 + (x ^2)))) ) ) proofend; ::f.x=cot.(arccot.x) theorem :: FDIFF_11:20 for Z being open Subset of REAL st Z c= dom (cot * arccot) & Z c= ].(- 1),1.[ holds ( cot * arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((cot * arccot) `| Z) . x = 1 / (((sin . (arccot . x)) ^2) * (1 + (x ^2))) ) ) proofend; ::f.x=sec.(arctan.x) theorem :: FDIFF_11:21 for Z being open Subset of REAL st Z c= dom (sec * arctan) & Z c= ].(- 1),1.[ holds ( sec * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((sec * arctan) `| Z) . x = (sin . (arctan . x)) / (((cos . (arctan . x)) ^2) * (1 + (x ^2))) ) ) proofend; ::f.x=sec.(arccot.x) theorem :: FDIFF_11:22 for Z being open Subset of REAL st Z c= dom (sec * arccot) & Z c= ].(- 1),1.[ holds ( sec * arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((sec * arccot) `| Z) . x = - ((sin . (arccot . x)) / (((cos . (arccot . x)) ^2) * (1 + (x ^2)))) ) ) proofend; ::f.x=cosec.(arctan.x) theorem :: FDIFF_11:23 for Z being open Subset of REAL st Z c= dom (cosec * arctan) & Z c= ].(- 1),1.[ holds ( cosec * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((cosec * arctan) `| Z) . x = - ((cos . (arctan . x)) / (((sin . (arctan . x)) ^2) * (1 + (x ^2)))) ) ) proofend; ::f.x=cosec.(arccot.x) theorem :: FDIFF_11:24 for Z being open Subset of REAL st Z c= dom (cosec * arccot) & Z c= ].(- 1),1.[ holds ( cosec * arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((cosec * arccot) `| Z) . x = (cos . (arccot . x)) / (((sin . (arccot . x)) ^2) * (1 + (x ^2))) ) ) proofend; ::f.x=sin.x*arctan.x theorem :: FDIFF_11:25 for Z being open Subset of REAL st Z c= dom (sin (#) arctan) & Z c= ].(- 1),1.[ holds ( sin (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) arctan) `| Z) . x = ((cos . x) * (arctan . x)) + ((sin . x) / (1 + (x ^2))) ) ) proofend; ::f.x=sin.x*arccot.x theorem :: FDIFF_11:26 for Z being open Subset of REAL st Z c= dom (sin (#) arccot) & Z c= ].(- 1),1.[ holds ( sin (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) arccot) `| Z) . x = ((cos . x) * (arccot . x)) - ((sin . x) / (1 + (x ^2))) ) ) proofend; ::f.x=cos.x*arctan.x theorem :: FDIFF_11:27 for Z being open Subset of REAL st Z c= dom (cos (#) arctan) & Z c= ].(- 1),1.[ holds ( cos (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) arctan) `| Z) . x = (- ((sin . x) * (arctan . x))) + ((cos . x) / (1 + (x ^2))) ) ) proofend; ::f.x=cos.x*arccot.x theorem :: FDIFF_11:28 for Z being open Subset of REAL st Z c= dom (cos (#) arccot) & Z c= ].(- 1),1.[ holds ( cos (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) arccot) `| Z) . x = (- ((sin . x) * (arccot . x))) - ((cos . x) / (1 + (x ^2))) ) ) proofend; ::f.x=tan.x*arctan.x theorem :: FDIFF_11:29 for Z being open Subset of REAL st Z c= dom (tan (#) arctan) & Z c= ].(- 1),1.[ holds ( tan (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((tan (#) arctan) `| Z) . x = ((arctan . x) / ((cos . x) ^2)) + ((tan . x) / (1 + (x ^2))) ) ) proofend; ::f.x=tan.x*arccot.x theorem :: FDIFF_11:30 for Z being open Subset of REAL st Z c= dom (tan (#) arccot) & Z c= ].(- 1),1.[ holds ( tan (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((tan (#) arccot) `| Z) . x = ((arccot . x) / ((cos . x) ^2)) - ((tan . x) / (1 + (x ^2))) ) ) proofend; ::f.x=cot.x*arctan.x theorem :: FDIFF_11:31 for Z being open Subset of REAL st Z c= dom (cot (#) arctan) & Z c= ].(- 1),1.[ holds ( cot (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((cot (#) arctan) `| Z) . x = (- ((arctan . x) / ((sin . x) ^2))) + ((cot . x) / (1 + (x ^2))) ) ) proofend; ::f.x=cot.x*arccot.x theorem :: FDIFF_11:32 for Z being open Subset of REAL st Z c= dom (cot (#) arccot) & Z c= ].(- 1),1.[ holds ( cot (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((cot (#) arccot) `| Z) . x = (- ((arccot . x) / ((sin . x) ^2))) - ((cot . x) / (1 + (x ^2))) ) ) proofend; ::f.x=sec.x*arctan.x theorem :: FDIFF_11:33 for Z being open Subset of REAL st Z c= dom (sec (#) arctan) & Z c= ].(- 1),1.[ holds ( sec (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((sec (#) arctan) `| Z) . x = (((sin . x) * (arctan . x)) / ((cos . x) ^2)) + (1 / ((cos . x) * (1 + (x ^2)))) ) ) proofend; ::f.x=sec.x*arccot.x theorem :: FDIFF_11:34 for Z being open Subset of REAL st Z c= dom (sec (#) arccot) & Z c= ].(- 1),1.[ holds ( sec (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((sec (#) arccot) `| Z) . x = (((sin . x) * (arccot . x)) / ((cos . x) ^2)) - (1 / ((cos . x) * (1 + (x ^2)))) ) ) proofend; ::f.x=cosec.x*arctan.x theorem :: FDIFF_11:35 for Z being open Subset of REAL st Z c= dom (cosec (#) arctan) & Z c= ].(- 1),1.[ holds ( cosec (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((cosec (#) arctan) `| Z) . x = (- (((cos . x) * (arctan . x)) / ((sin . x) ^2))) + (1 / ((sin . x) * (1 + (x ^2)))) ) ) proofend; ::f.x=cosec.x*arccot.x theorem :: FDIFF_11:36 for Z being open Subset of REAL st Z c= dom (cosec (#) arccot) & Z c= ].(- 1),1.[ holds ( cosec (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((cosec (#) arccot) `| Z) . x = (- (((cos . x) * (arccot . x)) / ((sin . x) ^2))) - (1 / ((sin . x) * (1 + (x ^2)))) ) ) proofend; ::f.x=arctan.x+arccot.x theorem Th37: :: FDIFF_11:37 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( arctan + arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan + arccot) `| Z) . x = 0 ) ) proofend; ::f.x=arctan.x-arccot.x theorem Th38: :: FDIFF_11:38 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( arctan - arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan - arccot) `| Z) . x = 2 / (1 + (x ^2)) ) ) proofend; ::f.x=sin.x*(arctan.x+arccot.x) theorem :: FDIFF_11:39 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( sin (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (arctan + arccot)) `| Z) . x = (cos . x) * ((arctan . x) + (arccot . x)) ) ) proofend; ::f.x=sin.x*(arctan.x-arccot.x) theorem :: FDIFF_11:40 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( sin (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) (arctan - arccot)) `| Z) . x = ((cos . x) * ((arctan . x) - (arccot . x))) + ((2 * (sin . x)) / (1 + (x ^2))) ) ) proofend; ::f.x=cos.x*(arctan.x+arccot.x) theorem :: FDIFF_11:41 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( cos (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (arctan + arccot)) `| Z) . x = - ((sin . x) * ((arctan . x) + (arccot . x))) ) ) proofend; ::f.x=cos.x*(arctan.x-arccot.x) theorem :: FDIFF_11:42 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( cos (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos (#) (arctan - arccot)) `| Z) . x = (- ((sin . x) * ((arctan . x) - (arccot . x)))) + ((2 * (cos . x)) / (1 + (x ^2))) ) ) proofend; ::f.x=tan.x*(arctan.x+arccot.x) theorem :: FDIFF_11:43 for Z being open Subset of REAL st Z c= dom tan & Z c= ].(- 1),1.[ holds ( tan (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan (#) (arctan + arccot)) `| Z) . x = ((arctan . x) + (arccot . x)) / ((cos . x) ^2) ) ) proofend; ::f.x=tan.x*(arctan.x-arccot.x) theorem :: FDIFF_11:44 for Z being open Subset of REAL st Z c= dom tan & Z c= ].(- 1),1.[ holds ( tan (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((tan (#) (arctan - arccot)) `| Z) . x = (((arctan . x) - (arccot . x)) / ((cos . x) ^2)) + ((2 * (tan . x)) / (1 + (x ^2))) ) ) proofend; ::f.x=cot.x*(arctan.x+arccot.x) theorem :: FDIFF_11:45 for Z being open Subset of REAL st Z c= dom cot & Z c= ].(- 1),1.[ holds ( cot (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot (#) (arctan + arccot)) `| Z) . x = - (((arctan . x) + (arccot . x)) / ((sin . x) ^2)) ) ) proofend; ::f.x=cot.x*(arctan.x-arccot.x) theorem :: FDIFF_11:46 for Z being open Subset of REAL st Z c= dom cot & Z c= ].(- 1),1.[ holds ( cot (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cot (#) (arctan - arccot)) `| Z) . x = (- (((arctan . x) - (arccot . x)) / ((sin . x) ^2))) + ((2 * (cot . x)) / (1 + (x ^2))) ) ) proofend; ::f.x=sec.x*(arctan.x+arccot.x) theorem :: FDIFF_11:47 for Z being open Subset of REAL st Z c= dom sec & Z c= ].(- 1),1.[ holds ( sec (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sec (#) (arctan + arccot)) `| Z) . x = (((arctan . x) + (arccot . x)) * (sin . x)) / ((cos . x) ^2) ) ) proofend; ::f.x=sec.x*(arctan.x-arccot.x) theorem :: FDIFF_11:48 for Z being open Subset of REAL st Z c= dom sec & Z c= ].(- 1),1.[ holds ( sec (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sec (#) (arctan - arccot)) `| Z) . x = ((((arctan . x) - (arccot . x)) * (sin . x)) / ((cos . x) ^2)) + ((2 * (sec . x)) / (1 + (x ^2))) ) ) proofend; ::f.x=cosec.x*(arctan.x+arccot.x) theorem :: FDIFF_11:49 for Z being open Subset of REAL st Z c= dom cosec & Z c= ].(- 1),1.[ holds ( cosec (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cosec (#) (arctan + arccot)) `| Z) . x = - ((((arctan . x) + (arccot . x)) * (cos . x)) / ((sin . x) ^2)) ) ) proofend; ::f.x=cosec.x*(arctan.x-arccot.x) theorem :: FDIFF_11:50 for Z being open Subset of REAL st Z c= dom cosec & Z c= ].(- 1),1.[ holds ( cosec (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cosec (#) (arctan - arccot)) `| Z) . x = (- ((((arctan . x) - (arccot . x)) * (cos . x)) / ((sin . x) ^2))) + ((2 * (cosec . x)) / (1 + (x ^2))) ) ) proofend; ::f.x=exp_R.x*(arctan.x+arccot.x) theorem :: FDIFF_11:51 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( exp_R (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (arctan + arccot)) `| Z) . x = (exp_R . x) * ((arctan . x) + (arccot . x)) ) ) proofend; ::f.x=exp_R.x*(arctan.x-arccot.x) theorem :: FDIFF_11:52 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( exp_R (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (arctan - arccot)) `| Z) . x = ((exp_R . x) * ((arctan . x) - (arccot . x))) + ((2 * (exp_R . x)) / (1 + (x ^2))) ) ) proofend; ::f.x=(arctan.x+arccot.x)/exp_R.x theorem :: FDIFF_11:53 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( (arctan + arccot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((arctan + arccot) / exp_R) `| Z) . x = - (((arctan . x) + (arccot . x)) / (exp_R . x)) ) ) proofend; ::f.x=(arctan.x-arccot.x)/exp_R.x theorem :: FDIFF_11:54 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( (arctan - arccot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((arctan - arccot) / exp_R) `| Z) . x = (((2 / (1 + (x ^2))) - (arctan . x)) + (arccot . x)) / (exp_R . x) ) ) proofend; ::f.x=exp_R.(arctan.x+arccot.x) theorem :: FDIFF_11:55 for Z being open Subset of REAL st Z c= dom (exp_R * (arctan + arccot)) & Z c= ].(- 1),1.[ holds ( exp_R * (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (arctan + arccot)) `| Z) . x = 0 ) ) proofend; ::f.x=exp_R.(arctan.x-arccot.x) theorem :: FDIFF_11:56 for Z being open Subset of REAL st Z c= dom (exp_R * (arctan - arccot)) & Z c= ].(- 1),1.[ holds ( exp_R * (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * (arctan - arccot)) `| Z) . x = (2 * (exp_R . ((arctan . x) - (arccot . x)))) / (1 + (x ^2)) ) ) proofend; ::f.x=sin.(arctan.x+arccot.x) theorem :: FDIFF_11:57 for Z being open Subset of REAL st Z c= dom (sin * (arctan + arccot)) & Z c= ].(- 1),1.[ holds ( sin * (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (arctan + arccot)) `| Z) . x = 0 ) ) proofend; ::f.x=sin.(arctan.x-arccot.x) theorem :: FDIFF_11:58 for Z being open Subset of REAL st Z c= dom (sin * (arctan - arccot)) & Z c= ].(- 1),1.[ holds ( sin * (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * (arctan - arccot)) `| Z) . x = (2 * (cos . ((arctan . x) - (arccot . x)))) / (1 + (x ^2)) ) ) proofend; ::f.x=cos.(arctan.x+arccot.x) theorem :: FDIFF_11:59 for Z being open Subset of REAL st Z c= dom (cos * (arctan + arccot)) & Z c= ].(- 1),1.[ holds ( cos * (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (arctan + arccot)) `| Z) . x = 0 ) ) proofend; ::f.x=cos.(arctan.x-arccot.x) theorem :: FDIFF_11:60 for Z being open Subset of REAL st Z c= dom (cos * (arctan - arccot)) & Z c= ].(- 1),1.[ holds ( cos * (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * (arctan - arccot)) `| Z) . x = - ((2 * (sin . ((arctan . x) - (arccot . x)))) / (1 + (x ^2))) ) ) proofend; ::f.x=arctan.x*arccot.x theorem :: FDIFF_11:61 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( arctan (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan (#) arccot) `| Z) . x = ((arccot . x) - (arctan . x)) / (1 + (x ^2)) ) ) proofend; ::f.x=arctan.(1/x)*arccot.(1/x) theorem :: FDIFF_11:62 for Z being open Subset of REAL st not 0 in Z & Z c= dom ((arctan * ((id Z) ^)) (#) (arccot * ((id Z) ^))) & ( for x being Real st x in Z holds ( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds ( (arctan * ((id Z) ^)) (#) (arccot * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((arctan * ((id Z) ^)) (#) (arccot * ((id Z) ^))) `| Z) . x = ((arctan . (1 / x)) - (arccot . (1 / x))) / (1 + (x ^2)) ) ) proofend; ::f.x=x*arctan(1/x) theorem :: FDIFF_11:63 for Z being open Subset of REAL st not 0 in Z & Z c= dom ((id Z) (#) (arctan * ((id Z) ^))) & ( for x being Real st x in Z holds ( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds ( (id Z) (#) (arctan * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arctan * ((id Z) ^))) `| Z) . x = (arctan . (1 / x)) - (x / (1 + (x ^2))) ) ) proofend; ::f.x=x*arccot(1/x) theorem :: FDIFF_11:64 for Z being open Subset of REAL st not 0 in Z & Z c= dom ((id Z) (#) (arccot * ((id Z) ^))) & ( for x being Real st x in Z holds ( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds ( (id Z) (#) (arccot * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arccot * ((id Z) ^))) `| Z) . x = (arccot . (1 / x)) + (x / (1 + (x ^2))) ) ) proofend; ::f.x=x^2*arctan(1/x) theorem :: FDIFF_11:65 for Z being open Subset of REAL for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (arctan * ((id Z) ^))) & g = #Z 2 & ( for x being Real st x in Z holds ( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds ( g (#) (arctan * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (arctan * ((id Z) ^))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2))) ) ) proofend; ::f.x=x^2*arccot(1/x) theorem :: FDIFF_11:66 for Z being open Subset of REAL for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (arccot * ((id Z) ^))) & g = #Z 2 & ( for x being Real st x in Z holds ( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds ( g (#) (arccot * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (arccot * ((id Z) ^))) `| Z) . x = ((2 * x) * (arccot . (1 / x))) + ((x ^2) / (1 + (x ^2))) ) ) proofend; ::f.x=1/arctan.x theorem Th67: :: FDIFF_11:67 for Z being open Subset of REAL st Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arctan . x <> 0 ) holds ( arctan ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan ^) `| Z) . x = - (1 / (((arctan . x) ^2) * (1 + (x ^2)))) ) ) proofend; ::f.x=1/arccot.x theorem Th68: :: FDIFF_11:68 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( arccot ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) ) ) proofend; ::f.x=1/(n*(arctan.x)|^n) theorem :: FDIFF_11:69 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * (arctan ^))) & Z c= ].(- 1),1.[ & n > 0 & ( for x being Real st x in Z holds arctan . x <> 0 ) holds ( (1 / n) (#) ((#Z n) * (arctan ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * (arctan ^))) `| Z) . x = - (1 / (((arctan . x) #Z (n + 1)) * (1 + (x ^2)))) ) ) proofend; ::f.x=1/(n*(arccot.x)|^n) theorem :: FDIFF_11:70 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * (arccot ^))) & Z c= ].(- 1),1.[ & n > 0 holds ( (1 / n) (#) ((#Z n) * (arccot ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * (arccot ^))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2))) ) ) proofend; ::f.x=2*(arctan #R (1/2)) theorem :: FDIFF_11:71 for Z being open Subset of REAL st Z c= dom (2 (#) ((#R (1 / 2)) * arctan)) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arctan . x > 0 ) holds ( 2 (#) ((#R (1 / 2)) * arctan) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * arctan)) `| Z) . x = ((arctan . x) #R (- (1 / 2))) / (1 + (x ^2)) ) ) proofend; ::f.x=2*(arccot #R (1/2)) theorem :: FDIFF_11:72 for Z being open Subset of REAL st Z c= dom (2 (#) ((#R (1 / 2)) * arccot)) & Z c= ].(- 1),1.[ holds ( 2 (#) ((#R (1 / 2)) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * arccot)) `| Z) . x = - (((arccot . x) #R (- (1 / 2))) / (1 + (x ^2))) ) ) proofend; ::f.x=(2/3)*(arctan #R (3/2)) theorem :: FDIFF_11:73 for Z being open Subset of REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * arctan)) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arctan . x > 0 ) holds ( (2 / 3) (#) ((#R (3 / 2)) * arctan) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * arctan)) `| Z) . x = ((arctan . x) #R (1 / 2)) / (1 + (x ^2)) ) ) proofend; ::f.x=(2/3)*(arccot #R (3/2)) theorem :: FDIFF_11:74 for Z being open Subset of REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * arccot)) & Z c= ].(- 1),1.[ holds ( (2 / 3) (#) ((#R (3 / 2)) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * arccot)) `| Z) . x = - (((arccot . x) #R (1 / 2)) / (1 + (x ^2))) ) ) proofend;