:: Several Differentiation Formulas of Special Functions -- Part {III} :: by Bo Li , Yan Zhang and Xiquan Liang :: :: Received March 22, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin theorem Th1: :: FDIFF_7:1 for x being Real holds x #Z 2 = x ^2 proofend; theorem Th2: :: FDIFF_7:2 for x being Real st x > 0 holds x #R (1 / 2) = sqrt x proofend; theorem Th3: :: FDIFF_7:3 for x being Real st x > 0 holds x #R (- (1 / 2)) = 1 / (sqrt x) proofend; Lm1: for x being Real holds 2 * ((cos . (x / 2)) ^2) = 1 + (cos . x) proofend; Lm2: for x being Real holds 2 * ((sin . (x / 2)) ^2) = 1 - (cos . x) proofend; ::f.x=r*arcsinx theorem :: FDIFF_7:4 for r being Real for Z being open Subset of REAL st Z c= ].(- 1),1.[ & Z c= dom (r (#) arcsin) holds ( r (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arcsin) `| Z) . x = r / (sqrt (1 - (x ^2))) ) ) proofend; ::f.x=r*arccosx theorem :: FDIFF_7:5 for r being Real for Z being open Subset of REAL st Z c= ].(- 1),1.[ & Z c= dom (r (#) arccos) holds ( r (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arccos) `| Z) . x = - (r / (sqrt (1 - (x ^2)))) ) ) proofend; theorem Th6: :: FDIFF_7:6 for x being Real for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds ( arcsin * f is_differentiable_in x & diff ((arcsin * f),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) ) proofend; theorem Th7: :: FDIFF_7:7 for x being Real for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds ( arccos * f is_differentiable_in x & diff ((arccos * f),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) ) proofend; ::f.x=ln(arcsin.x) theorem :: FDIFF_7:8 for Z being open Subset of REAL st Z c= dom (ln * arcsin) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arcsin . x > 0 ) holds ( ln * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arcsin) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arcsin . x)) ) ) proofend; ::f.x=ln(arccos.x) theorem :: FDIFF_7:9 for Z being open Subset of REAL st Z c= dom (ln * arccos) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arccos . x > 0 ) holds ( ln * arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arccos) `| Z) . x = - (1 / ((sqrt (1 - (x ^2))) * (arccos . x))) ) ) proofend; ::f.x=(arcsin)|^n theorem Th10: :: FDIFF_7:10 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((#Z n) * arcsin) & Z c= ].(- 1),1.[ holds ( (#Z n) * arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arcsin) `| Z) . x = (n * ((arcsin . x) #Z (n - 1))) / (sqrt (1 - (x ^2))) ) ) proofend; ::f.x=(arccos)|^n theorem Th11: :: FDIFF_7:11 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((#Z n) * arccos) & Z c= ].(- 1),1.[ holds ( (#Z n) * arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arccos) `| Z) . x = - ((n * ((arccos . x) #Z (n - 1))) / (sqrt (1 - (x ^2)))) ) ) proofend; ::f.x=(1/2)*(arcsin)|^2 theorem :: FDIFF_7:12 for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * arcsin)) & Z c= ].(- 1),1.[ holds ( (1 / 2) (#) ((#Z 2) * arcsin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arcsin)) `| Z) . x = (arcsin . x) / (sqrt (1 - (x ^2))) ) ) proofend; ::f.x=(1/2)*(arccos)|^2 theorem :: FDIFF_7:13 for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * arccos)) & Z c= ].(- 1),1.[ holds ( (1 / 2) (#) ((#Z 2) * arccos) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arccos)) `| Z) . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) ) ) proofend; ::f.x=arcsin.(a*x+b) theorem Th14: :: FDIFF_7:14 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (arcsin * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds ( arcsin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arcsin * f) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) ) ) proofend; ::f.x=arccos.(a*x+b) theorem Th15: :: FDIFF_7:15 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (arccos * f) & ( for x being Real st x in Z holds ( f . x = (a * x) + b & f . x > - 1 & f . x < 1 ) ) holds ( arccos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arccos * f) `| Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) ) ) proofend; ::f.x=x*arcsin.x theorem Th16: :: FDIFF_7:16 for Z being open Subset of REAL st Z c= dom ((id Z) (#) arcsin) & Z c= ].(- 1),1.[ holds ( (id Z) (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arcsin) `| Z) . x = (arcsin . x) + (x / (sqrt (1 - (x ^2)))) ) ) proofend; ::f.x=x*arccos.x theorem Th17: :: FDIFF_7:17 for Z being open Subset of REAL st Z c= dom ((id Z) (#) arccos) & Z c= ].(- 1),1.[ holds ( (id Z) (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) arccos) `| Z) . x = (arccos . x) - (x / (sqrt (1 - (x ^2)))) ) ) proofend; ::f.x=(a*x+b)*arcsin.x theorem :: FDIFF_7:18 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) arcsin) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arcsin) `| Z) . x = (a * (arcsin . x)) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) proofend; ::f.x=(a*x+b)*arccos.x theorem :: FDIFF_7:19 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) arccos) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( f (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arccos) `| Z) . x = (a * (arccos . x)) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ) ) proofend; ::f.x=(1/2)*arcsin(2*x) theorem :: FDIFF_7:20 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (arcsin * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds ( (1 / 2) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arcsin * f)) `| Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) ) ) proofend; ::f.x=(1/2)*arccos(2*x) theorem :: FDIFF_7:21 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (arccos * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds ( (1 / 2) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arccos * f)) `| Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) ) ) proofend; ::f.x=(1-x|^2) #R (1/2) theorem Th22: :: FDIFF_7:22 for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * ((1 - (x #Z 2)) #R (- (1 / 2)))) ) ) proofend; ::f.x=x*arcsin.x+(1-x|^2) #R (1/2) theorem :: FDIFF_7:23 for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ) holds ( ((id Z) (#) arcsin) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . x ) ) proofend; ::f.x=x*arccos.x-(1-x|^2) #R (1/2) theorem :: FDIFF_7:24 for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arccos) - ((#R (1 / 2)) * f)) & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 & x <> 0 ) ) holds ( ((id Z) (#) arccos) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . x ) ) proofend; ::f.x=x*arcsin(x/a) theorem Th25: :: FDIFF_7:25 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arcsin * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arcsin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arcsin * f)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) proofend; ::f.x=x*arccos(x/a) theorem Th26: :: FDIFF_7:26 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arccos * f)) & ( for x being Real st x in Z holds ( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arccos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arccos * f)) `| Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ) ) proofend; ::f.x=(a^2-x|^2) #R (1/2) theorem Th27: :: FDIFF_7:27 for a being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = - (x * (((a ^2) - (x #Z 2)) #R (- (1 / 2)))) ) ) proofend; ::f.x=x*arcsin(x/a)+(a^2-x|^2) #R (1/2) theorem :: FDIFF_7:28 for a being Real for Z being open Subset of REAL for f3, f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds ( ((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) `| Z) . x = arcsin . (x / a) ) ) proofend; ::f.x=x*arccos(x/a)-(a^2-x|^2) #R (1/2) theorem :: FDIFF_7:29 for a being Real for Z being open Subset of REAL for f3, f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 & f3 . x = x / a & f3 . x > - 1 & f3 . x < 1 & x <> 0 & a > 0 ) ) holds ( ((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) `| Z) . x = arccos . (x / a) ) ) proofend; ::f.x=-1/(n*(sin.x)|^n) theorem :: FDIFF_7:30 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((- (1 / n)) (#) ((#Z n) * (sin ^))) & n > 0 & ( for x being Real st x in Z holds sin . x <> 0 ) holds ( (- (1 / n)) (#) ((#Z n) * (sin ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (1 / n)) (#) ((#Z n) * (sin ^))) `| Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ) ) proofend; ::f.x=1/(n*(cos.x)|^n) theorem :: FDIFF_7:31 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * (cos ^))) & n > 0 & ( for x being Real st x in Z holds cos . x <> 0 ) holds ( (1 / n) (#) ((#Z n) * (cos ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * (cos ^))) `| Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ) ) proofend; Lm3: right_open_halfline 0 = { g where g is Real : 0 < g } by XXREAL_1:230; ::f.x=sin(ln.x) theorem :: FDIFF_7:32 for Z being open Subset of REAL st Z c= dom (sin * ln) & ( for x being Real st x in Z holds x > 0 ) holds ( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ln) `| Z) . x = (cos . (ln . x)) / x ) ) proofend; ::f.x=cos(ln.x) theorem :: FDIFF_7:33 for Z being open Subset of REAL st Z c= dom (cos * ln) & ( for x being Real st x in Z holds x > 0 ) holds ( cos * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ln) `| Z) . x = - ((sin . (ln . x)) / x) ) ) proofend; ::f.x=sin(exp.x) theorem :: FDIFF_7:34 for Z being open Subset of REAL st Z c= dom (sin * exp_R) holds ( sin * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * exp_R) `| Z) . x = (exp_R . x) * (cos . (exp_R . x)) ) ) proofend; ::f.x=cos(exp_R.x) theorem :: FDIFF_7:35 for Z being open Subset of REAL st Z c= dom (cos * exp_R) holds ( cos * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * exp_R) `| Z) . x = - ((exp_R . x) * (sin . (exp_R . x))) ) ) proofend; ::f.x=exp_R.(cos.x) theorem :: FDIFF_7:36 for Z being open Subset of REAL st Z c= dom (exp_R * cos) holds ( exp_R * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * cos) `| Z) . x = - ((exp_R . (cos . x)) * (sin . x)) ) ) proofend; ::f.x=exp_R.(sin.x) theorem :: FDIFF_7:37 for Z being open Subset of REAL st Z c= dom (exp_R * sin) holds ( exp_R * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * sin) `| Z) . x = (exp_R . (sin . x)) * (cos . x) ) ) proofend; ::f.x=sin.x+cos.x theorem Th38: :: FDIFF_7:38 for Z being open Subset of REAL st Z c= dom (sin + cos) holds ( sin + cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + cos) `| Z) . x = (cos . x) - (sin . x) ) ) proofend; ::f.x=sin.x-cos.x theorem Th39: :: FDIFF_7:39 for Z being open Subset of REAL st Z c= dom (sin - cos) holds ( sin - cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin - cos) `| Z) . x = (cos . x) + (sin . x) ) ) proofend; ::f.x=exp_R.x*(sin.x-cos.x) theorem :: FDIFF_7:40 for Z being open Subset of REAL st Z c= dom (exp_R (#) (sin - cos)) holds ( exp_R (#) (sin - cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin - cos)) `| Z) . x = (2 * (exp_R . x)) * (sin . x) ) ) proofend; ::f.x=exp_R.x*(sin.x+cos.x) theorem :: FDIFF_7:41 for Z being open Subset of REAL st Z c= dom (exp_R (#) (sin + cos)) holds ( exp_R (#) (sin + cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) (sin + cos)) `| Z) . x = (2 * (exp_R . x)) * (cos . x) ) ) proofend; ::f.x=(sin.x+cos.x)/exp_R.x theorem :: FDIFF_7:42 for Z being open Subset of REAL st Z c= dom ((sin + cos) / exp_R) holds ( (sin + cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin + cos) / exp_R) `| Z) . x = - ((2 * (sin . x)) / (exp_R . x)) ) ) proofend; ::f.x=(sin.x-cos.x)/exp_R.x theorem :: FDIFF_7:43 for Z being open Subset of REAL st Z c= dom ((sin - cos) / exp_R) holds ( (sin - cos) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds (((sin - cos) / exp_R) `| Z) . x = (2 * (cos . x)) / (exp_R . x) ) ) proofend; ::f.x=exp_R.x*sin.x theorem :: FDIFF_7:44 for Z being open Subset of REAL st Z c= dom (exp_R (#) sin) holds ( exp_R (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) sin) `| Z) . x = (exp_R . x) * ((sin . x) + (cos . x)) ) ) proofend; ::f.x=exp_R.x*cos.x theorem :: FDIFF_7:45 for Z being open Subset of REAL st Z c= dom (exp_R (#) cos) holds ( exp_R (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) cos) `| Z) . x = (exp_R . x) * ((cos . x) - (sin . x)) ) ) proofend; :: f.x=tan.x theorem Th46: :: FDIFF_7:46 for x being Real st cos . x <> 0 holds ( sin / cos is_differentiable_in x & diff ((sin / cos),x) = 1 / ((cos . x) ^2) ) proofend; ::f.x=cot.x theorem Th47: :: FDIFF_7:47 for x being Real st sin . x <> 0 holds ( cos / sin is_differentiable_in x & diff ((cos / sin),x) = - (1 / ((sin . x) ^2)) ) proofend; ::f.x=(tan.x) #Z 2 theorem :: FDIFF_7:48 for Z being open Subset of REAL st Z c= dom ((#Z 2) * (sin / cos)) & ( for x being Real st x in Z holds cos . x <> 0 ) holds ( (#Z 2) * (sin / cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (sin / cos)) `| Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) ) ) proofend; ::f.x=(cot.x) #Z 2 theorem :: FDIFF_7:49 for Z being open Subset of REAL st Z c= dom ((#Z 2) * (cos / sin)) & ( for x being Real st x in Z holds sin . x <> 0 ) holds ( (#Z 2) * (cos / sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (cos / sin)) `| Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) ) ) proofend; ::f.x=tan.(x/2) theorem :: FDIFF_7:50 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((sin / cos) * f) & ( for x being Real st x in Z holds ( f . x = x / 2 & cos . (f . x) <> 0 ) ) holds ( (sin / cos) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((sin / cos) * f) `| Z) . x = 1 / (1 + (cos . x)) ) ) proofend; ::f.x=cot.(x/2) theorem :: FDIFF_7:51 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((cos / sin) * f) & ( for x being Real st x in Z holds ( f . x = x / 2 & sin . (f . x) <> 0 ) ) holds ( (cos / sin) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) ) ) proofend;