:: Some Differentiable Formulas of Special Functions :: by Jianbing Cao , Fahui Zhai and Xiquan Liang :: :: Received November 7, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin Lm1: for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x ) ) proofend; Lm2: for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 - f2) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 holds ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 - f2) `| Z) . x = - (2 * x) ) ) proofend; Lm3: for Z being open Subset of REAL st Z c= dom (#R (1 / 2)) holds ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) proofend; :: 1 f.x=(a+x)/(a-x) theorem :: FDIFF_5:1 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = a + x & f2 . x = a - x & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) ) proofend; :: 2 f.x=(x-a)/(x+a) theorem :: FDIFF_5:2 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x - a & f2 . x = x + a & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) ) proofend; :: 3 f.x=(x-a)/(x-b) theorem :: FDIFF_5:3 for a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x - a & f2 . x = x - b & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) ) proofend; :: 4 f.x=1/x theorem Th4: :: FDIFF_5:4 for Z being open Subset of REAL st not 0 in Z holds ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) proofend; Lm4: for Z being open Subset of REAL st not 0 in Z holds dom (sin * ((id Z) ^)) = Z proofend; theorem Th5: :: FDIFF_5:5 for Z being open Subset of REAL st not 0 in Z holds ( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) ) proofend; :: 6 f.x=cos(1/x) theorem Th6: :: FDIFF_5:6 for Z being open Subset of REAL st not 0 in Z & Z c= dom (cos * ((id Z) ^)) holds ( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) ) proofend; :: 7 f.x=x*sin(1/x) theorem :: FDIFF_5:7 for Z being open Subset of REAL st Z c= dom ((id Z) (#) (sin * ((id Z) ^))) & not 0 in Z holds ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) ) proofend; :: 8 f.x=x*cos(1/x) theorem :: FDIFF_5:8 for Z being open Subset of REAL st Z c= dom ((id Z) (#) (cos * ((id Z) ^))) & not 0 in Z holds ( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) ) proofend; :: 9 f.x=sin(1/x)*cos(1/x) theorem :: FDIFF_5:9 for Z being open Subset of REAL st Z c= dom ((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) & not 0 in Z holds ( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) ) proofend; :: 10 f.x=sin(n*x)*(sin x #Z n) theorem :: FDIFF_5:10 for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) proofend; :: 11 f.x=cos(n*x)*(sin x #Z n) theorem :: FDIFF_5:11 for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) proofend; :: 12 f.x=cos(n*x)*(cos x #Z n) theorem :: FDIFF_5:12 for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) ) proofend; :: 13 f.x=sin(n*x)*(cos x |^ n) theorem :: FDIFF_5:13 for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) proofend; :: 14 f.x=(1/x)*sin x theorem :: FDIFF_5:14 for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) sin) holds ( ((id Z) ^) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) ) proofend; :: 15 f.x=(1/x)*cos x theorem :: FDIFF_5:15 for Z being open Subset of REAL st not 0 in Z & Z c= dom (((id Z) ^) (#) cos) holds ( ((id Z) ^) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) ) proofend; :: 16 f.x=sin.x+x^(1/2) theorem :: FDIFF_5:16 for Z being open Subset of REAL st Z c= dom (sin + (#R (1 / 2))) holds ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) ) proofend; :: 17 f.x=x^2*sin(1/x) theorem :: FDIFF_5:17 for Z being open Subset of REAL for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (sin * ((id Z) ^))) & g = #Z 2 holds ( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) ) proofend; :: 18 f.x=x^2*cos(1/x) theorem :: FDIFF_5:18 for Z being open Subset of REAL for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (cos * ((id Z) ^))) & g = #Z 2 holds ( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) ) proofend; Lm5: for x being Real st x in dom ln holds x > 0 by TAYLOR_1:18, XXREAL_1:4; theorem Th19: :: FDIFF_5:19 for Z being open Subset of REAL st Z c= dom ln holds ( ln is_differentiable_on Z & ( for x being Real st x in Z holds (ln `| Z) . x = 1 / x ) ) proofend; :: 20 f.x=x*ln(x) theorem :: FDIFF_5:20 for Z being open Subset of REAL st Z c= dom ((id Z) (#) ln) holds ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) ) proofend; :: 21 f.x=x^2*ln(x) theorem :: FDIFF_5:21 for Z being open Subset of REAL for g being PartFunc of REAL,REAL st Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds x > 0 ) holds ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) proofend; :: 22 f.x=(a+x^2)/(a-x^2) theorem Th22: :: FDIFF_5:22 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((f1 + f2) / (f1 - f2)) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) holds ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) ) proofend; :: 23 f.x=ln((a+x^2)/(a-x^2)) theorem :: FDIFF_5:23 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds (f1 + f2) . x > 0 ) holds ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) proofend; :: 24 f.x=(1/x)*ln(x) theorem :: FDIFF_5:24 for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) ln) & ( for x being Real st x in Z holds x > 0 ) holds ( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) ) proofend; :: 25 f.x=1/ln(x) theorem :: FDIFF_5:25 for Z being open Subset of REAL st Z c= dom (ln ^) & ( for x being Real st x in Z holds ln . x <> 0 ) holds ( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) ) proofend;