:: Several Differentiable Formulas of Special Functions -- Part {II} :: by Yan Zhang , Bo Li and Xiquan Liang :: :: Received November 23, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin Lm1: for x being Real holds 1 - (cos (2 * x)) = 2 * ((sin x) ^2) proofend; Lm2: for x being Real holds 1 + (cos (2 * x)) = 2 * ((cos x) ^2) proofend; Lm3: for x being Real st sin . x > 0 holds sin . x = ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2) proofend; Lm4: for x being Real st sin . x > 0 & cos . x < 1 & cos . x > - 1 holds (sin . x) / ((1 - (cos . x)) #R (1 / 2)) = (1 + (cos . x)) #R (1 / 2) proofend; :: a #R x=exp.(x*ln a) theorem Th1: :: FDIFF_6:1 for a, x being Real st a > 0 holds exp_R . (x * (log (number_e,a))) = a #R x proofend; :: 15 a #R (-x)=exp.(-x*ln a) theorem Th2: :: FDIFF_6:2 for a, x being Real st a > 0 holds exp_R . (- (x * (log (number_e,a)))) = a #R (- x) proofend; Lm5: for x being Real st sin . x > 0 & cos . x < 1 & cos . x > - 1 holds (sin . x) / ((1 + (cos . x)) #R (1 / 2)) = (1 - (cos . x)) #R (1 / 2) proofend; :: 1 f.x=a^2-x^2 theorem Th3: :: FDIFF_6:3 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; :: 2 f.x=(a^2+x^2)/(a^2-x^2) theorem Th4: :: FDIFF_6:4 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)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (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 ^2)) * x) / (((a ^2) - (x |^ 2)) ^2) ) ) proofend; :: 3 f.x=ln((a^2+x^2)/(a^2-x^2)) theorem Th5: :: FDIFF_6:5 for a being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom f & f = ln * ((f1 + f2) / (f1 - f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 - f2) . x > 0 & a <> 0 ) ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = ((4 * (a ^2)) * x) / ((a |^ 4) - (x |^ 4)) ) ) proofend; :: 4 f.x=(1/(4*a^2))*ln((a^2+x^2)/(a^2-x^2)) theorem :: FDIFF_6:6 for a being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (4 * (a ^2))) (#) f) & f = ln * ((f1 + f2) / (f1 - f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 - f2) . x > 0 & a <> 0 ) ) holds ( (1 / (4 * (a ^2))) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (4 * (a ^2))) (#) f) `| Z) . x = x / ((a |^ 4) - (x |^ 4)) ) ) proofend; :: 5 f.x=x^2/(1+x^2) theorem Th7: :: FDIFF_6:7 for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 / (f2 + f1)) & f1 = #Z 2 & ( for x being Real st x in Z holds ( f2 . x = 1 & x <> 0 ) ) holds ( f1 / (f2 + f1) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / (f2 + f1)) `| Z) . x = (2 * x) / ((1 + (x ^2)) ^2) ) ) proofend; :: 6 f.x=(1/2)*ln(x^2/(1+x^2)) theorem :: FDIFF_6:8 for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) f) & f = ln * (f1 / (f2 + f1)) & f1 = #Z 2 & ( for x being Real st x in Z holds ( f2 . x = 1 & x <> 0 ) ) holds ( (1 / 2) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) f) `| Z) . x = 1 / (x * (1 + (x ^2))) ) ) proofend; :: 7 f.x=ln(x|^n) theorem :: FDIFF_6:9 for n being Element of NAT for Z being open Subset of REAL st Z c= dom (ln * (#Z n)) & ( for x being Real st x in Z holds x > 0 ) holds ( ln * (#Z n) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (#Z n)) `| Z) . x = n / x ) ) proofend; :: 8 f.x=1/x+ln((x-1)/x) theorem :: FDIFF_6:10 for Z being open Subset of REAL for f2, f1 being PartFunc of REAL,REAL st Z c= dom ((f2 ^) + (ln * (f1 / f2))) & ( for x being Real st x in Z holds ( f2 . x = x & f2 . x > 0 & f1 . x = x - 1 & f1 . x > 0 ) ) holds ( (f2 ^) + (ln * (f1 / f2)) is_differentiable_on Z & ( for x being Real st x in Z holds (((f2 ^) + (ln * (f1 / f2))) `| Z) . x = 1 / ((x ^2) * (x - 1)) ) ) proofend; :: 10 f.x=a #R x=exp.(x*ln a) theorem Th11: :: FDIFF_6:11 for a being Real 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 * (log (number_e,a)) ) & a > 0 holds ( exp_R * f is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * f) `| Z) . x = (a #R x) * (log (number_e,a)) ) ) proofend; :: 11 f.x=(a #R x)*(x-1/ln a)/ln a theorem :: FDIFF_6:12 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (log (number_e,a))) (#) ((exp_R * f1) (#) f2)) & ( for x being Real st x in Z holds ( f1 . x = x * (log (number_e,a)) & f2 . x = x - (1 / (log (number_e,a))) ) ) & a > 0 & a <> 1 holds ( (1 / (log (number_e,a))) (#) ((exp_R * f1) (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (log (number_e,a))) (#) ((exp_R * f1) (#) f2)) `| Z) . x = x * (a #R x) ) ) proofend; :: 12 f.x=a #R x*exp(x)/(1+ln a) theorem :: FDIFF_6:13 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / (1 + (log (number_e,a)))) (#) ((exp_R * f) (#) exp_R)) & ( for x being Real st x in Z holds f . x = x * (log (number_e,a)) ) & a > 0 & a <> 1 / number_e holds ( (1 / (1 + (log (number_e,a)))) (#) ((exp_R * f) (#) exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (1 + (log (number_e,a)))) (#) ((exp_R * f) (#) exp_R)) `| Z) . x = (a #R x) * (exp_R . x) ) ) proofend; :: 13 f.x=exp_R(-x) theorem Th14: :: FDIFF_6:14 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 ) holds ( exp_R * f is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * f) `| Z) . x = - (exp_R (- x)) ) ) proofend; :: 14 f.x=-(x+1)*exp_R(-x) theorem :: FDIFF_6:15 for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 (#) (exp_R * f2)) & ( for x being Real st x in Z holds ( f1 . x = (- x) - 1 & f2 . x = - x ) ) holds ( f1 (#) (exp_R * f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x) ) ) proofend; :: 16 f.x=a #R (-x)=exp_R.(-x*ln a) theorem Th16: :: FDIFF_6:16 for a being Real 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 * (log (number_e,a))) ) & a > 0 holds ( - (exp_R * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (exp_R * f)) `| Z) . x = (a #R (- x)) * (log (number_e,a)) ) ) proofend; :: 17 f.x=-(a #R -x)*(x+1/ln a)/ln a theorem :: FDIFF_6:17 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (log (number_e,a))) (#) ((- (exp_R * f1)) (#) f2)) & ( for x being Real st x in Z holds ( f1 . x = - (x * (log (number_e,a))) & f2 . x = x + (1 / (log (number_e,a))) ) ) & a > 0 & a <> 1 holds ( (1 / (log (number_e,a))) (#) ((- (exp_R * f1)) (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (log (number_e,a))) (#) ((- (exp_R * f1)) (#) f2)) `| Z) . x = x / (a #R x) ) ) proofend; :: 18 f.x=(1/(ln a-1))*a #R x/exp_R(x) theorem :: FDIFF_6:18 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / ((log (number_e,a)) - 1)) (#) ((exp_R * f) / exp_R)) & ( for x being Real st x in Z holds f . x = x * (log (number_e,a)) ) & a > 0 & a <> number_e holds ( (1 / ((log (number_e,a)) - 1)) (#) ((exp_R * f) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / ((log (number_e,a)) - 1)) (#) ((exp_R * f) / exp_R)) `| Z) . x = (a #R x) / (exp_R . x) ) ) proofend; :: 19 f.x=(1/(1-ln a))*exp_R(x)/a #R x theorem :: FDIFF_6:19 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / (1 - (log (number_e,a)))) (#) (exp_R / (exp_R * f))) & ( for x being Real st x in Z holds f . x = x * (log (number_e,a)) ) & a > 0 & a <> number_e holds ( (1 / (1 - (log (number_e,a)))) (#) (exp_R / (exp_R * f)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (1 - (log (number_e,a)))) (#) (exp_R / (exp_R * f))) `| Z) . x = (exp_R . x) / (a #R x) ) ) proofend; :: 20 f.x=ln(exp_R.x+1) theorem :: FDIFF_6:20 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * (exp_R + f)) & ( for x being Real st x in Z holds f . x = 1 ) holds ( ln * (exp_R + f) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (exp_R + f)) `| Z) . x = (exp_R . x) / ((exp_R . x) + 1) ) ) proofend; :: 21 f.x=ln(exp_R.x-1) theorem :: FDIFF_6:21 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * (exp_R - f)) & ( for x being Real st x in Z holds ( f . x = 1 & (exp_R - f) . x > 0 ) ) holds ( ln * (exp_R - f) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (exp_R - f)) `| Z) . x = (exp_R . x) / ((exp_R . x) - 1) ) ) proofend; :: 22 f.x=-ln(1-exp_R.x) theorem :: FDIFF_6:22 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (- (ln * (f - exp_R))) & ( for x being Real st x in Z holds ( f . x = 1 & (f - exp_R) . x > 0 ) ) holds ( - (ln * (f - exp_R)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * (f - exp_R))) `| Z) . x = (exp_R . x) / (1 - (exp_R . x)) ) ) proofend; :: 23 f.x=exp_R(2*x)+1 theorem Th23: :: FDIFF_6:23 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (((#Z 2) * exp_R) + f) & ( for x being Real st x in Z holds f . x = 1 ) holds ( ((#Z 2) * exp_R) + f is_differentiable_on Z & ( for x being Real st x in Z holds ((((#Z 2) * exp_R) + f) `| Z) . x = 2 * (exp_R (2 * x)) ) ) proofend; :: 24 f.x=(1/2)*ln(exp_R(2*x)+1) theorem :: FDIFF_6:24 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (ln * f)) & f = ((#Z 2) * exp_R) + f1 & ( for x being Real st x in Z holds f1 . x = 1 ) holds ( (1 / 2) (#) (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) + (exp_R (- x))) ) ) proofend; :: 25 f.x=exp_R(2*x)-1 theorem Th25: :: FDIFF_6:25 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (((#Z 2) * exp_R) - f) & ( for x being Real st x in Z holds f . x = 1 ) holds ( ((#Z 2) * exp_R) - f is_differentiable_on Z & ( for x being Real st x in Z holds ((((#Z 2) * exp_R) - f) `| Z) . x = 2 * (exp_R (2 * x)) ) ) proofend; :: 26 f.x=(1/2)*ln(exp_R(2*x)-1) theorem :: FDIFF_6:26 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (ln * f)) & f = ((#Z 2) * exp_R) - f1 & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) ) holds ( (1 / 2) (#) (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (ln * f)) `| Z) . x = (exp_R x) / ((exp_R x) - (exp_R (- x))) ) ) proofend; :: 27 f.x=(exp_R.x-1)^2 theorem Th27: :: FDIFF_6:27 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((#Z 2) * (exp_R - f)) & ( for x being Real st x in Z holds f . x = 1 ) holds ( (#Z 2) * (exp_R - f) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (exp_R - f)) `| Z) . x = (2 * (exp_R . x)) * ((exp_R . x) - 1) ) ) proofend; :: 28 f.x=ln((exp_R.x-1)^2/exp_R.x) theorem :: FDIFF_6:28 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom f & f = ln * (((#Z 2) * (exp_R - f1)) / exp_R) & ( for x being Real st x in Z holds ( f1 . x = 1 & (exp_R - f1) . x > 0 ) ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = ((exp_R . x) + 1) / ((exp_R . x) - 1) ) ) proofend; :: 29 f.x=(exp_R.x+1)^2 theorem Th29: :: FDIFF_6:29 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((#Z 2) * (exp_R + f)) & ( for x being Real st x in Z holds f . x = 1 ) holds ( (#Z 2) * (exp_R + f) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (exp_R + f)) `| Z) . x = (2 * (exp_R . x)) * ((exp_R . x) + 1) ) ) proofend; :: 30 f.x=ln((exp_R.x+1)^2/exp_R.x) theorem :: FDIFF_6:30 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom f & f = ln * (((#Z 2) * (exp_R + f1)) / exp_R) & ( for x being Real st x in Z holds f1 . x = 1 ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = ((exp_R . x) - 1) / ((exp_R . x) + 1) ) ) proofend; :: 31 f.x=(1-exp_R.x)^2 theorem Th31: :: FDIFF_6:31 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((#Z 2) * (f - exp_R)) & ( for x being Real st x in Z holds f . x = 1 ) holds ( (#Z 2) * (f - exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z 2) * (f - exp_R)) `| Z) . x = - ((2 * (exp_R . x)) * (1 - (exp_R . x))) ) ) proofend; :: 32 f.x=ln(exp_R.x/(1-exp_R.x)^2) theorem :: FDIFF_6:32 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom f & f = ln * (exp_R / ((#Z 2) * (f1 - exp_R))) & ( for x being Real st x in Z holds ( f1 . x = 1 & (f1 - exp_R) . x > 0 ) ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = (1 + (exp_R . x)) / (1 - (exp_R . x)) ) ) proofend; :: 33 f.x=ln(exp_R.x/(1+exp_R.x)^2) theorem :: FDIFF_6:33 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom f & f = ln * (exp_R / ((#Z 2) * (f1 + exp_R))) & ( for x being Real st x in Z holds f1 . x = 1 ) holds ( f is_differentiable_on Z & ( for x being Real st x in Z holds (f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x)) ) ) proofend; :: 34 f.x=ln(exp_R(x)+exp_R(-x)) theorem :: FDIFF_6:34 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom (ln * f) & f = exp_R + (exp_R * f1) & ( for x being Real st x in Z holds f1 . x = - x ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) ) ) proofend; :: 35 f.x=ln(exp_R(x)-exp_R(-x)) theorem :: FDIFF_6:35 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom (ln * f) & f = exp_R - (exp_R * f1) & ( for x being Real st x in Z holds ( f1 . x = - x & f . x > 0 ) ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) ) ) proofend; :: 36 f.x=(2/3)*((1+exp_R.x) #R (3/2)) theorem :: FDIFF_6:36 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * (f + exp_R))) & ( for x being Real st x in Z holds f . x = 1 ) holds ( (2 / 3) (#) ((#R (3 / 2)) * (f + exp_R)) is_differentiable_on Z & ( for x being Real 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)) ) ) proofend; :: 37 f.x=(2/(3*lna))*((1+a |^x) #R (3/2)) theorem :: FDIFF_6:37 for a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((2 / (3 * (log (number_e,a)))) (#) ((#R (3 / 2)) * (f + (exp_R * f1)))) & ( for x being Real st x in Z holds ( f . x = 1 & f1 . x = x * (log (number_e,a)) ) ) & a > 0 & a <> 1 holds ( (2 / (3 * (log (number_e,a)))) (#) ((#R (3 / 2)) * (f + (exp_R * f1))) is_differentiable_on Z & ( for x being Real 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)) ) ) proofend; :: 38 f.x=(-1/2)*cos(2*x) theorem :: FDIFF_6:38 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- (1 / 2)) (#) (cos * f)) & ( for x being Real st x in Z holds f . x = 2 * x ) holds ( (- (1 / 2)) (#) (cos * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (1 / 2)) (#) (cos * f)) `| Z) . x = sin (2 * x) ) ) proofend; theorem :: FDIFF_6:39 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * (f - cos))) & ( for x being Real st x in Z holds ( f . x = 1 & sin . x > 0 & cos . x < 1 & cos . x > - 1 ) ) holds ( 2 (#) ((#R (1 / 2)) * (f - cos)) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * (f - cos))) `| Z) . x = (1 + (cos . x)) #R (1 / 2) ) ) proofend; theorem :: FDIFF_6:40 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- 2) (#) ((#R (1 / 2)) * (f + cos))) & ( for x being Real st x in Z holds ( f . x = 1 & sin . x > 0 & cos . x < 1 & cos . x > - 1 ) ) holds ( (- 2) (#) ((#R (1 / 2)) * (f + cos)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 2) (#) ((#R (1 / 2)) * (f + cos))) `| Z) . x = (1 - (cos . x)) #R (1 / 2) ) ) proofend; Lm6: for Z being open Subset of REAL for f1 being PartFunc of REAL,REAL st Z c= dom (f1 + (2 (#) sin)) & ( for x being Real st x in Z holds f1 . x = 1 ) holds ( f1 + (2 (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + (2 (#) sin)) `| Z) . x = 2 * (cos . x) ) ) proofend; theorem :: FDIFF_6:41 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (ln * f)) & f = f1 + (2 (#) sin) & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) ) holds ( (1 / 2) (#) (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (ln * f)) `| Z) . x = (cos . x) / (1 + (2 * (sin . x))) ) ) proofend; Lm7: for Z being open Subset of REAL for f1 being PartFunc of REAL,REAL st Z c= dom (f1 + (2 (#) cos)) & ( for x being Real st x in Z holds f1 . x = 1 ) holds ( f1 + (2 (#) cos) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + (2 (#) cos)) `| Z) . x = - (2 * (sin . x)) ) ) proofend; theorem :: FDIFF_6:42 for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((- (1 / 2)) (#) (ln * f)) & f = f1 + (2 (#) cos) & ( for x being Real st x in Z holds ( f1 . x = 1 & f . x > 0 ) ) holds ( (- (1 / 2)) (#) (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (1 / 2)) (#) (ln * f)) `| Z) . x = (sin . x) / (1 + (2 * (cos . x))) ) ) proofend; :: 43 f.x=1/(4*a)*sin(2*a*x) theorem Th43: :: FDIFF_6:43 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / (4 * a)) (#) (sin * f)) & ( for x being Real st x in Z holds f . x = (2 * a) * x ) & a <> 0 holds ( (1 / (4 * a)) (#) (sin * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (4 * a)) (#) (sin * f)) `| Z) . x = (1 / 2) * (cos ((2 * a) * x)) ) ) proofend; :: 44 f.x=x/2-1/(4*a)*sin(2*a*x) theorem :: FDIFF_6:44 for a being Real for Z being open Subset of REAL for f1, f being PartFunc of REAL,REAL st Z c= dom (f1 - ((1 / (4 * a)) (#) (sin * f))) & ( for x being Real st x in Z holds ( f1 . x = x / 2 & f . x = (2 * a) * x ) ) & a <> 0 holds ( f1 - ((1 / (4 * a)) (#) (sin * f)) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 - ((1 / (4 * a)) (#) (sin * f))) `| Z) . x = (sin (a * x)) ^2 ) ) proofend; :: 45 f.x=x/2+1/(4*a)*sin(2*a*x) theorem :: FDIFF_6:45 for a being Real for Z being open Subset of REAL for f1, f being PartFunc of REAL,REAL st Z c= dom (f1 + ((1 / (4 * a)) (#) (sin * f))) & ( for x being Real st x in Z holds ( f1 . x = x / 2 & f . x = (2 * a) * x ) ) & a <> 0 holds ( f1 + ((1 / (4 * a)) (#) (sin * f)) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + ((1 / (4 * a)) (#) (sin * f))) `| Z) . x = (cos (a * x)) ^2 ) ) proofend; :: 46 f.x=(1/n)*(cos.x #Z n) theorem Th46: :: FDIFF_6:46 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * cos)) & n > 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 = - (((cos . x) #Z (n - 1)) * (sin . x)) ) ) proofend; :: 47 f.x=(1/3)*(cos.x #Z 3)-cos.x theorem :: FDIFF_6:47 for Z being open Subset of REAL st Z c= dom (((1 / 3) (#) ((#Z 3) * cos)) - cos) holds ( ((1 / 3) (#) ((#Z 3) * cos)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / 3) (#) ((#Z 3) * cos)) - cos) `| Z) . x = (sin . x) |^ 3 ) ) proofend; :: 48 f.x=sin.x-(1/3)*(sin.x #Z 3) theorem :: FDIFF_6:48 for Z being open Subset of REAL st Z c= dom (sin - ((1 / 3) (#) ((#Z 3) * sin))) holds ( sin - ((1 / 3) (#) ((#Z 3) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin - ((1 / 3) (#) ((#Z 3) * sin))) `| Z) . x = (cos . x) |^ 3 ) ) proofend; :: 49 f.x=sin(ln x) theorem :: FDIFF_6:49 for Z being open Subset of REAL st Z c= dom (sin * ln) holds ( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ln) `| Z) . x = (cos . (log (number_e,x))) / x ) ) proofend; :: 50 f.x=-cos(ln x) theorem :: FDIFF_6:50 for Z being open Subset of REAL st Z c= dom (- (cos * ln)) holds ( - (cos * ln) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ) ) proofend;