:: Several Differentiation Formulas of Special Functions -- Part {IV} :: by Bo Li and Peng Wang :: :: Received September 29, 2006 :: Copyright (c) 2006-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, RCOMP_1, SUBSET_1, PARTFUN1, RELAT_1, SIN_COS, FUNCT_1, CARD_1, XBOOLE_0, ORDINAL4, TARSKI, ARYTM_3, PREPOWER, NEWTON, ARYTM_1, FDIFF_1, SQUARE_1, LIMFUNC1, TAYLOR_1, XXREAL_0, VALUED_1, NAT_1; notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, RELSET_1, FUNCT_1, PARTFUN1, PARTFUN2, XCMPLX_0, XREAL_0, RCOMP_1, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS, REAL_1, NAT_1, NEWTON, VALUED_1, FDIFF_1, PREPOWER, LIMFUNC1; constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1, LIMFUNC1, FDIFF_1, PREPOWER, SIN_COS, TAYLOR_1, VALUED_1, RELSET_1, NEWTON; registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, INT_1, MEMBERED, RCOMP_1, VALUED_0, XREAL_0, SQUARE_1, PREPOWER, NEWTON; requirements SUBSET, REAL, NUMERALS, ARITHM; begin reserve x,a,b,c for Real, n for Nat, Z for open Subset of REAL, f, f1,f2 for PartFunc of REAL,REAL; theorem :: FDIFF_8:1 x in dom tan implies cos.x<>0; theorem :: FDIFF_8:2 x in dom cot implies sin.x<>0; :: ((f1/f2).x) ^ n = (f1.x) ^ n/(f2.x) ^ n theorem :: FDIFF_8:3 Z c= dom (f1/f2) implies for x st x in Z holds ((f1/f2).x) #Z n = (f1.x) #Z n/(f2.x) #Z n; :: f.x=(x+a)/(x-b) theorem :: FDIFF_8:4 Z c= dom (f1/f2) & (for x st x in Z holds f1.x=x+a & f2.x=x-b) implies (f1/f2) is_differentiable_on Z & for x st x in Z holds ((f1/f2)`|Z).x = (-a-b)/ (x-b)^2; :: f.x=ln(1/x) theorem :: FDIFF_8:5 not 0 in Z & Z c= dom (ln*((id Z)^)) implies (ln*((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((ln*((id Z)^))`|Z).x = -1/x; :: f.x = tan.(a*x+b) theorem :: FDIFF_8:6 Z c= dom (tan*f) & (for x st x in Z holds f.x = a*x+b) implies tan*f is_differentiable_on Z & for x st x in Z holds ((tan*f)`|Z).x = a/(cos.(a *x+b))^2; :: f.x = cot.(a*x+b) theorem :: FDIFF_8:7 Z c= dom (cot*f) & (for x st x in Z holds f.x = a*x+b) implies cot*f is_differentiable_on Z & for x st x in Z holds ((cot*f)`|Z).x = -a/(sin.( a*x+b))^2; :: f.x = tan.(1/x) theorem :: FDIFF_8:8 not 0 in Z & Z c= dom (tan*((id Z)^)) implies (tan*((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((tan*((id Z)^))`|Z).x = -1/(x^2 *(cos.(1/x))^2); :: f.x = cot.(1/x) theorem :: FDIFF_8:9 not 0 in Z & Z c= dom (cot*((id Z)^)) implies (cot*((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((cot*((id Z)^))`|Z).x = 1/(x^2* (sin.(1/x))^2); :: f.x = tan.(a+b*x+c*x^2) theorem :: FDIFF_8:10 Z c= dom (tan*(f1+c(#)f2)) & f2=#Z 2 & (for x st x in Z holds f1.x = a +b*x) implies tan*(f1+c(#)f2) is_differentiable_on Z & for x st x in Z holds (( tan*(f1+c(#)f2))`|Z).x = (b+2*c*x)/(cos.(a+b*x+c*x^2))^2; :: f.x = cot.(a+b*x+c*x^2) theorem :: FDIFF_8:11 Z c= dom (cot*(f1+c(#)f2)) & f2=#Z 2 & (for x st x in Z holds f1.x = a +b*x) implies cot*(f1+c(#)f2) is_differentiable_on Z & for x st x in Z holds (( cot*(f1+c(#)f2))`|Z).x = -(b+2*c*x)/(sin.(a+b*x+c*x^2))^2; :: f.x = tan.(exp_R.x) theorem :: FDIFF_8:12 Z c= dom (tan*exp_R) implies tan*exp_R is_differentiable_on Z & for x st x in Z holds ((tan*exp_R)`|Z).x = exp_R.x/(cos.(exp_R.x))^2; :: f.x = cot.(exp_R.x) theorem :: FDIFF_8:13 Z c= dom (cot*exp_R) implies cot*exp_R is_differentiable_on Z & for x st x in Z holds ((cot*exp_R)`|Z).x = -exp_R.x/(sin.(exp_R.x))^2; :: f.x = tan.(ln.x) theorem :: FDIFF_8:14 Z c= dom (tan*ln) implies tan*ln is_differentiable_on Z & for x st x in Z holds ((tan*ln)`|Z).x = 1/(x*(cos.(ln.x))^2); :: f.x = cot.(ln.x) theorem :: FDIFF_8:15 Z c= dom (cot*ln) implies cot*ln is_differentiable_on Z & for x st x in Z holds ((cot*ln)`|Z).x = -1/(x*(sin.(ln.x))^2); :: f.x = exp_R.(tan.x) theorem :: FDIFF_8:16 Z c= dom (exp_R*tan) implies exp_R*tan is_differentiable_on Z & for x st x in Z holds ((exp_R*tan)`|Z).x = exp_R.(tan.x)/(cos.x)^2; :: f.x = exp_R.(cot.x) theorem :: FDIFF_8:17 Z c= dom (exp_R*cot) implies exp_R*cot is_differentiable_on Z & for x st x in Z holds ((exp_R*cot)`|Z).x = -exp_R.(cot.x)/(sin.x)^2; :: f.x = ln.(tan.x) theorem :: FDIFF_8:18 Z c= dom (ln*tan) implies ln*tan is_differentiable_on Z & for x st x in Z holds ((ln*tan)`|Z).x = 1/(cos.x*sin.x); :: f.x = ln.(cot.x) theorem :: FDIFF_8:19 Z c= dom (ln*cot) implies ln*cot is_differentiable_on Z & for x st x in Z holds ((ln*cot)`|Z).x = -1/(sin.x*cos.x); :: f.x=(tan.x) ^ n theorem :: FDIFF_8:20 Z c= dom (( #Z n)*tan) & 1<=n implies ( #Z n)*tan is_differentiable_on Z & for x st x in Z holds ((( #Z n)*tan)`|Z).x =n*(sin.x) #Z (n-1)/(cos.x) #Z ( n+1); :: f.x=(cot.x) ^ n theorem :: FDIFF_8:21 Z c= dom (( #Z n)*cot) & 1<=n implies ( #Z n)*cot is_differentiable_on Z & for x st x in Z holds ((( #Z n)*cot)`|Z).x =-n*(cos.x) #Z (n-1)/(sin.x) #Z (n+1); :: f.x = tan.x+1/cos.x theorem :: FDIFF_8:22 (Z c= dom (tan+cos^) & for x st x in Z holds (1+sin.x)<>0 & (1-sin.x) <>0) implies tan+cos^ is_differentiable_on Z & for x st x in Z holds ((tan+cos^ )`|Z).x = 1/(1-sin.x); :: f.x = tan.x-1/cos.x theorem :: FDIFF_8:23 (Z c= dom (tan-cos^) & for x st x in Z holds (1-sin.x)<>0 & (1+sin.x) <>0) implies tan-cos^ is_differentiable_on Z & for x st x in Z holds ((tan-cos^ )`|Z).x = 1/(1+sin.x); :: f.x = tan.x-x theorem :: FDIFF_8:24 Z c= dom (tan-id Z) implies tan-id Z is_differentiable_on Z & for x st x in Z holds ((tan-id Z)`|Z).x=(sin.x)^2/(cos.x)^2; :: f.x = -cot.x-x theorem :: FDIFF_8:25 Z c= dom (-cot-id Z) implies -cot-id Z is_differentiable_on Z & for x st x in Z holds ((-cot-id Z)`|Z).x=(cos.x)^2/(sin.x)^2; :: f.x = (1/a)*tan.(a*x)-x theorem :: FDIFF_8:26 (Z c= dom ((1/a)(#)(tan*f)-id Z) & for x st x in Z holds f.x=a*x & a<> 0) implies (1/a)(#)(tan*f)-id Z is_differentiable_on Z & for x st x in Z holds (((1/a)(#)(tan*f)-id Z)`|Z).x=(sin.(a*x))^2/(cos.(a*x))^2; :: f.x = (-1/a)*cot.(a*x)-x theorem :: FDIFF_8:27 (Z c= dom ((-1/a)(#)(cot*f)-id Z) & for x st x in Z holds f.x=a*x & a <>0) implies (-1/a)(#)(cot*f)-id Z is_differentiable_on Z & for x st x in Z holds (((-1/a)(#)(cot*f)-id Z)`|Z).x=(cos.(a*x))^2/(sin.(a*x))^2; :: f.x = (a*x+b)*tan.x theorem :: FDIFF_8:28 (Z c= dom (f(#)tan) & for x st x in Z holds f.x=a*x+b) implies (f(#) tan) is_differentiable_on Z & for x st x in Z holds ((f(#)tan)`|Z).x = a*sin.x/ cos.x+(a*x+b)/(cos.x)^2; :: f.x = (a*x+b)*cot.x theorem :: FDIFF_8:29 (Z c= dom (f(#)cot) & for x st x in Z holds f.x=a*x+b) implies (f(#) cot) is_differentiable_on Z & for x st x in Z holds ((f(#)cot)`|Z).x = a*cos.x/ sin.x-(a*x+b)/(sin.x)^2; :: f.x = exp_R.x*tan.x theorem :: FDIFF_8:30 Z c= dom (exp_R(#)tan) implies (exp_R(#)tan) is_differentiable_on Z & for x st x in Z holds ((exp_R(#)tan)`|Z).x = exp_R.x*sin.x/cos.x+exp_R.x/(cos.x )^2; :: f.x = exp_R.x*cot.x theorem :: FDIFF_8:31 Z c= dom (exp_R(#)cot) implies (exp_R(#)cot) is_differentiable_on Z & for x st x in Z holds ((exp_R(#)cot)`|Z).x = exp_R.x*cos.x/sin.x-exp_R.x/(sin.x )^2; :: f.x = ln.x*tan.x theorem :: FDIFF_8:32 Z c= dom (ln(#)tan) implies (ln(#)tan) is_differentiable_on Z & for x st x in Z holds ((ln(#)tan)`|Z).x = sin.x/cos.x/x+ln.x/(cos.x)^2; :: f.x = ln.x*cot.x theorem :: FDIFF_8:33 Z c= dom (ln(#)cot) implies ln(#)cot is_differentiable_on Z & for x st x in Z holds ((ln(#)cot)`|Z).x = cos.x/sin.x/x-ln.x/(sin.x)^2; :: f.x = 1/x*tan.x theorem :: FDIFF_8:34 not 0 in Z & Z c= dom ((id Z)^(#)tan) implies ((id Z)^(#)tan) is_differentiable_on Z & for x st x in Z holds (((id Z)^(#)tan)`|Z).x = -sin.x/ cos.x/x^2+1/x/(cos.x)^2; :: f.x = 1/x*cot.x theorem :: FDIFF_8:35 not 0 in Z & Z c= dom ((id Z)^(#)cot) implies ((id Z)^(#)cot) is_differentiable_on Z & for x st x in Z holds (((id Z)^(#)cot)`|Z).x = -cos.x/ sin.x/x^2-1/x/(sin.x)^2;