:: Several Differentiable Formulas of Special Functions :: by Yan Zhang and Xiquan Liang :: :: Received July 6, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin :: 1 f.x=ln(a+x) theorem Th1: :: FDIFF_4:1 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (a + x) ) ) proofend; :: 2 f.x=ln(x-a) theorem Th2: :: FDIFF_4:2 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = x - a & f . x > 0 ) ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (x - a) ) ) proofend; :: 3 f.x=-ln(a-x) theorem :: FDIFF_4:3 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) proofend; :: 4 f.x=x-a*ln(a+x) theorem :: FDIFF_4:4 for a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - (a (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) holds ( (id Z) - (a (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) ) proofend; :: 5 f.x=(2*a)*ln(a+x)-x theorem :: FDIFF_4:5 for a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom (((2 * a) (#) f) - (id Z)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) holds ( ((2 * a) (#) f) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) ) proofend; :: 6 f.x=x-(2*a)*ln(x+a) theorem :: FDIFF_4:6 for a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) holds ( (id Z) - ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) ) proofend; :: 7 f.x=x + (2*a)*ln(x-a) theorem :: FDIFF_4:7 for a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) holds ( (id Z) + ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) ) proofend; :: 8 f.x=x+ (a-b)*ln(x+b) theorem :: FDIFF_4:8 for a, b being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a - b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) holds ( (id Z) + ((a - b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) ) proofend; :: 9 f.x=x+ (a+b)*ln(x-b) theorem :: FDIFF_4:9 for a, b being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) holds ( (id Z) + ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) ) proofend; :: 10 f.x=x- (a+b)*ln(x+b) theorem :: FDIFF_4:10 for a, b being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) holds ( (id Z) - ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) ) proofend; :: 11 f.x=x+ (b-a)*ln(x-b) theorem :: FDIFF_4:11 for b, a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((b - a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) holds ( (id Z) + ((b - a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ) ) proofend; :: 12 f.x=a+b*x+c*x^|2 theorem Th12: :: FDIFF_4:12 for c, a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + (c (#) f2)) & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) & f2 = #Z 2 holds ( f1 + (c (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ) ) proofend; :: 13 f.x=ln(a+b*x+c*x |^2) theorem Th13: :: FDIFF_4:13 for c, a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a + (b * x) & (f1 + (c (#) f2)) . x > 0 ) ) holds ( ln * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) ) proofend; :: 14 f.x=1/(a+x) theorem Th14: :: FDIFF_4:14 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) holds ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) ) proofend; :: 15 f.x=-1/(a+x) theorem :: FDIFF_4:15 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- 1) (#) (f ^)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) holds ( (- 1) (#) (f ^) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) ) proofend; :: 16 f.x=1/(a-x) theorem :: FDIFF_4:16 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds ( f . x = a - x & f . x <> 0 ) ) holds ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = 1 / ((a - x) ^2) ) ) proofend; :: 17 f.x=a^2+x^|2 theorem Th17: :: FDIFF_4:17 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 ^2 ) & 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; :: 18 f.x=ln(a^2+x|^2) theorem :: FDIFF_4:18 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)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 + f2) . x > 0 ) ) holds ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ) ) proofend; :: 19 f.x=-ln(a^2-x|^2) theorem :: FDIFF_4:19 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))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 - f2) . x > 0 ) ) holds ( - (ln * (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ) ) proofend; :: 20 f.x=a+x|^3 theorem Th20: :: FDIFF_4:20 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 3 holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) ) proofend; :: 21 f.x=ln(a+x|^3) theorem :: FDIFF_4:21 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)) & f2 = #Z 3 & ( for x being Real st x in Z holds ( f1 . x = a & (f1 + f2) . x > 0 ) ) holds ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) ) proofend; :: 22 f.x=ln((a+x)/(a-x)) theorem :: FDIFF_4:22 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)) & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 & f2 . x = a - x & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) ) ) proofend; :: 23 f.x=ln((x-a)/(x+a)) theorem :: FDIFF_4: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)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x + a & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) ) ) proofend; :: 24 f.x=ln((x-a)/(x-b)) theorem Th24: :: FDIFF_4:24 for a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) ) proofend; :: 25 f.x=(1/(a-b))*ln((x-a)/(x-b)) theorem :: FDIFF_4:25 for a, b being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (a - b)) (#) f) & f = ln * (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 & a - b <> 0 ) ) holds ( (1 / (a - b)) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) ) proofend; :: 26 f.x=ln((x-a)/x|^2) theorem :: FDIFF_4:26 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)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) ) proofend; :: irrational function :: 27 f.x=(a+x) #R (3/2) theorem Th27: :: FDIFF_4:27 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((#R (3 / 2)) * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( (#R (3 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) ) proofend; :: 28 f.x=(a+x) #R (2/3) theorem :: FDIFF_4:28 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) ) proofend; :: 29 f.x=(-2/3)*(a+x) #R (2/3) theorem :: FDIFF_4:29 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) ) proofend; :: 30 f.x=2*(a+x) #R (1/2) theorem :: FDIFF_4:30 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) ) proofend; :: 31 f.x=(-2)*(a-x)#R (1/2) theorem :: FDIFF_4:31 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- 2) (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) ) proofend; :: 32 f.x=(2/(3*b))*((a+b*x) #R (3/2)) theorem :: FDIFF_4:32 for b, a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + (b * x) & b <> 0 & f . x > 0 ) ) holds ( (2 / (3 * b)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ) ) proofend; :: 33 f.x=(-2/(3*b))*((a-b*x) #R (3/2)) theorem :: FDIFF_4:33 for b, a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - (b * x) & b <> 0 & f . x > 0 ) ) holds ( (- (2 / (3 * b))) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ) ) proofend; :: 34 f.x=(a^2+x|^2) #R (1/2) theorem :: FDIFF_4:34 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 |^ 2)) #R (- (1 / 2))) ) ) proofend; :: 35 f.x=-(a^2-x|^2) #R (1/2) theorem :: FDIFF_4:35 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 |^ 2)) #R (- (1 / 2))) ) ) proofend; :: 36 f.x=(x+x|^2) #R (1/2) theorem :: FDIFF_4:36 for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = x & f . x > 0 ) ) holds ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ) ) proofend; :: trigonometric functions :: 37 f.x=sin(a*x+b) theorem :: FDIFF_4:37 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (sin * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( sin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) ) proofend; :: 38 f.x=sin(a*x+b) theorem :: FDIFF_4:38 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (cos * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( cos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) ) proofend; :: 39 f.x=1/cos.x theorem :: FDIFF_4:39 for Z being open Subset of REAL st ( for x being Real st x in Z holds cos . x <> 0 ) holds ( cos ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) ) ) proofend; :: 40 f.x=1/sin.x theorem :: FDIFF_4:40 for Z being open Subset of REAL st ( for x being Real st x in Z holds sin . x <> 0 ) holds ( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) ) proofend; :: 41 f.x=sin.x*cos.x theorem :: FDIFF_4:41 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 (2 * x) ) ) proofend; :: 42 f.x=ln(cos.x) theorem :: FDIFF_4:42 for Z being open Subset of REAL st Z c= dom (ln * cos) & ( for x being Real st x in Z holds cos . x > 0 ) holds ( ln * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * cos) `| Z) . x = - (tan x) ) ) proofend; :: 43 f.x=ln(sin.x) theorem :: FDIFF_4:43 for Z being open Subset of REAL st Z c= dom (ln * sin) & ( for x being Real st x in Z holds sin . x > 0 ) holds ( ln * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * sin) `| Z) . x = cot x ) ) proofend; :: 44 f.x=-x*cos.x theorem Th44: :: FDIFF_4:44 for Z being open Subset of REAL st 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 = (- (cos . x)) + (x * (sin . x)) ) ) proofend; :: f.x=x*sin.x theorem Th45: :: FDIFF_4:45 for Z being open Subset of REAL st 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 = (sin . x) + (x * (cos . x)) ) ) proofend; :: 46 f.x=-x*cos.x+sin.x theorem :: FDIFF_4:46 for Z being open Subset of REAL st Z c= dom (((- (id Z)) (#) cos) + sin) holds ( ((- (id Z)) (#) cos) + sin is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) ) proofend; :: 47 f.x=x*sin.x+cos.x theorem :: FDIFF_4:47 for Z being open Subset of REAL st Z c= dom (((id Z) (#) sin) + cos) holds ( ((id Z) (#) sin) + cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) ) ) proofend; :: 48 f.x=2*(sin #R (1/2)) theorem :: FDIFF_4:48 for Z being open Subset of REAL st Z c= dom (2 (#) ((#R (1 / 2)) * sin)) & ( for x being Real st x in Z holds sin . x > 0 ) holds ( 2 (#) ((#R (1 / 2)) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) ) ) proofend; theorem Th49: :: FDIFF_4:49 for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) holds ( (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) ) ) proofend; :: 50 f.x=sin.x+(1/2)*(sin.x #Z 2) theorem :: FDIFF_4:50 for Z being open Subset of REAL st Z c= dom (sin + ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds ( sin . x > 0 & sin . x < 1 ) ) holds ( sin + ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) ) proofend; :: 51 f.x=(1/2)*(sin.x #Z 2)-cos.x theorem :: FDIFF_4:51 for Z being open Subset of REAL st Z c= dom (((1 / 2) (#) ((#Z 2) * sin)) - cos) & ( for x being Real st x in Z holds ( sin . x > 0 & cos . x < 1 ) ) holds ( ((1 / 2) (#) ((#Z 2) * sin)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) ) proofend; :: 52 f.x=sin.x-(1/2)*(sin #Z 2) theorem :: FDIFF_4:52 for Z being open Subset of REAL st Z c= dom (sin - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds ( sin . x > 0 & sin . x > - 1 ) ) holds ( sin - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) ) proofend; :: 53 f.x=-cos.x-(1/2)*(sin.x #Z 2) theorem :: FDIFF_4:53 for Z being open Subset of REAL st Z c= dom ((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds ( sin . x > 0 & cos . x > - 1 ) ) holds ( (- cos) - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) ) proofend; :: 54 f.x=(1/n)*(sin.x #Z n) theorem :: FDIFF_4:54 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * sin)) & n > 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 = ((sin . x) #Z (n - 1)) * (cos . x) ) ) proofend; :: exponential function :: 55 f.x=exp.x*(x-1) theorem :: FDIFF_4:55 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (exp_R (#) f) & ( for x being Real st x in Z holds f . x = x - 1 ) holds ( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) ) proofend; :: 56 f.x=ln(exp.x/(exp.x+1)) theorem :: FDIFF_4:56 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * (exp_R / (exp_R + f))) & ( for x being Real st x in Z holds f . x = 1 ) holds ( ln * (exp_R / (exp_R + f)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) ) ) proofend; :: 57 f.x=ln((exp.x-1)/exp.x) theorem :: FDIFF_4:57 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * ((exp_R - f) / exp_R)) & ( for x being Real st x in Z holds ( f . x = 1 & (exp_R - f) . x > 0 ) ) holds ( ln * ((exp_R - f) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) ) ) proofend;