:: Some Differentiable Formulas of Special Functions :: by Jianbing Cao , Fahui Zhai and Xiquan Liang :: :: Received November 7, 2005 :: Copyright (c) 2005-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, SUBSET_1, NUMBERS, RCOMP_1, PARTFUN1, TARSKI, RELAT_1, ARYTM_3, FUNCT_1, PREPOWER, FDIFF_1, XBOOLE_0, CARD_1, ARYTM_1, NEWTON, LIMFUNC1, XXREAL_0, SQUARE_1, ORDINAL4, SIN_COS, VALUED_1, TAYLOR_1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, PARTFUN2, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, RCOMP_1, REAL_1, VALUED_1, FDIFF_1, NEWTON, PREPOWER, TAYLOR_1, LIMFUNC1, SIN_COS, RFUNCT_1, SQUARE_1; constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1, FDIFF_1, PREPOWER, SIN_COS, TAYLOR_1, VALUED_1, LIMFUNC1, XXREAL_2, RELSET_1, NEWTON; registrations RELSET_1, NUMBERS, INT_1, MEMBERED, RCOMP_1, VALUED_0, XXREAL_0, XREAL_0, PREPOWER, NEWTON, SQUARE_1; requirements SUBSET, NUMERALS, ARITHM, BOOLE; begin reserve y for set, x,a,b for Real, n for Element of NAT, Z for open Subset of REAL, f,f1,f2,g for PartFunc of REAL,REAL; :: 1 f.x=(a+x)/(a-x) theorem :: FDIFF_5:1 Z c= dom (f1/f2) & (for x st x in Z holds f1.x=a+x & f2.x=a-x & f2.x<> 0) implies (f1/f2) is_differentiable_on Z & for x st x in Z holds ((f1/f2)`|Z). x = (2*a)/(a-x)^2; :: 2 f.x=(x-a)/(x+a) theorem :: FDIFF_5:2 Z c= dom (f1/f2) & (for x st x in Z holds f1.x=x-a & f2.x=x+a & f2.x<> 0) implies (f1/f2) is_differentiable_on Z & for x st x in Z holds ((f1/f2)`|Z). x = (2*a)/(x+a)^2; :: 3 f.x=(x-a)/(x-b) theorem :: FDIFF_5:3 Z c= dom (f1/f2) & (for x st x in Z holds f1.x=x-a & f2.x=x-b & f2.x<> 0) implies (f1/f2) is_differentiable_on Z & for x st x in Z holds ((f1/f2)`|Z). x = (a-b)/(x-b)^2; :: 4 f.x=1/x theorem :: FDIFF_5:4 not 0 in Z implies (id Z)^ is_differentiable_on Z & for x st x in Z holds (((id Z)^)`|Z).x= -1/x^2; theorem :: FDIFF_5:5 not 0 in Z implies sin*((id Z)^) is_differentiable_on Z & for x st x in Z holds ((sin*((id Z)^))`|Z).x = -(1/x^2)*cos.(1/x); :: 6 f.x=cos(1/x) theorem :: FDIFF_5:6 not 0 in Z & Z c= dom (cos*((id Z)^)) implies cos*((id Z)^) is_differentiable_on Z & for x st x in Z holds ((cos*((id Z)^))`|Z).x = 1/x^2* sin.(1/x); :: 7 f.x=x*sin(1/x) theorem :: FDIFF_5:7 Z c= dom ((id Z)(#)(sin*((id Z)^))) & not 0 in Z implies (id Z)(#)(sin *((id Z)^)) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(sin*((id Z)^)))`|Z).x = sin.(1/x)-(1/x)*cos.(1/x); :: 8 f.x=x*cos(1/x) theorem :: FDIFF_5:8 Z c= dom ((id Z)(#)(cos*((id Z)^))) & not 0 in Z implies (id Z)(#)(cos *((id Z)^)) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(cos*((id Z)^)))`|Z).x = cos.(1/x)+(1/x)*sin.(1/x); :: 9 f.x=sin(1/x)*cos(1/x) theorem :: FDIFF_5:9 Z c= dom ((sin*((id Z)^))(#)(cos*((id Z)^))) & not 0 in Z implies (sin *((id Z)^))(#)(cos*((id Z)^)) is_differentiable_on Z & for x st x in Z holds (( (sin*((id Z)^))(#)(cos*((id Z)^)))`|Z).x = (1/x^2)*((sin.(1/x))^2-(cos.(1/x))^2 ); :: 10 f.x=sin(n*x)*(sin x ^ n) theorem :: FDIFF_5:10 Z c= dom ((sin*f)(#)(( #Z n)*sin)) & n>=1 & (for x st x in Z holds f.x =n*x) implies (sin*f)(#)(( #Z n)*sin) is_differentiable_on Z & for x st x in Z holds (((sin*f)(#)(( #Z n)*sin))`|Z).x =n*(sin.x) #Z (n-1)*sin.((n+1)*x); :: 11 f.x=cos(n*x)*(sin x ^ n) theorem :: FDIFF_5:11 Z c= dom ((cos*f)(#)(( #Z n)*sin)) & n>=1 & (for x st x in Z holds f.x =n*x) implies (cos*f)(#)(( #Z n)*sin) is_differentiable_on Z & for x st x in Z holds (((cos*f)(#)(( #Z n)*sin))`|Z).x =n*(sin.x) #Z (n-1) * cos.((n+1)*x); :: 12 f.x=cos(n*x)*(cos x ^ n) theorem :: FDIFF_5:12 Z c= dom ((cos*f)(#)(( #Z n)*cos)) & n>=1 & (for x st x in Z holds f.x =n*x) implies (cos*f)(#)(( #Z n)*cos) is_differentiable_on Z & for x st x in Z holds (((cos*f)(#)(( #Z n)*cos))`|Z).x =-n*(cos.x) #Z (n-1) *sin.((n+1)*x); :: 13 f.x=sin(n*x)*(cos x ^ n) theorem :: FDIFF_5:13 Z c= dom ((sin*f)(#)(( #Z n)*cos)) & n>=1 & (for x st x in Z holds f.x =n*x) implies (sin*f)(#)(( #Z n)*cos) is_differentiable_on Z & for x st x in Z holds (((sin*f)(#)(( #Z n)*cos))`|Z).x =n*(cos.x) #Z (n-1) *cos.((n+1)*x); :: 14 f.x=(1/x)*sin x theorem :: FDIFF_5:14 not 0 in Z & Z c= dom (((id Z)^)(#)sin) implies ((id Z)^)(#)sin is_differentiable_on Z & for x st x in Z holds ((((id Z)^)(#)sin)`|Z).x =(1/x)* cos.x-(1/x^2)*sin.x; :: 15 f.x=(1/x)*cos x theorem :: FDIFF_5:15 not 0 in Z & Z c= dom (((id Z)^)(#)cos) implies ((id Z)^)(#)cos is_differentiable_on Z & for x st x in Z holds ((((id Z)^)(#)cos)`|Z).x =-(1/x) *sin.x-(1/x^2)*cos.x; :: 16 f.x=sin.x+x^(1/2) theorem :: FDIFF_5:16 Z c= dom (sin+( #R (1/2))) implies sin+( #R (1/2)) is_differentiable_on Z & for x st x in Z holds ((sin+( #R (1/2)))`|Z).x =cos.x+ (1/2)* x #R (-1/2); :: 17 f.x=x^2*sin(1/x) theorem :: FDIFF_5:17 not 0 in Z & Z c= dom (g(#)(sin*((id Z)^))) & g=#Z 2 implies g(#)(sin* ((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((g(#)(sin*((id Z)^)) )`|Z).x = 2*x*sin.(1/x)-cos.(1/x); :: 18 f.x=x^2*cos(1/x) theorem :: FDIFF_5:18 not 0 in Z & Z c= dom (g(#)(cos*((id Z)^))) & g=#Z 2 implies g(#)(cos* ((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((g(#)(cos*((id Z)^)) )`|Z).x = 2*x*cos.(1/x)+sin.(1/x); theorem :: FDIFF_5:19 Z c= dom ln implies ln is_differentiable_on Z & for x st x in Z holds (ln`|Z).x = 1/x; :: 20 f.x=x*ln(x) theorem :: FDIFF_5:20 Z c= dom ((id Z)(#)ln) implies (id Z)(#)ln is_differentiable_on Z & for x st x in Z holds (((id Z)(#)ln)`|Z).x = 1+ln.x; :: 21 f.x=x^2*ln(x) theorem :: FDIFF_5:21 Z c= dom (g(#)ln) & g=#Z 2 & (for x st x in Z holds x>0) implies g(#) ln is_differentiable_on Z & for x st x in Z holds ((g(#)ln)`|Z).x = x+2*x*ln.x; :: 22 f.x=(a+x^2)/(a-x^2) theorem :: FDIFF_5:22 Z c= dom ((f1+f2)/(f1-f2)) & (for x st x in Z holds f1.x=a) & f2 =#Z 2 & (for x st x in Z holds (f1-f2).x>0) implies (f1+f2)/(f1-f2) is_differentiable_on Z & for x st x in Z holds (((f1+f2)/(f1-f2))`|Z).x = (4*a* x)/(a-x|^2)|^2; :: 23 f.x=ln((a+x^2)/(a-x^2)) theorem :: FDIFF_5:23 Z c= dom (ln*((f1+f2)/(f1-f2))) & (for x st x in Z holds f1.x=a) & f2= #Z 2 & (for x st x in Z holds (f1-f2).x>0) & (for x st x in Z holds (f1+f2).x>0 ) implies ln*((f1+f2)/(f1-f2)) is_differentiable_on Z & for x st x in Z holds ( (ln*((f1+f2)/(f1-f2)))`|Z).x = (4*a*x)/(a|^2-x|^4); :: 24 f.x=(1/x)*ln(x) theorem :: FDIFF_5:24 Z c= dom (((id Z)^)(#)ln) & (for x st x in Z holds x >0) implies ((id Z)^)(#)ln is_differentiable_on Z & for x st x in Z holds ((((id Z)^)(#)ln)`|Z). x = (1/x^2)*(1-ln.x); :: 25 f.x=1/ln(x) theorem :: FDIFF_5:25 Z c= dom (ln^) & (for x st x in Z holds ln.x<>0) implies (ln^) is_differentiable_on Z & for x st x in Z holds ((ln^)`|Z).x =-1/(x*(ln.x)^2);