:: Several Integrability Formulas of Special Functions
:: by Cuiying Peng , Fuguo Ge and Xiquan Liang
::
:: Copyright (c) 2007-2018 Association of Mizar Users

Lm1: sin (PI / 4) > 0
proof end;

Lm2: sin (- (PI / 4)) < 0
proof end;

theorem Th1: :: INTEGRA8:1
for x being Real
for n being Element of NAT holds sin (x + ((2 * n) * PI)) = sin x
proof end;

theorem Th2: :: INTEGRA8:2
for x being Real
for n being Element of NAT holds sin (x + (((2 * n) + 1) * PI)) = - (sin x)
proof end;

theorem Th3: :: INTEGRA8:3
for x being Real
for n being Element of NAT holds cos (x + ((2 * n) * PI)) = cos x
proof end;

theorem Th4: :: INTEGRA8:4
for x being Real
for n being Element of NAT holds cos (x + (((2 * n) + 1) * PI)) = - (cos x)
proof end;

theorem Th5: :: INTEGRA8:5
for x being Real st sin (x / 2) >= 0 holds
sin (x / 2) = sqrt ((1 - (cos x)) / 2)
proof end;

theorem Th6: :: INTEGRA8:6
for x being Real st sin (x / 2) < 0 holds
sin (x / 2) = - (sqrt ((1 - (cos x)) / 2))
proof end;

theorem Th7: :: INTEGRA8:7
sin (PI / 4) = (sqrt 2) / 2
proof end;

theorem Th8: :: INTEGRA8:8
sin (- (PI / 4)) = - ((sqrt 2) / 2)
proof end;

theorem Th9: :: INTEGRA8:9
[.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] c= ].(- 1),1.[
proof end;

theorem Th10: :: INTEGRA8:10
arcsin ((sqrt 2) / 2) = PI / 4
proof end;

theorem Th11: :: INTEGRA8:11
arcsin (- ((sqrt 2) / 2)) = - (PI / 4)
proof end;

theorem Th12: :: INTEGRA8:12
for x being Real st cos (x / 2) >= 0 holds
cos (x / 2) = sqrt ((1 + (cos x)) / 2)
proof end;

Lm3: cos (PI / 4) > 0
proof end;

theorem Th13: :: INTEGRA8:13
cos (PI / 4) = (sqrt 2) / 2
proof end;

theorem Th14: :: INTEGRA8:14
cos ((3 * PI) / 4) = - ((sqrt 2) / 2)
proof end;

theorem Th15: :: INTEGRA8:15
arccos ((sqrt 2) / 2) = PI / 4
proof end;

theorem Th16: :: INTEGRA8:16
arccos (- ((sqrt 2) / 2)) = (3 * PI) / 4
proof end;

theorem Th17: :: INTEGRA8:17
sinh . 1 = (() - 1) / ()
proof end;

theorem Th18: :: INTEGRA8:18
proof end;

theorem Th19: :: INTEGRA8:19
cosh . 1 = (() + 1) / ()
proof end;

Lm4: for f1, f2 being PartFunc of REAL,REAL holds (- f1) (#) (- f2) = f1 (#) f2
proof end;

theorem Th20: :: INTEGRA8:20
for L1 being LinearFunc holds - L1 is LinearFunc
proof end;

theorem Th21: :: INTEGRA8:21
for R1 being RestFunc holds - R1 is RestFunc
proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem Th22: :: INTEGRA8:22
for f1 being PartFunc of REAL,REAL
for x0 being Real st f1 is_differentiable_in x0 holds
( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) )
proof end;

theorem Th23: :: INTEGRA8:23
for f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st Z c= dom (- f1) & f1 is_differentiable_on Z holds
( - f1 is_differentiable_on Z & ( for x being Real st x in Z holds
((- f1) | Z) . x = - (diff (f1,x)) ) )
proof end;

theorem :: INTEGRA8:24
proof end;

theorem Th25: :: INTEGRA8:25
for x being Real holds
( - cos is_differentiable_in x & diff ((),x) = sin . x )
proof end;

theorem Th26: :: INTEGRA8:26
( - cos is_differentiable_on REAL & ( for x being Real st x in REAL holds
diff ((),x) = sin . x ) )
proof end;

theorem Th27: :: INTEGRA8:27
proof end;

theorem Th28: :: INTEGRA8:28
proof end;

theorem Th29: :: INTEGRA8:29

theorem Th30: :: INTEGRA8:30
proof end;

theorem Th31: :: INTEGRA8:31
proof end;

theorem Th32: :: INTEGRA8:32
proof end;

theorem Th33: :: INTEGRA8:33
for Z being open Subset of REAL st Z c= dom tan holds
( tan is_differentiable_on Z & ( for x being Real st x in Z holds
() . x = 1 / ((cos . x) ^2) ) )
proof end;

theorem Th34: :: INTEGRA8:34
for Z being open Subset of REAL st Z c= dom cot holds
( cot is_differentiable_on Z & ( for x being Real st x in Z holds
() . x = - (1 / ((sin . x) ^2)) ) )
proof end;

theorem :: INTEGRA8:35
for r being Real holds rng () c= REAL
proof end;

definition
let r be Real;
func Cst r -> Function of REAL,REAL equals :: INTEGRA8:def 1
REAL --> r;
coherence
REAL --> r is Function of REAL,REAL
proof end;
end;

:: deftheorem defines Cst INTEGRA8:def 1 :
for r being Real holds Cst r = REAL --> r;

theorem Th36: :: INTEGRA8:36
for a, b being Real
for A being non empty closed_interval Subset of REAL holds chi (A,A) = (Cst 1) | A
proof end;

theorem Th37: :: INTEGRA8:37
for a, b being Real
for A being non empty closed_interval Subset of REAL st A = [.a,b.] holds
( upper_bound A = b & lower_bound A = a )
proof end;

theorem :: INTEGRA8:38
for a, b being Real st a <= b holds
integral ((Cst 1),a,b) = b - a
proof end;

Lm5:
by FUNCT_2:def 1;

Lm6:
by FUNCT_2:def 1;

Lm7: dom () = REAL
by FUNCT_2:def 1;

Lm8:
by FUNCT_2:def 1;

Lm9:
by FUNCT_2:def 1;

Lm10:
by FUNCT_2:def 1;

Lm11: for A being non empty closed_interval Subset of REAL holds
( cos is_integrable_on A & cos | A is bounded )

proof end;

theorem Th39: :: INTEGRA8:39
for A being non empty closed_interval Subset of REAL holds integral (cos,A) = (sin . ()) - (sin . ())
proof end;

theorem :: INTEGRA8:40
for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds
integral (cos,A) = 1
proof end;

theorem :: INTEGRA8:41
for A being non empty closed_interval Subset of REAL st A = holds
integral (cos,A) = 0
proof end;

theorem :: INTEGRA8:42
for A being non empty closed_interval Subset of REAL st A = [.0,((PI * 3) / 2).] holds
integral (cos,A) = - 1
proof end;

theorem :: INTEGRA8:43
for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds
integral (cos,A) = 0
proof end;

theorem :: INTEGRA8:44
for A being non empty closed_interval Subset of REAL
for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
integral (cos,A) = 0
proof end;

theorem :: INTEGRA8:45
for A being non empty closed_interval Subset of REAL
for x being Real
for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
integral (cos,A) = - (2 * (sin x))
proof end;

Lm12: for A being non empty closed_interval Subset of REAL holds
( - sin is_integrable_on A & () | A is bounded )

proof end;

theorem Th46: :: INTEGRA8:46
for A being non empty closed_interval Subset of REAL holds integral ((),A) = (cos . ()) - (cos . ())
proof end;

theorem :: INTEGRA8:47
for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds
integral ((),A) = - 1
proof end;

theorem :: INTEGRA8:48
for A being non empty closed_interval Subset of REAL st A = holds
integral ((),A) = - 2
proof end;

theorem :: INTEGRA8:49
for A being non empty closed_interval Subset of REAL st A = [.0,((PI * 3) / 2).] holds
integral ((),A) = - 1
proof end;

theorem :: INTEGRA8:50
for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds
integral ((),A) = 0
proof end;

theorem :: INTEGRA8:51
for A being non empty closed_interval Subset of REAL
for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
integral ((),A) = - 2
proof end;

theorem :: INTEGRA8:52
for A being non empty closed_interval Subset of REAL
for x being Real
for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
integral ((),A) = - (2 * (cos x))
proof end;

Lm13: for A being non empty closed_interval Subset of REAL holds
( exp_R is_integrable_on A & exp_R | A is bounded )

proof end;

theorem Th53: :: INTEGRA8:53
for A being non empty closed_interval Subset of REAL holds integral (exp_R,A) = () - ()
proof end;

reconsider jj = 1 as Real ;

theorem :: INTEGRA8:54
for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds
integral (exp_R,A) = number_e - 1
proof end;

Lm14: for A being non empty closed_interval Subset of REAL holds sinh | A is continuous
proof end;

Lm15: for A being non empty closed_interval Subset of REAL holds
( sinh is_integrable_on A & sinh | A is bounded )

by ;

theorem Th55: :: INTEGRA8:55
for A being non empty closed_interval Subset of REAL holds integral (sinh,A) = (cosh . ()) - (cosh . ())
proof end;

theorem :: INTEGRA8:56
for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds
integral (sinh,A) = (() ^2) / ()
proof end;

Lm16: for A being non empty closed_interval Subset of REAL holds cosh | A is continuous
proof end;

Lm17: for A being non empty closed_interval Subset of REAL holds
( cosh is_integrable_on A & cosh | A is bounded )

by ;

theorem Th57: :: INTEGRA8:57
for A being non empty closed_interval Subset of REAL holds integral (cosh,A) = (sinh . ()) - (sinh . ())
proof end;

theorem :: INTEGRA8:58
for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds
integral (cosh,A) = (() - 1) / ()
proof end;

theorem :: INTEGRA8:59
for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z & dom tan = Z & dom tan = dom f2 & ( for x being Real st x in Z holds
( f2 . x = 1 / ((cos . x) ^2) & cos . x <> 0 ) ) & f2 | A is continuous holds
integral (f2,A) = (tan . ()) - (tan . ())
proof end;

theorem :: INTEGRA8:60
for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z & dom cot = Z & dom cot = dom f2 & ( for x being Real st x in Z holds
( f2 . x = - (1 / ((sin . x) ^2)) & sin . x <> 0 ) ) & f2 | A is continuous holds
integral (f2,A) = (cot . ()) - (cot . ())
proof end;

theorem :: INTEGRA8:61
for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st dom tanh = dom f2 & ( for x being Real st x in REAL holds
f2 . x = 1 / (() ^2) ) & f2 | A is continuous holds
integral (f2,A) = (tanh . ()) - (tanh . ())
proof end;

Lm18: dom (arcsin | ].(- 1),1.[) = ].(- 1),1.[
by ;

theorem Th62: :: INTEGRA8:62
for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st A c= ].(- 1),1.[ & dom (arcsin | ].(- 1),1.[) = dom f2 & ( for x being Real holds
( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) ) & f2 | A is continuous holds
integral (f2,A) = () - ()
proof end;

theorem Th63: :: INTEGRA8:63
for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st A c= ].(- 1),1.[ & dom (arccos | ].(- 1),1.[) = dom f2 & ( for x being Real holds
( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) ) & f2 | A is continuous holds
integral (f2,A) = () - ()
proof end;

theorem :: INTEGRA8:64
for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arcsin | ].(- 1),1.[) = dom f2 & ( for x being Real holds
( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) ) & f2 | A is continuous holds
integral (f2,A) = PI / 2
proof end;

theorem :: INTEGRA8:65
for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arccos | ].(- 1),1.[) = dom f2 & ( for x being Real holds
( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) ) & f2 | A is continuous holds
integral (f2,A) = - (PI / 2)
proof end;

theorem Th66: :: INTEGRA8:66
for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f | Z is_integrable_on A & (f | Z) | A is bounded & g | Z is_integrable_on A & (g | Z) | A is bounded holds
integral (((f | Z) + (g | Z)),A) = (((f . ()) - (f . ())) + (g . ())) - (g . ())
proof end;

theorem Th67: :: INTEGRA8:67
for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f | Z is_integrable_on A & (f | Z) | A is bounded & g | Z is_integrable_on A & (g | Z) | A is bounded holds
integral (((f | Z) - (g | Z)),A) = ((f . ()) - (f . ())) - ((g . ()) - (g . ()))
proof end;

theorem Th68: :: INTEGRA8:68
for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL
for r being Real
for Z being open Subset of REAL st f is_differentiable_on Z & A c= Z & f | Z is_integrable_on A & (f | Z) | A is bounded holds
integral ((r (#) (f `| Z)),A) = (r * (f . ())) - (r * (f . ()))
proof end;

Lm19: for A being non empty closed_interval Subset of REAL holds
( sin is_integrable_on A & sin | A is bounded )

proof end;

theorem Th69: :: INTEGRA8:69
for A being non empty closed_interval Subset of REAL holds integral ((),A) = (((() . ()) - (() . ())) + (sin . ())) - (sin . ())
proof end;

theorem :: INTEGRA8:70
for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds
integral ((),A) = 2
proof end;

theorem :: INTEGRA8:71
for A being non empty closed_interval Subset of REAL st A = holds
integral ((),A) = 2
proof end;

theorem :: INTEGRA8:72
for A being non empty closed_interval Subset of REAL st A = [.0,((PI * 3) / 2).] holds
integral ((),A) = 0
proof end;

theorem :: INTEGRA8:73
for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds
integral ((),A) = 0
proof end;

theorem :: INTEGRA8:74
for A being non empty closed_interval Subset of REAL
for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
integral ((),A) = 2
proof end;

theorem :: INTEGRA8:75
for A being non empty closed_interval Subset of REAL
for x being Real
for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
integral ((),A) = (2 * (cos x)) - (2 * (sin x))
proof end;

theorem Th76: :: INTEGRA8:76
for A being non empty closed_interval Subset of REAL holds integral ((),A) = (((cosh . ()) - (cosh . ())) + (sinh . ())) - (sinh . ())
proof end;

theorem :: INTEGRA8:77
for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds
integral ((),A) = number_e - 1
proof end;

theorem Th78: :: INTEGRA8:78
for A being non empty closed_interval Subset of REAL holds integral ((),A) = ((() . ()) - (() . ())) - ((sin . ()) - (sin . ()))
proof end;

theorem :: INTEGRA8:79
for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds
integral ((),A) = 0
proof end;

theorem :: INTEGRA8:80
for A being non empty closed_interval Subset of REAL st A = holds
integral ((),A) = 2
proof end;

theorem :: INTEGRA8:81
for A being non empty closed_interval Subset of REAL st A = [.0,((PI * 3) / 2).] holds
integral ((),A) = 2
proof end;

theorem :: INTEGRA8:82
for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds
integral ((),A) = 0
proof end;

theorem :: INTEGRA8:83
for A being non empty closed_interval Subset of REAL
for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
integral ((),A) = 2
proof end;

theorem :: INTEGRA8:84
for A being non empty closed_interval Subset of REAL
for x being Real
for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
integral ((),A) = (2 * (cos x)) + (2 * (sin x))
proof end;

theorem :: INTEGRA8:85
for A being non empty closed_interval Subset of REAL
for r being Real holds integral ((),A) = (r * (() . ())) - (r * (() . ()))
proof end;

theorem :: INTEGRA8:86
for A being non empty closed_interval Subset of REAL
for r being Real holds integral ((),A) = (r * (sin . ())) - (r * (sin . ()))
proof end;

theorem :: INTEGRA8:87
for A being non empty closed_interval Subset of REAL
for r being Real holds integral ((),A) = (r * (cosh . ())) - (r * (cosh . ()))
proof end;

theorem :: INTEGRA8:88
for A being non empty closed_interval Subset of REAL
for r being Real holds integral ((),A) = (r * (sinh . ())) - (r * (sinh . ()))
proof end;

theorem :: INTEGRA8:89
for A being non empty closed_interval Subset of REAL
for r being Real holds integral ((),A) = (r * ()) - (r * ())
proof end;

theorem Th90: :: INTEGRA8:90
for A being non empty closed_interval Subset of REAL holds integral ((),A) = (1 / 2) * (((cos . ()) * (cos . ())) - ((cos . ()) * (cos . ())))
proof end;

theorem :: INTEGRA8:91
for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds
integral ((),A) = 1 / 2
proof end;

theorem :: INTEGRA8:92
for A being non empty closed_interval Subset of REAL st A = holds
integral ((),A) = 0
proof end;

theorem :: INTEGRA8:93
for A being non empty closed_interval Subset of REAL st A = [.0,(PI * (3 / 2)).] holds
integral ((),A) = 1 / 2
proof end;

theorem :: INTEGRA8:94
for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds
integral ((),A) = 0
proof end;

theorem :: INTEGRA8:95
for A being non empty closed_interval Subset of REAL
for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
integral ((),A) = 0
proof end;

theorem :: INTEGRA8:96
for A being non empty closed_interval Subset of REAL
for x being Real
for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
integral ((),A) = 0
proof end;

Lm20: for A being non empty closed_interval Subset of REAL holds
( cos (#) cos is_integrable_on A & () | A is bounded )

proof end;

theorem :: INTEGRA8:97
for A being non empty closed_interval Subset of REAL holds integral ((),A) = (((cos . ()) * (sin . ())) - ((cos . ()) * (sin . ()))) + (integral ((),A))
proof end;

theorem :: INTEGRA8:98
for A being non empty closed_interval Subset of REAL holds integral ((),A) = (((cosh . ()) * (sinh . ())) - ((cosh . ()) * (sinh . ()))) - (integral ((),A))
proof end;

theorem :: INTEGRA8:99
for A being non empty closed_interval Subset of REAL holds integral ((),A) = (1 / 2) * (((cosh . ()) * (cosh . ())) - ((cosh . ()) * (cosh . ())))
proof end;

theorem :: INTEGRA8:100
for A being non empty closed_interval Subset of REAL holds integral ((),A) = (1 / 2) * ((() ^2) - (() ^2))
proof end;

Lm21: for A being non empty closed_interval Subset of REAL holds
( exp_R (#) () is_integrable_on A & (exp_R (#) ()) | A is bounded )

proof end;

Lm22: for A being non empty closed_interval Subset of REAL holds
( exp_R (#) () is_integrable_on A & (exp_R (#) ()) | A is bounded )

proof end;

theorem :: INTEGRA8:101
for A being non empty closed_interval Subset of REAL holds integral ((exp_R (#) ()),A) = (() . ()) - (() . ())
proof end;

theorem :: INTEGRA8:102
for A being non empty closed_interval Subset of REAL holds integral ((exp_R (#) ()),A) = (() . ()) - (() . ())
proof end;