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