:: Several Differentiation Formulas of Special Functions -- Part {V} :: by Bo Li and Pan Wang :: :: Received September 19, 2007 :: Copyright (c) 2007-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 REAL_1, RCOMP_1, SUBSET_1, NUMBERS, TARSKI, RELAT_1, SIN_COS, FDIFF_1, FUNCT_1, ARYTM_3, SQUARE_1, ARYTM_1, CARD_1, XBOOLE_0, VALUED_1, TAYLOR_1, XXREAL_0, LIMFUNC1, XXREAL_1, SIN_COS4; notations TARSKI, SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, XCMPLX_0, XREAL_0, RELSET_1, PARTFUN1, RCOMP_1, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS, REAL_1, VALUED_1, FDIFF_1, LIMFUNC1, FDIFF_9; constructors REAL_1, PARTFUN1, PARTFUN2, LIMFUNC1, RCOMP_1, TAYLOR_1, SIN_COS, FDIFF_1, RFUNCT_1, SQUARE_1, ARYTM_0, COMSEQ_3, FDIFF_9, VALUED_1, RELSET_1, XREAL_0; registrations RELSET_1, MEMBERED, RCOMP_1, XXREAL_0, VALUED_0, NUMBERS, XREAL_0, SQUARE_1, SIN_COS; requirements SUBSET, NUMERALS, ARITHM; begin reserve x for Real, Z for open Subset of REAL; ::f.x=tan.(cot.x) 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); ::f.x=tan.(tan.x) 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); ::f.x=cot.(cot.x) 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); ::f.x=cot.(tan.x) 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); ::f.x= tan.x - cot.x theorem :: FDIFF_10:5 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; ::f.x= tan.x + cot.x theorem :: FDIFF_10:6 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; ::f.x=sin.(sin.x) 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; ::f.x=sin.(cos.x) 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; ::f.x=cos.(sin.x) 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; ::f.x=cos.(cos.x) 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; :: f.x=cos.x * cot.x 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; :: f.x=sin.x * tan.x 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; :: f.x=sin.x * cot.x 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; :: f.x=cos.x * tan.x 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; :: f.x=sin.x * cos.x 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; :: f.x=ln.x * sin.x 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; :: f.x=ln.x * cos.x 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; :: f.x=ln.x * exp_R.x 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; ::f.x=ln.(ln.x) 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); ::f.x=exp_R.(exp_R.x) 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; ::f.x=sin.(tan.x) 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; ::f.x=sin.(cot.x) 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; ::f.x=cos.(tan.x) 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; ::f.x=cos.(cot.x) 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; ::f.x=sin.x*(tan.x+cot.x) 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); ::f.x=cos.x*(tan.x+cot.x) 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); :: f.x=sin.x*(tan.x-cot.x) 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); :: f.x=cos.x*(tan.x-cot.x) 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); ::f.x=exp_R.x*(tan.x + cot.x) 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); ::f.x=exp_R.x*(tan.x - cot.x) 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); ::f.x=sin.x*(sin.x+cos.x) 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; ::f.x=sin.x*(sin.x-cos.x) 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; :: f.x=cos.x*(sin.x-cos.x) 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; :: f.x=cos.x*(sin.x+cos.x) 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; ::f.x=sin.(tan.x+cot.x) 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); ::f.x=sin.(tan.x-cot.x) 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); ::f.x=cos.(tan.x-cot.x) 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); ::f.x=cos.(tan.x+cot.x) 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); ::f.x=exp_R.(tan.x + cot.x) 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); ::f.x=exp_R.(tan.x - cot.x) 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); ::f.x=(tan.x-cot.x)/exp_.x 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; ::f.x=(tan.x+cot.x)/exp_.x 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; :: f.x = sin.(sec.x) 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; :: f.x = cos.(sec.x) 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; :: f.x = sin.(cosec.x) 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; :: f.x = cos.(cose.x) 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;