:: Several Differentiation Formulas of Special Functions -- Part {III}
:: by Bo Li , Yan Zhang and Xiquan Liang
::
:: Copyright (c) 2006-2021 Association of Mizar Users

theorem Th1: :: FDIFF_7:1
for x being Real holds x #Z 2 = x ^2
proof end;

theorem Th2: :: FDIFF_7:2
for x being Real st x > 0 holds
x #R (1 / 2) = sqrt x
proof end;

theorem Th3: :: FDIFF_7:3
for x being Real st x > 0 holds
x #R (- (1 / 2)) = 1 / (sqrt x)
proof end;

Lm1: for x being Real holds 2 * ((cos . (x / 2)) ^2) = 1 + (cos . x)
proof end;

Lm2: for x being Real holds 2 * ((sin . (x / 2)) ^2) = 1 - (cos . x)
proof end;

::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 () holds
( r (#) arcsin is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = r / (sqrt (1 - (x ^2))) ) )
proof end;

::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 () holds
( r (#) arccos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (r / (sqrt (1 - (x ^2)))) ) )
proof end;

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 ((),x) = (diff (f,x)) / (sqrt (1 - ((f . x) ^2))) )
proof end;

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 ((),x) = - ((diff (f,x)) / (sqrt (1 - ((f . x) ^2)))) )
proof end;

::f.x=ln(arcsin.x)
theorem :: FDIFF_7:8
for Z being open Subset of REAL st Z c= dom () & 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
(() | Z) . x = 1 / ((sqrt (1 - (x ^2))) * ()) ) )
proof end;

::f.x=ln(arccos.x)
theorem :: FDIFF_7:9
for Z being open Subset of REAL st Z c= dom () & 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
(() | Z) . x = - (1 / ((sqrt (1 - (x ^2))) * ())) ) )
proof end;

::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 * (() #Z (n - 1))) / (sqrt (1 - (x ^2))) ) )
proof end;

::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 * (() #Z (n - 1))) / (sqrt (1 - (x ^2)))) ) )
proof end;

::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 = () / (sqrt (1 - (x ^2))) ) )
proof end;

::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 = - (() / (sqrt (1 - (x ^2)))) ) )
proof end;

::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 () & ( 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
(() | Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) ) )
proof end;

::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 () & ( 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
(() | Z) . x = - (a / (sqrt (1 - (((a * x) + b) ^2)))) ) )
proof end;

::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 = () + (x / (sqrt (1 - (x ^2)))) ) )
proof end;

::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 = () - (x / (sqrt (1 - (x ^2)))) ) )
proof end;

::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 () & 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
(() | Z) . x = (a * ()) + (((a * x) + b) / (sqrt (1 - (x ^2)))) ) )
proof end;

::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 () & 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
(() | Z) . x = (a * ()) - (((a * x) + b) / (sqrt (1 - (x ^2)))) ) )
proof end;

::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) (#) ()) & ( for x being Real st x in Z holds
( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds
( (1 / 2) (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ()) | Z) . x = 1 / (sqrt (1 - ((2 * x) ^2))) ) )
proof end;

::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) (#) ()) & ( for x being Real st x in Z holds
( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds
( (1 / 2) (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ()) | Z) . x = - (1 / (sqrt (1 - ((2 * x) ^2)))) ) )
proof end;

::f.x=(1-x|^2) ^ (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)))) ) )
proof end;

::f.x=x*arcsin.x+(1-x^2) ^ (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 ) )
proof end;

::f.x=x*arccos.x-(1-x^2) ^ (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 ) )
proof end;

::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) (#) ()) & ( for x being Real st x in Z holds
( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds
( (id Z) (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ()) | Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2))))) ) )
proof end;

::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) (#) ()) & ( for x being Real st x in Z holds
( f . x = x / a & f . x > - 1 & f . x < 1 ) ) holds
( (id Z) (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) ()) | Z) . x = (arccos . (x / a)) - (x / (a * (sqrt (1 - ((x / a) ^2))))) ) )
proof end;

::f.x=(a^2-x^2) ^ (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)))) ) )
proof end;

::f.x=x*arcsin(x/a)+(a^2-x^2) ^ (1/2)
theorem :: FDIFF_7:28
for a being Real
for Z being open Subset of REAL
for f, f1, f2, f3 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) ) )
proof end;

::f.x=x*arccos(x/a)-(a^2-x^2) ^ (1/2)
theorem :: FDIFF_7:29
for a being Real
for Z being open Subset of REAL
for f, f1, f2, f3 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) ) )
proof end;

::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) * ())) & n > 0 & ( for x being Real st x in Z holds
sin . x <> 0 ) holds
( (- (1 / n)) (#) ((#Z n) * ()) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / n)) (#) ((#Z n) * ())) | Z) . x = (cos . x) / ((sin . x) #Z (n + 1)) ) )
proof end;

::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) * ())) & n > 0 & ( for x being Real st x in Z holds
cos . x <> 0 ) holds
( (1 / n) (#) ((#Z n) * ()) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * ())) | Z) . x = (sin . x) / ((cos . x) #Z (n + 1)) ) )
proof end;

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 () & ( 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
(() | Z) . x = (cos . (ln . x)) / x ) )
proof end;

::f.x=cos(ln.x)
theorem :: FDIFF_7:33
for Z being open Subset of REAL st Z c= dom () & ( 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
(() | Z) . x = - ((sin . (ln . x)) / x) ) )
proof end;

::f.x=sin(exp.x)
theorem :: FDIFF_7:34
for Z being open Subset of REAL st Z c= dom () holds
( sin * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = () * (cos . ()) ) )
proof end;

::f.x=cos(exp_R.x)
theorem :: FDIFF_7:35
for Z being open Subset of REAL st Z c= dom () holds
( cos * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (() * (sin . ())) ) )
proof end;

::f.x=exp_R.(cos.x)
theorem :: FDIFF_7:36
for Z being open Subset of REAL st Z c= dom () holds
( exp_R * cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((exp_R . (cos . x)) * (sin . x)) ) )
proof end;

::f.x=exp_R.(sin.x)
theorem :: FDIFF_7:37
for Z being open Subset of REAL st Z c= dom () holds
( exp_R * sin is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (exp_R . (sin . x)) * (cos . x) ) )
proof end;

::f.x=sin.x+cos.x
theorem Th38: :: FDIFF_7:38
for Z being open Subset of REAL st Z c= dom () holds
( sin + cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (cos . x) - (sin . x) ) )
proof end;

::f.x=sin.x-cos.x
theorem Th39: :: FDIFF_7:39
for Z being open Subset of REAL st Z c= dom () holds
( sin - cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (cos . x) + (sin . x) ) )
proof end;

::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 (#) ()) holds
( exp_R (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) ()) | Z) . x = (2 * ()) * (sin . x) ) )
proof end;

::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 (#) ()) holds
( exp_R (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) ()) | Z) . x = (2 * ()) * (cos . x) ) )
proof end;

::f.x=(sin.x+cos.x)/exp_R.x
theorem :: FDIFF_7:42
for Z being open Subset of REAL st Z c= dom (() / exp_R) holds
( () / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((() / exp_R) | Z) . x = - ((2 * (sin . x)) / ()) ) )
proof end;

::f.x=(sin.x-cos.x)/exp_R.x
theorem :: FDIFF_7:43
for Z being open Subset of REAL st Z c= dom (() / exp_R) holds
( () / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((() / exp_R) | Z) . x = (2 * (cos . x)) / () ) )
proof end;

::f.x=exp_R.x*sin.x
theorem :: FDIFF_7:44
for Z being open Subset of REAL st Z c= dom () holds
( exp_R (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = () * ((sin . x) + (cos . x)) ) )
proof end;

::f.x=exp_R.x*cos.x
theorem :: FDIFF_7:45
for Z being open Subset of REAL st Z c= dom () holds
( exp_R (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = () * ((cos . x) - (sin . x)) ) )
proof end;

:: 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 ((),x) = 1 / ((cos . x) ^2) )
proof end;

::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 ((),x) = - (1 / ((sin . x) ^2)) )
proof end;

::f.x=(tan.x) ^ 2
theorem :: FDIFF_7:48
for Z being open Subset of REAL st Z c= dom ((#Z 2) * ()) & ( for x being Real st x in Z holds
cos . x <> 0 ) holds
( (#Z 2) * () is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z 2) * ()) | Z) . x = (2 * (sin . x)) / ((cos . x) #Z 3) ) )
proof end;

::f.x=(cot.x) ^ 2
theorem :: FDIFF_7:49
for Z being open Subset of REAL st Z c= dom ((#Z 2) * ()) & ( for x being Real st x in Z holds
sin . x <> 0 ) holds
( (#Z 2) * () is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z 2) * ()) | Z) . x = - ((2 * (cos . x)) / ((sin . x) #Z 3)) ) )
proof end;

::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 (() * f) & ( for x being Real st x in Z holds
( f . x = x / 2 & cos . (f . x) <> 0 ) ) holds
( () * f is_differentiable_on Z & ( for x being Real st x in Z holds
((() * f) | Z) . x = 1 / (1 + (cos . x)) ) )
proof end;

::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 (() * f) & ( for x being Real st x in Z holds
( f . x = x / 2 & sin . (f . x) <> 0 ) ) holds
( () * f is_differentiable_on Z & ( for x being Real st x in Z holds
((() * f) | Z) . x = - (1 / (1 - (cos . x))) ) )
proof end;