:: Several Differentiable Formulas of Special Functions -- Part {II} :: by Yan Zhang , Bo Li and Xiquan Liang :: :: Received November 23, 2005 :: Copyright (c) 2005-2016 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, ARYTM_1, SIN_COS, RELAT_1, SQUARE_1, ARYTM_3, FUNCT_1, XXREAL_0, CARD_1, PREPOWER, POWER, TARSKI, FDIFF_1, VALUED_1, NEWTON, XBOOLE_0, TAYLOR_1, ORDINAL4, COMPLEX1, LIMFUNC1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, LIMFUNC1, RCOMP_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, VALUED_1, FDIFF_1, NEWTON, INT_2, PREPOWER, POWER, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1; constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1, LIMFUNC1, FDIFF_1, PREPOWER, POWER, SIN_COS, TAYLOR_1, VALUED_1, RELSET_1, NEWTON; registrations ORDINAL1, RELSET_1, XXREAL_0, INT_1, MEMBERED, RCOMP_1, VALUED_0, XREAL_0, NEWTON, SIN_COS, SQUARE_1, PREPOWER; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin reserve y for set, x,a for Real, n for Element of NAT, Z for open Subset of REAL, f,f1,f2 for PartFunc of REAL,REAL; :: a #R x=exp.(x*ln a) theorem :: FDIFF_6:1 a>0 implies exp_R.(x*log(number_e,a))=a #R x; :: 15 a #R (-x)=exp.(-x*ln a) theorem :: FDIFF_6:2 a>0 implies exp_R.(-x*log(number_e,a))=a #R (-x); :: 1 f.x=a^2-x^2 theorem :: FDIFF_6:3 Z c= dom (f1-f2) & (for x st x in Z holds f1.x=a^2) & f2=#Z 2 implies f1-f2 is_differentiable_on Z & for x st x in Z holds ((f1-f2)`|Z).x = - 2*x; :: 2 f.x=(a^2+x^2)/(a^2-x^2) theorem :: FDIFF_6:4 Z c= dom ((f1+f2)/(f1-f2)) & f2=#Z 2 & (for x st x in Z holds f1. x=a^2 & (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^2*x/(a^2-x|^2)^2; :: 3 f.x=ln((a^2+x^2)/(a^2-x^2)) theorem :: FDIFF_6:5 Z c= dom f & f=ln*((f1+f2)/(f1-f2)) & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & (f1-f2).x>0 & a<>0) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =4*a^2*x/(a|^4-x|^4); :: 4 f.x=(1/(4*a^2))*ln((a^2+x^2)/(a^2-x^2)) theorem :: FDIFF_6:6 Z c= dom ((1/(4*a^2))(#)f) & f=ln*((f1+f2)/(f1-f2)) & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & (f1-f2).x>0 & a<>0) implies (1/(4*a^2))(#)f is_differentiable_on Z & for x st x in Z holds (((1/(4*a^2))(#)f)`|Z).x =x/(a|^ 4-x|^4); :: 5 f.x=x^2/(1+x^2) theorem :: FDIFF_6:7 Z c= dom (f1/(f2+f1)) & f1=#Z 2 & (for x st x in Z holds f2.x=1 & x<>0) implies f1/(f2+f1) is_differentiable_on Z & for x st x in Z holds ((f1/( f2+f1))`|Z).x =2*x/(1+x^2)^2; :: 6 f.x=(1/2)*ln(x^2/(1+x^2)) theorem :: FDIFF_6:8 Z c= dom ((1/2)(#)f) & f=ln*(f1/(f2+f1)) & f1=#Z 2 & (for x st x in Z holds f2.x=1 & x<>0) implies (1/2)(#)f is_differentiable_on Z & for x st x in Z holds (((1/2)(#)f)`|Z).x =1/(x*(1+x^2)); :: 7 f.x=ln(x|^n) theorem :: FDIFF_6:9 Z c= dom (ln*( #Z n)) & (for x st x in Z holds x>0) implies ln*( #Z n) is_differentiable_on Z & for x st x in Z holds ((ln*( #Z n))`|Z).x =n/x; :: 8 f.x=1/x+ln((x-1)/x) theorem :: FDIFF_6:10 Z c= dom (f2^+ln*(f1/f2)) & (for x st x in Z holds f2.x = x & f2.x>0 & f1.x=x-1 & f1.x >0 ) implies f2^+ln*(f1/f2) is_differentiable_on Z & for x st x in Z holds ( (f2^+ln*(f1/f2))`|Z).x= 1/(x^2*(x-1)); :: 10 f.x=a #R x=exp.(x*ln a) theorem :: FDIFF_6:11 Z c= dom (exp_R*f) & (for x st x in Z holds f.x=x*log(number_e,a )) & a>0 implies exp_R*f is_differentiable_on Z & for x st x in Z holds ((exp_R *f)`|Z).x =a #R x*log(number_e,a); :: 11 f.x=(a #R x)*(x-1/ln a)/ln a theorem :: FDIFF_6:12 Z c= dom ((1/log(number_e,a))(#)((exp_R*f1)(#)f2)) & (for x st x in Z holds f1.x=x*log(number_e,a) & f2.x=x-1/log(number_e,a)) & a>0 & a<>1 implies ( 1/log(number_e,a))(#)((exp_R*f1)(#)f2) is_differentiable_on Z & for x st x in Z holds (((1/log(number_e,a))(#)((exp_R*f1)(#)f2))`|Z).x =x * a #R x; :: 12 f.x=a #R x*exp(x)/(1+ln a) theorem :: FDIFF_6:13 Z c= dom ((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R)) & (for x st x in Z holds f.x=x*log(number_e,a)) & a>0 & a<>1/number_e implies (1/(1+log( number_e,a)))(#)((exp_R*f)(#)exp_R) is_differentiable_on Z & for x st x in Z holds (((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R))`|Z).x =a #R x*exp_R.x; :: 13 f.x=exp_R(-x) theorem :: FDIFF_6:14 Z c= dom (exp_R*f) & (for x st x in Z holds f.x=-x) implies exp_R*f is_differentiable_on Z & for x st x in Z holds ((exp_R*f)`|Z).x = - exp_R(-x); :: 14 f.x=-(x+1)*exp_R(-x) theorem :: FDIFF_6:15 Z c= dom (f1(#)(exp_R*f2)) & (for x st x in Z holds f1.x=-x-1 & f2.x=- x) implies f1(#)(exp_R*f2) is_differentiable_on Z & for x st x in Z holds ((f1 (#)(exp_R*f2))`|Z).x = x/exp_R(x); :: 16 f.x=a #R (-x)=exp_R.(-x*ln a) theorem :: FDIFF_6:16 Z c= dom -(exp_R*f) & (for x st x in Z holds f.x=-x*log(number_e ,a)) & a>0 implies -(exp_R*f) is_differentiable_on Z & for x st x in Z holds (( -(exp_R*f))`|Z).x =a #R (-x)*log(number_e,a); :: 17 f.x=-(a #R -x)*(x+1/ln a)/ln a theorem :: FDIFF_6:17 Z c= dom ((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2)) & (for x st x in Z holds f1.x=-x*log(number_e,a) & f2.x=x+1/log(number_e,a)) & a>0 & a<>1 implies (1/log(number_e,a))(#)((-(exp_R*f1))(#)f2) is_differentiable_on Z & for x st x in Z holds (((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2))`|Z).x =x /a #R x; :: 18 f.x=(1/(ln a-1))*a #R x/exp_R(x) theorem :: FDIFF_6:18 Z c= dom ((1/(log(number_e,a)-1))(#)((exp_R*f)/exp_R)) & (for x st x in Z holds f.x=x*log(number_e,a)) & a>0 & a<>number_e implies (1/(log(number_e, a)-1))(#)((exp_R*f)/exp_R) is_differentiable_on Z & for x st x in Z holds (((1/ (log(number_e,a)-1))(#)((exp_R*f)/exp_R))`|Z).x =a #R x/exp_R.x; :: 19 f.x=(1/(1-ln a))*exp_R(x)/a #R x theorem :: FDIFF_6:19 Z c= dom ((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f))) & (for x st x in Z holds f.x=x*log(number_e,a)) & a>0 & a<>number_e implies (1/(1-log( number_e,a)))(#)(exp_R/(exp_R*f)) is_differentiable_on Z & for x st x in Z holds (((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f)))`|Z).x =exp_R.x/a #R x; :: 20 f.x=ln(exp_R.x+1) theorem :: FDIFF_6:20 Z c= dom (ln*(exp_R+f)) & (for x st x in Z holds f.x=1 ) implies ln*( exp_R+f) is_differentiable_on Z & for x st x in Z holds ((ln*(exp_R+f))`|Z).x = exp_R.x/(exp_R.x+1); :: 21 f.x=ln(exp_R.x-1) theorem :: FDIFF_6:21 Z c= dom (ln*(exp_R-f)) & (for x st x in Z holds f.x=1 & (exp_R-f).x>0 ) implies ln*(exp_R-f) is_differentiable_on Z & for x st x in Z holds ((ln*( exp_R-f))`|Z).x = exp_R.x/(exp_R.x-1); :: 22 f.x=-ln(1-exp_R.x) theorem :: FDIFF_6:22 Z c= dom -(ln*(f-exp_R)) & (for x st x in Z holds f.x=1 & (f-exp_R).x> 0) implies -(ln*(f-exp_R)) is_differentiable_on Z & for x st x in Z holds ( (- ln*(f-exp_R)) `|Z).x = exp_R.x/(1-exp_R.x); :: 23 f.x=exp_R(2*x)+1 theorem :: FDIFF_6:23 Z c= dom ((( #Z 2)*exp_R)+f) & (for x st x in Z holds f.x=1) implies (( #Z 2)*exp_R)+f is_differentiable_on Z & for x st x in Z holds (((( #Z 2)*exp_R)+f)`|Z).x =2*exp_R(2*x); :: 24 f.x=(1/2)*ln(exp_R(2*x)+1) theorem :: FDIFF_6:24 Z c= dom ((1/2)(#)(ln*f)) & f=(( #Z 2)*exp_R)+f1 & (for x st x in Z holds f1.x=1) implies (1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)+exp_R(-x)); :: 25 f.x=exp_R(2*x)-1 theorem :: FDIFF_6:25 Z c= dom ((( #Z 2)*exp_R)-f) & (for x st x in Z holds f.x=1) implies (( #Z 2)*exp_R)-f is_differentiable_on Z & for x st x in Z holds (((( #Z 2)*exp_R)-f)`|Z).x =2*exp_R(2*x); :: 26 f.x=(1/2)*ln(exp_R(2*x)-1) theorem :: FDIFF_6:26 Z c= dom ((1/2)(#)(ln*f)) & f=(( #Z 2)*exp_R)-f1 & (for x st x in Z holds f1.x=1 & f.x>0) implies (1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)-exp_R(-x)); :: 27 f.x=(exp_R.x-1)^2 theorem :: FDIFF_6:27 Z c= dom (( #Z 2)*(exp_R-f)) & (for x st x in Z holds f.x=1) implies ( #Z 2)*(exp_R-f) is_differentiable_on Z & for x st x in Z holds ((( #Z 2)*(exp_R-f))`|Z).x =2*exp_R.x*(exp_R.x-1); :: 28 f.x=ln((exp_R.x-1)^2/exp_R.x) theorem :: FDIFF_6:28 Z c= dom f & f=ln*((( #Z 2)*(exp_R-f1))/exp_R) & (for x st x in Z holds f1.x=1 & (exp_R-f1).x>0) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =(exp_R.x+1)/(exp_R.x-1); :: 29 f.x=(exp_R.x+1)^2 theorem :: FDIFF_6:29 Z c= dom (( #Z 2)*(exp_R+f)) & (for x st x in Z holds f.x=1) implies ( #Z 2)*(exp_R+f) is_differentiable_on Z & for x st x in Z holds ((( #Z 2)*(exp_R+f))`|Z).x =2*exp_R.x*(exp_R.x+1); :: 30 f.x=ln((exp_R.x+1)^2/exp_R.x) theorem :: FDIFF_6:30 Z c= dom f & f=ln*((( #Z 2)*(exp_R+f1))/exp_R) & (for x st x in Z holds f1.x=1) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =(exp_R.x-1)/(exp_R.x+1); :: 31 f.x=(1-exp_R.x)^2 theorem :: FDIFF_6:31 Z c= dom (( #Z 2)*(f-exp_R)) & (for x st x in Z holds f.x=1) implies ( #Z 2)*(f-exp_R) is_differentiable_on Z & for x st x in Z holds ((( #Z 2)*(f-exp_R))`|Z).x =-2*exp_R.x*(1-exp_R.x); :: 32 f.x=ln(exp_R.x/(1-exp_R.x)^2) theorem :: FDIFF_6:32 Z c= dom f & f=ln*(exp_R/(( #Z 2)*(f1-exp_R))) & (for x st x in Z holds f1.x=1 & (f1-exp_R).x>0) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =(1+exp_R.x)/(1-exp_R.x); :: 33 f.x=ln(exp_R.x/(1+exp_R.x)^2) theorem :: FDIFF_6:33 Z c= dom f & f=ln*(exp_R/(( #Z 2)*(f1+exp_R))) & (for x st x in Z holds f1.x=1) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =(1-exp_R.x)/(1+exp_R.x); :: 34 f.x=ln(exp_R(x)+exp_R(-x)) theorem :: FDIFF_6:34 Z c= dom (ln*f) & f=exp_R+(exp_R*f1) & (for x st x in Z holds f1.x=-x) implies ln*f is_differentiable_on Z & for x st x in Z holds ((ln*f)`|Z).x =( exp_R(x)-exp_R(-x))/(exp_R(x)+exp_R(-x)); :: 35 f.x=ln(exp_R(x)-exp_R(-x)) theorem :: FDIFF_6:35 Z c= dom (ln*f) & f=exp_R-(exp_R*f1) & (for x st x in Z holds f1.x=-x & f.x>0) implies ln*f is_differentiable_on Z & for x st x in Z holds ((ln*f)`|Z ).x=(exp_R(x)+exp_R(-x))/ (exp_R(x)-exp_R(-x)); :: 36 f.x=(2/3)*((1+exp_R.x) #R (3/2)) theorem :: FDIFF_6:36 Z c= dom ((2/3)(#)(( #R (3/2))*(f+exp_R))) & (for x st x in Z holds f. x=1) implies (2/3)(#)(( #R (3/2))*(f+exp_R)) is_differentiable_on Z & for x st x in Z holds (((2/3)(#)(( #R (3/2))*(f+exp_R)))`|Z).x =exp_R.x*(1+exp_R.x) #R ( 1/2); :: 37 f.x=(2/(3*lna))*((1+a |^x) #R (3/2)) theorem :: FDIFF_6:37 Z c= dom ((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1)))) & ( for x st x in Z holds f.x=1 & f1.x=x*log(number_e,a)) & a>0 & a<>1 implies (2/( 3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1))) is_differentiable_on Z & for x st x in Z holds (((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1))))`|Z) .x =a #R x * (1+a #R x) #R (1/2); :: 38 f.x=(-1/2)*cos(2*x) theorem :: FDIFF_6:38 Z c= dom ((-1/2)(#)(cos*f)) & (for x st x in Z holds f.x=2*x) implies (-1/2)(#)(cos*f) is_differentiable_on Z & for x st x in Z holds (((-1/2)(#)(cos *f))`|Z).x =sin(2*x); theorem :: FDIFF_6:39 Z c= dom (2(#)(( #R (1/2))*(f-cos))) & (for x st x in Z holds f.x=1 & sin.x>0 & cos.x<1 & cos.x>-1) implies 2(#)(( #R (1/2))*(f-cos)) is_differentiable_on Z & for x st x in Z holds ((2(#)(( #R (1/2))*(f-cos)))`|Z) .x =(1+cos.x) #R (1/2); theorem :: FDIFF_6:40 Z c= dom ((-2)(#)(( #R (1/2))*(f+cos))) & (for x st x in Z holds f.x=1 & sin.x>0 & cos.x<1 & cos.x>-1) implies (-2)(#)(( #R (1/2))*(f+cos)) is_differentiable_on Z & for x st x in Z holds (((-2)(#)(( #R (1/2))*(f+cos))) `|Z).x =(1-cos.x) #R (1/2); theorem :: FDIFF_6:41 Z c= dom ((1/2)(#)(ln*f)) & f=f1+2(#)sin & (for x st x in Z holds f1.x =1 & f.x >0) implies (1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =cos.x/(1+2*sin.x); theorem :: FDIFF_6:42 Z c= dom ((-1/2)(#)(ln*f)) & f=f1+2(#)cos & (for x st x in Z holds f1. x=1 & f.x >0) implies (-1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z holds (((-1/2)(#)(ln*f))`|Z).x =sin.x/(1+2*cos.x); :: 43 f.x=1/(4*a)*sin(2*a*x) theorem :: FDIFF_6:43 Z c= dom ((1/(4*a))(#)(sin*f)) & (for x st x in Z holds f.x=2*a* x) & a<>0 implies (1/(4*a))(#)(sin*f) is_differentiable_on Z & for x st x in Z holds (((1/(4*a))(#)(sin*f))`|Z).x =1/2 * cos(2*a*x); :: 44 f.x=x/2-1/(4*a)*sin(2*a*x) theorem :: FDIFF_6:44 Z c= dom (f1-((1/(4*a))(#)(sin*f))) & (for x st x in Z holds f1.x=x/2 & f.x=2*a*x) & a<>0 implies f1-((1/(4*a))(#)(sin*f)) is_differentiable_on Z & for x st x in Z holds ((f1-((1/(4*a))(#)(sin*f)))`|Z).x =(sin(a*x))^2; :: 45 f.x=x/2+1/(4*a)*sin(2*a*x) theorem :: FDIFF_6:45 Z c= dom (f1+((1/(4*a))(#)(sin*f))) & (for x st x in Z holds f1.x=x/2 & f.x=2*a*x) & a<>0 implies f1+((1/(4*a))(#)(sin*f)) is_differentiable_on Z & for x st x in Z holds ((f1+((1/(4*a))(#)(sin*f)))`|Z).x =(cos(a*x))^2; :: 46 f.x=(1/n)*(cos.x #Z n) theorem :: FDIFF_6:46 Z c= dom ((1/n)(#)(( #Z n)*cos)) & n>0 implies (1/n)(#)(( #Z n)* cos) is_differentiable_on Z & for x st x in Z holds (((1/n)(#)(( #Z n)*cos))`|Z ).x =-(cos.x) #Z (n-1)*sin.x; :: 47 f.x=(1/3)*(cos.x #Z 3)-cos.x theorem :: FDIFF_6:47 Z c= dom (((1/3)(#)(( #Z 3)*cos))-cos) implies (1/3)(#)(( #Z 3)*cos)- cos is_differentiable_on Z & for x st x in Z holds ((((1/3)(#)(( #Z 3)*cos))- cos)`|Z).x =(sin.x)|^3; :: 48 f.x=sin.x-(1/3)*(sin.x #Z 3) theorem :: FDIFF_6:48 Z c= dom (sin-((1/3)(#)(( #Z 3)*sin))) implies sin-((1/3)(#)(( #Z 3)* sin)) is_differentiable_on Z & for x st x in Z holds ((sin-((1/3)(#)(( #Z 3)* sin)))`|Z).x =(cos.x)|^3; :: 49 f.x=sin(ln x) theorem :: FDIFF_6:49 Z c= dom (sin*ln) implies sin*ln is_differentiable_on Z & for x st x in Z holds ((sin*ln)`|Z).x =cos.(log(number_e,x))/x; :: 50 f.x=-cos(ln x) theorem :: FDIFF_6:50 Z c= dom (-(cos*ln)) implies -(cos*ln) is_differentiable_on Z & for x st x in Z holds ((-(cos*ln))`|Z).x =sin.(log(number_e,x))/x;