:: Several Differentiation Formulas of Special Functions -- Part {VII} :: by Fuguo Ge and Bing Xie :: :: Received September 23, 2008 :: Copyright (c) 2008-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, SUBSET_1, RCOMP_1, PARTFUN1, TARSKI, RELAT_1, SIN_COS9, SIN_COS, FUNCT_1, XXREAL_0, ARYTM_1, ARYTM_3, FDIFF_1, SQUARE_1, CARD_1, XXREAL_1, SIN_COS4, VALUED_1, XBOOLE_0, ORDINAL4, PREPOWER; notations TARSKI, SUBSET_1, XXREAL_0, FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, RCOMP_1, SIN_COS, RFUNCT_1, SQUARE_1, VALUED_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FDIFF_1, PARTFUN2, TAYLOR_1, PREPOWER, FDIFF_9, SIN_COS9; constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, SIN_COS, PARTFUN2, TOPALG_2, TAYLOR_1, PREPOWER, LIMFUNC1, FDIFF_9, SIN_COS9, COMPLEX1; registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1, SIN_COS6, NUMBERS, INT_1, VALUED_0, SQUARE_1, PREPOWER; requirements SUBSET, NUMERALS, ARITHM, REAL; begin reserve x for Real, n for Element of NAT, y for set, Z for open Subset of REAL, g for PartFunc of REAL,REAL; ::f.x=arctan.(sin.x) theorem :: FDIFF_11:1 Z c= dom (arctan*sin) & (for x st x in Z holds sin.x > -1 & sin.x < 1) implies arctan*sin is_differentiable_on Z & for x st x in Z holds ((arctan*sin) `|Z).x = cos.x/(1+(sin.x)^2); ::f.x=arccot.(sin.x) theorem :: FDIFF_11:2 Z c= dom (arccot*sin) & (for x st x in Z holds sin.x > -1 & sin.x < 1) implies arccot*sin is_differentiable_on Z & for x st x in Z holds ((arccot*sin) `|Z).x = -cos.x/(1+(sin.x)^2); ::f.x=arctan.(cos.x) theorem :: FDIFF_11:3 Z c= dom (arctan*cos) & (for x st x in Z holds cos.x > -1 & cos.x < 1) implies arctan*cos is_differentiable_on Z & for x st x in Z holds ((arctan*cos) `|Z).x = -sin.x/(1+(cos.x)^2); ::f.x=arccot.(cos.x) theorem :: FDIFF_11:4 Z c= dom (arccot*cos) & (for x st x in Z holds cos.x > -1 & cos.x < 1) implies arccot*cos is_differentiable_on Z & for x st x in Z holds ((arccot*cos) `|Z).x = sin.x/(1+(cos.x)^2); ::f.x=arctan.(tan.x) theorem :: FDIFF_11:5 Z c= dom (arctan*tan) & (for x st x in Z holds tan.x > -1 & tan.x < 1) implies arctan*tan is_differentiable_on Z & for x st x in Z holds ((arctan*tan) `|Z).x = 1; ::f.x=arccot.(tan.x) theorem :: FDIFF_11:6 Z c= dom (arccot*tan) & (for x st x in Z holds tan.x > -1 & tan.x < 1) implies arccot*tan is_differentiable_on Z & for x st x in Z holds ((arccot*tan) `|Z).x = -1; ::f.x=arctan.(cot.x) theorem :: FDIFF_11:7 Z c= dom (arctan*cot) & (for x st x in Z holds cot.x > -1 & cot.x < 1) implies arctan*cot is_differentiable_on Z & for x st x in Z holds ((arctan*cot) `|Z).x = -1; ::f.x=arccot.(cot.x) theorem :: FDIFF_11:8 Z c= dom (arccot*cot) & (for x st x in Z holds cot.x > -1 & cot.x < 1) implies arccot*cot is_differentiable_on Z & for x st x in Z holds ((arccot*cot) `|Z).x = 1; ::f.x=arctan.(arctan.x) theorem :: FDIFF_11:9 Z c= dom (arctan*arctan) & Z c= ].-1,1.[ & (for x st x in Z holds arctan.x > -1 & arctan.x < 1) implies arctan*arctan is_differentiable_on Z & for x st x in Z holds ((arctan*arctan)`|Z).x = 1/((1+x^2)*(1+(arctan.x)^2)); ::f.x=arccot.(arctan.x) theorem :: FDIFF_11:10 Z c= dom (arccot*arctan) & Z c= ].-1,1.[ & (for x st x in Z holds arctan.x > -1 & arctan.x < 1) implies arccot*arctan is_differentiable_on Z & for x st x in Z holds ((arccot*arctan)`|Z).x = -1/((1+x^2)*(1+(arctan.x)^2)); ::f.x=arctan.(arccot.x) theorem :: FDIFF_11:11 Z c= dom (arctan*arccot) & Z c= ].-1,1.[ & (for x st x in Z holds arccot.x > -1 & arccot.x < 1) implies arctan*arccot is_differentiable_on Z & for x st x in Z holds ((arctan*arccot)`|Z).x = -1/((1+x^2)*(1+(arccot.x)^2)); ::f.x=arccot.(arccot.x) theorem :: FDIFF_11:12 Z c= dom (arccot*arccot) & Z c= ].-1,1.[ & (for x st x in Z holds arccot.x > -1 & arccot.x < 1) implies arccot*arccot is_differentiable_on Z & for x st x in Z holds ((arccot*arccot)`|Z).x = 1/((1+x^2)*(1+(arccot.x)^2)); ::f.x=sin.(arctan.x) theorem :: FDIFF_11:13 Z c= dom (sin*arctan) & Z c= ].-1,1.[ implies sin*arctan is_differentiable_on Z & for x st x in Z holds ((sin*arctan)`|Z).x = cos.( arctan.x)/(1+x^2); ::f.x=sin.(arccot.x) theorem :: FDIFF_11:14 Z c= dom (sin*arccot) & Z c= ].-1,1.[ implies sin*arccot is_differentiable_on Z & for x st x in Z holds ((sin*arccot)`|Z).x = -cos.( arccot.x)/(1+x^2); ::f.x=cos.(arctan.x) theorem :: FDIFF_11:15 Z c= dom (cos*arctan) & Z c= ].-1,1.[ implies cos*arctan is_differentiable_on Z & for x st x in Z holds ((cos*arctan)`|Z).x = -sin.( arctan.x)/(1+x^2); ::f.x=cos.(arccot.x) theorem :: FDIFF_11:16 Z c= dom (cos*arccot) & Z c= ].-1,1.[ implies cos*arccot is_differentiable_on Z & for x st x in Z holds ((cos*arccot)`|Z).x = sin.( arccot.x)/(1+x^2); ::f.x=tan.(arctan.x) theorem :: FDIFF_11:17 Z c= dom (tan*arctan) & Z c= ].-1,1.[ implies tan*arctan is_differentiable_on Z & for x st x in Z holds ((tan*arctan)`|Z).x = 1/((cos.( arctan.x))^2*(1+x^2)); ::f.x=tan.(arccot.x) theorem :: FDIFF_11:18 Z c= dom (tan*arccot) & Z c= ].-1,1.[ implies tan*arccot is_differentiable_on Z & for x st x in Z holds ((tan*arccot)`|Z).x = -1/((cos.( arccot.x))^2*(1+x^2)); ::f.x=cot.(arctan.x) theorem :: FDIFF_11:19 Z c= dom (cot*arctan) & Z c= ].-1,1.[ implies cot*arctan is_differentiable_on Z & for x st x in Z holds ((cot*arctan)`|Z).x = -1/((sin.( arctan.x))^2*(1+x^2)); ::f.x=cot.(arccot.x) theorem :: FDIFF_11:20 Z c= dom (cot*arccot) & Z c= ].-1,1.[ implies cot*arccot is_differentiable_on Z & for x st x in Z holds ((cot*arccot)`|Z).x = 1/((sin.( arccot.x))^2*(1+x^2)); ::f.x=sec.(arctan.x) theorem :: FDIFF_11:21 Z c= dom (sec*arctan) & Z c= ].-1,1.[ implies sec*arctan is_differentiable_on Z & for x st x in Z holds ((sec*arctan)`|Z).x = sin.( arctan.x)/((cos.(arctan.x))^2*(1+x^2)); ::f.x=sec.(arccot.x) theorem :: FDIFF_11:22 Z c= dom (sec*arccot) & Z c= ].-1,1.[ implies sec*arccot is_differentiable_on Z & for x st x in Z holds ((sec*arccot)`|Z).x = -sin.( arccot.x)/((cos.(arccot.x))^2*(1+x^2)); ::f.x=cosec.(arctan.x) theorem :: FDIFF_11:23 Z c= dom (cosec*arctan) & Z c= ].-1,1.[ implies cosec*arctan is_differentiable_on Z & for x st x in Z holds ((cosec*arctan)`|Z).x = -cos.( arctan.x)/((sin.(arctan.x))^2*(1+x^2)); ::f.x=cosec.(arccot.x) theorem :: FDIFF_11:24 Z c= dom (cosec*arccot) & Z c= ].-1,1.[ implies cosec*arccot is_differentiable_on Z & for x st x in Z holds ((cosec*arccot)`|Z).x = cos.( arccot.x)/((sin.(arccot.x))^2*(1+x^2)); ::f.x=sin.x*arctan.x theorem :: FDIFF_11:25 Z c= dom (sin(#)arctan) & Z c= ].-1,1.[ implies (sin(#)arctan) is_differentiable_on Z & for x st x in Z holds ((sin(#)arctan)`|Z).x = cos.x* arctan.x+sin.x/(1+x^2); ::f.x=sin.x*arccot.x theorem :: FDIFF_11:26 Z c= dom (sin(#)arccot) & Z c= ].-1,1.[ implies (sin(#)arccot) is_differentiable_on Z & for x st x in Z holds ((sin(#)arccot)`|Z).x = cos.x* arccot.x-sin.x/(1+x^2); ::f.x=cos.x*arctan.x theorem :: FDIFF_11:27 Z c= dom (cos(#)arctan) & Z c= ].-1,1.[ implies (cos(#)arctan) is_differentiable_on Z & for x st x in Z holds ((cos(#)arctan)`|Z).x = -sin.x* arctan.x+cos.x/(1+x^2); ::f.x=cos.x*arccot.x theorem :: FDIFF_11:28 Z c= dom (cos(#)arccot) & Z c= ].-1,1.[ implies (cos(#)arccot) is_differentiable_on Z & for x st x in Z holds ((cos(#)arccot)`|Z).x = -sin.x* arccot.x-cos.x/(1+x^2); ::f.x=tan.x*arctan.x theorem :: FDIFF_11:29 Z c= dom (tan(#)arctan) & Z c= ].-1,1.[ implies (tan(#)arctan) is_differentiable_on Z & for x st x in Z holds ((tan(#)arctan)`|Z).x = arctan.x /(cos.x)^2+tan.x/(1+x^2); ::f.x=tan.x*arccot.x theorem :: FDIFF_11:30 Z c= dom (tan(#)arccot) & Z c= ].-1,1.[ implies (tan(#)arccot) is_differentiable_on Z & for x st x in Z holds ((tan(#)arccot)`|Z).x = arccot.x /(cos.x)^2-tan.x/(1+x^2); ::f.x=cot.x*arctan.x theorem :: FDIFF_11:31 Z c= dom (cot(#)arctan) & Z c= ].-1,1.[ implies (cot(#)arctan) is_differentiable_on Z & for x st x in Z holds ((cot(#)arctan)`|Z).x = -arctan. x/(sin.x)^2+cot.x/(1+x^2); ::f.x=cot.x*arccot.x theorem :: FDIFF_11:32 Z c= dom (cot(#)arccot) & Z c= ].-1,1.[ implies (cot(#)arccot) is_differentiable_on Z & for x st x in Z holds ((cot(#)arccot)`|Z).x = -arccot. x/(sin.x)^2-cot.x/(1+x^2); ::f.x=sec.x*arctan.x theorem :: FDIFF_11:33 Z c= dom (sec(#)arctan) & Z c= ].-1,1.[ implies (sec(#)arctan) is_differentiable_on Z & for x st x in Z holds ((sec(#)arctan)`|Z).x = (sin.x* arctan.x)/(cos.x)^2+1/(cos.x*(1+x^2)); ::f.x=sec.x*arccot.x theorem :: FDIFF_11:34 Z c= dom (sec(#)arccot) & Z c= ].-1,1.[ implies (sec(#)arccot) is_differentiable_on Z & for x st x in Z holds ((sec(#)arccot)`|Z).x = (sin.x* arccot.x)/(cos.x)^2-1/(cos.x*(1+x^2)); ::f.x=cosec.x*arctan.x theorem :: FDIFF_11:35 Z c= dom (cosec(#)arctan) & Z c= ].-1,1.[ implies (cosec(#)arctan) is_differentiable_on Z & for x st x in Z holds ((cosec(#)arctan)`|Z).x = -(cos. x*arctan.x)/(sin.x)^2+1/(sin.x*(1+x^2)); ::f.x=cosec.x*arccot.x theorem :: FDIFF_11:36 Z c= dom (cosec(#)arccot) & Z c= ].-1,1.[ implies (cosec(#)arccot) is_differentiable_on Z & for x st x in Z holds ((cosec(#)arccot)`|Z).x = -(cos. x*arccot.x)/(sin.x)^2-1/(sin.x*(1+x^2)); ::f.x=arctan.x+arccot.x theorem :: FDIFF_11:37 Z c= ].-1,1.[ implies (arctan+arccot) is_differentiable_on Z & for x st x in Z holds ((arctan+arccot)`|Z).x = 0; ::f.x=arctan.x-arccot.x theorem :: FDIFF_11:38 Z c= ].-1,1.[ implies (arctan-arccot) is_differentiable_on Z & for x st x in Z holds ((arctan-arccot)`|Z).x = 2/(1+x^2); ::f.x=sin.x*(arctan.x+arccot.x) theorem :: FDIFF_11:39 Z c= ].-1,1.[ implies sin(#)(arctan+arccot) is_differentiable_on Z & for x st x in Z holds ((sin(#)(arctan+arccot))`|Z).x = cos.x*(arctan.x+arccot.x ); ::f.x=sin.x*(arctan.x-arccot.x) theorem :: FDIFF_11:40 Z c= ].-1,1.[ implies sin(#)(arctan-arccot) is_differentiable_on Z & for x st x in Z holds ((sin(#)(arctan-arccot))`|Z).x = cos.x*(arctan.x-arccot.x )+2*sin.x/(1+x^2); ::f.x=cos.x*(arctan.x+arccot.x) theorem :: FDIFF_11:41 Z c= ].-1,1.[ implies cos(#)(arctan+arccot) is_differentiable_on Z & for x st x in Z holds ((cos(#)(arctan+arccot))`|Z).x = -sin.x*(arctan.x+arccot. x); ::f.x=cos.x*(arctan.x-arccot.x) theorem :: FDIFF_11:42 Z c= ].-1,1.[ implies cos(#)(arctan-arccot) is_differentiable_on Z & for x st x in Z holds ((cos(#)(arctan-arccot))`|Z).x = -sin.x*(arctan.x-arccot. x)+2*cos.x/(1+x^2); ::f.x=tan.x*(arctan.x+arccot.x) theorem :: FDIFF_11:43 Z c= dom tan & Z c= ].-1,1.[ implies tan(#)(arctan+arccot) is_differentiable_on Z & for x st x in Z holds ((tan(#)(arctan+arccot))`|Z).x = (arctan.x+arccot.x)/(cos.x)^2; ::f.x=tan.x*(arctan.x-arccot.x) theorem :: FDIFF_11:44 Z c= dom tan & Z c= ].-1,1.[ implies tan(#)(arctan-arccot) is_differentiable_on Z & for x st x in Z holds ((tan(#)(arctan-arccot))`|Z).x = (arctan.x-arccot.x)/(cos.x)^2+2*tan.x/(1+x^2); ::f.x=cot.x*(arctan.x+arccot.x) theorem :: FDIFF_11:45 Z c= dom cot & Z c= ].-1,1.[ implies cot(#)(arctan+arccot) is_differentiable_on Z & for x st x in Z holds ((cot(#)(arctan+arccot))`|Z).x = -(arctan.x+arccot.x)/(sin.x)^2; ::f.x=cot.x*(arctan.x-arccot.x) theorem :: FDIFF_11:46 Z c= dom cot & Z c= ].-1,1.[ implies cot(#)(arctan-arccot) is_differentiable_on Z & for x st x in Z holds ((cot(#)(arctan-arccot))`|Z).x = -(arctan.x-arccot.x)/(sin.x)^2+2*cot.x/(1+x^2); ::f.x=sec.x*(arctan.x+arccot.x) theorem :: FDIFF_11:47 Z c= dom sec & Z c= ].-1,1.[ implies sec(#)(arctan+arccot) is_differentiable_on Z & for x st x in Z holds ((sec(#)(arctan+arccot))`|Z).x = (arctan.x+arccot.x)*sin.x/(cos.x)^2; ::f.x=sec.x*(arctan.x-arccot.x) theorem :: FDIFF_11:48 Z c= dom sec & Z c= ].-1,1.[ implies sec(#)(arctan-arccot) is_differentiable_on Z & for x 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); ::f.x=cosec.x*(arctan.x+arccot.x) theorem :: FDIFF_11:49 Z c= dom cosec & Z c= ].-1,1.[ implies cosec(#)(arctan+arccot) is_differentiable_on Z & for x st x in Z holds ((cosec(#)(arctan+arccot))`|Z).x = -(arctan.x+arccot.x)*cos.x/(sin.x)^2; ::f.x=cosec.x*(arctan.x-arccot.x) theorem :: FDIFF_11:50 Z c= dom cosec & Z c= ].-1,1.[ implies cosec(#)(arctan-arccot) is_differentiable_on Z & for x 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); ::f.x=exp_R.x*(arctan.x+arccot.x) theorem :: FDIFF_11:51 Z c= ].-1,1.[ implies exp_R(#)(arctan+arccot) is_differentiable_on Z & for x st x in Z holds ((exp_R(#)(arctan+arccot))`|Z).x = exp_R.x*(arctan.x+ arccot.x); ::f.x=exp_R.x*(arctan.x-arccot.x) theorem :: FDIFF_11:52 Z c= ].-1,1.[ implies exp_R(#)(arctan-arccot) is_differentiable_on Z & for x 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); ::f.x=(arctan.x+arccot.x)/exp_R.x theorem :: FDIFF_11:53 Z c= ].-1,1.[ implies (arctan+arccot)/exp_R is_differentiable_on Z & for x st x in Z holds (((arctan+arccot)/exp_R)`|Z).x = -(arctan.x+arccot.x)/ exp_R.x; ::f.x=(arctan.x-arccot.x)/exp_R.x theorem :: FDIFF_11:54 Z c= ].-1,1.[ implies (arctan-arccot)/exp_R is_differentiable_on Z & for x st x in Z holds (((arctan-arccot)/exp_R)`|Z).x = ((2/(1+x^2))-arctan.x+ arccot.x)/exp_R.x; ::f.x=exp_R.(arctan.x+arccot.x) theorem :: FDIFF_11:55 Z c= dom (exp_R*(arctan+arccot)) & Z c= ].-1,1.[ implies exp_R*(arctan +arccot) is_differentiable_on Z & for x st x in Z holds (exp_R*(arctan+arccot) `|Z).x = 0; ::f.x=exp_R.(arctan.x-arccot.x) theorem :: FDIFF_11:56 Z c= dom (exp_R*(arctan-arccot)) & Z c= ].-1,1.[ implies exp_R*(arctan -arccot) is_differentiable_on Z & for x st x in Z holds (exp_R*(arctan-arccot) `|Z).x = 2*exp_R.(arctan.x-arccot.x)/(1+x^2); ::f.x=sin.(arctan.x+arccot.x) theorem :: FDIFF_11:57 Z c= dom (sin*(arctan+arccot)) & Z c= ].-1,1.[ implies sin*(arctan+ arccot) is_differentiable_on Z & for x st x in Z holds (sin*(arctan+arccot)`|Z) .x = 0; ::f.x=sin.(arctan.x-arccot.x) theorem :: FDIFF_11:58 Z c= dom (sin*(arctan-arccot)) & Z c= ].-1,1.[ implies sin*(arctan- arccot) is_differentiable_on Z & for x st x in Z holds (sin*(arctan-arccot)`|Z) .x = 2*cos.(arctan.x-arccot.x)/(1+x^2); ::f.x=cos.(arctan.x+arccot.x) theorem :: FDIFF_11:59 Z c= dom (cos*(arctan+arccot)) & Z c= ].-1,1.[ implies cos*(arctan+ arccot) is_differentiable_on Z & for x st x in Z holds (cos*(arctan+arccot)`|Z) .x = 0; ::f.x=cos.(arctan.x-arccot.x) theorem :: FDIFF_11:60 Z c= dom (cos*(arctan-arccot)) & Z c= ].-1,1.[ implies cos*(arctan- arccot) is_differentiable_on Z & for x st x in Z holds (cos*(arctan-arccot)`|Z) .x = -2*sin.(arctan.x-arccot.x)/(1+x^2); ::f.x=arctan.x*arccot.x theorem :: FDIFF_11:61 Z c= ].-1,1.[ implies arctan(#)arccot is_differentiable_on Z & for x st x in Z holds ((arctan(#)arccot)`|Z).x = (arccot.x-arctan.x)/(1+x^2); ::f.x=arctan.(1/x)*arccot.(1/x) theorem :: FDIFF_11:62 not 0 in Z & Z c= dom((arctan*((id Z)^))(#)(arccot*((id Z)^))) & (for x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (arctan*((id Z)^) )(#)(arccot*((id Z)^)) is_differentiable_on Z & for x st x in Z holds (((arctan *((id Z)^))(#)(arccot*((id Z)^)))`|Z).x = (arctan.(1/x)-arccot.(1/x))/(1+x^2) ; ::f.x=x*arctan(1/x) theorem :: FDIFF_11:63 not 0 in Z & Z c= dom ((id Z)(#)(arctan*((id Z)^))) & (for x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (id Z)(#)(arctan*((id Z)^)) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arctan*((id Z)^)))`| Z).x = arctan.(1/x)-x/(1+x^2); ::f.x=x*arccot(1/x) theorem :: FDIFF_11:64 not 0 in Z & Z c= dom ((id Z)(#)(arccot*((id Z)^))) & (for x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (id Z)(#)(arccot*((id Z)^)) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arccot*((id Z)^)))`| Z).x = arccot.(1/x)+x/(1+x^2); ::f.x=x^2*arctan(1/x) theorem :: FDIFF_11:65 not 0 in Z & Z c= dom (g(#)(arctan*((id Z)^))) & g=#Z 2 & (for x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies g(#)(arctan*((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((g(#)(arctan*((id Z)^)))`|Z).x = 2*x*arctan.(1/x)-x^2/(1+x^2); ::f.x=x^2*arccot(1/x) theorem :: FDIFF_11:66 not 0 in Z & Z c= dom (g(#)(arccot*((id Z)^))) & g=#Z 2 & (for x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies g(#)(arccot*((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((g(#)(arccot*((id Z)^)))`|Z).x = 2*x*arccot.(1/x)+x^2/(1+x^2); ::f.x=1/arctan.x theorem :: FDIFF_11:67 Z c= ].-1,1.[ & (for x st x in Z holds arctan.x<>0) implies arctan^ is_differentiable_on Z & for x st x in Z holds ((arctan^)`|Z).x = -1/(( arctan.x)^2*(1+x^2)); ::f.x=1/arccot.x theorem :: FDIFF_11:68 Z c= ].-1,1.[ implies arccot^ is_differentiable_on Z & for x st x in Z holds ((arccot^)`|Z).x= 1/((arccot.x)^2*(1+x^2)); ::f.x=1/(n*(arctan.x)|^n) theorem :: FDIFF_11:69 Z c= dom ((1/n)(#)(( #Z n)*(arctan^))) & Z c= ].-1,1.[ & n>0 & (for x st x in Z holds arctan.x<>0) implies (1/n)(#)(( #Z n)*(arctan^)) is_differentiable_on Z & for x st x in Z holds (((1/n)(#)(( #Z n)*(arctan^)))`| Z).x = -1/(((arctan.x) #Z (n+1))*(1+x^2)); ::f.x=1/(n*(arccot.x)|^n) theorem :: FDIFF_11:70 Z c= dom ((1/n)(#)(( #Z n)*(arccot^))) & Z c= ].-1,1.[ & n>0 implies ( 1/n)(#)(( #Z n)*(arccot^)) is_differentiable_on Z & for x st x in Z holds (((1/ n)(#)(( #Z n)*(arccot^)))`|Z).x = 1/(((arccot.x) #Z (n+1))*(1+x^2)); ::f.x=2*(arctan #R (1/2)) theorem :: FDIFF_11:71 Z c= dom ((2(#)(( #R (1/2))*arctan))) & Z c= ].-1,1.[ & (for x st x in Z holds arctan.x > 0) implies 2(#)(( #R (1/2))*arctan) is_differentiable_on Z & for x st x in Z holds ((2(#)(( #R (1/2))*arctan))`|Z).x = (arctan.x) #R (-1/2)/ (1+x^2); ::f.x=2*(arccot #R (1/2)) theorem :: FDIFF_11:72 Z c= dom ((2(#)(( #R (1/2))*arccot))) & Z c= ].-1,1.[ implies 2(#)(( #R (1/2))*arccot) is_differentiable_on Z & for x st x in Z holds ((2(#)(( #R (1 /2))*arccot))`|Z).x = -(arccot.x) #R (-1/2)/(1+x^2); ::f.x=(2/3)*(arctan #R (3/2)) theorem :: FDIFF_11:73 Z c= dom (((2/3)(#)(( #R (3/2))*arctan))) & Z c= ].-1,1.[ & (for x st x in Z holds arctan.x > 0) implies (2/3)(#)(( #R (3/2))*arctan) is_differentiable_on Z & for x st x in Z holds (((2/3)(#)(( #R (3/2))*arctan)) `|Z).x = (arctan.x) #R (1/2)/(1+x^2); ::f.x=(2/3)*(arccot #R (3/2)) theorem :: FDIFF_11:74 Z c= dom (((2/3)(#)(( #R (3/2))*arccot))) & Z c= ].-1,1.[ implies (2/3 )(#)(( #R (3/2))*arccot) is_differentiable_on Z & for x st x in Z holds (((2/3) (#)(( #R (3/2))*arccot))`|Z).x = -(arccot.x) #R (1/2)/(1+x^2);