:: by Cuiying Peng , Fuguo Ge and Xiquan Liang

::

:: Received August 28, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

Lm1: sin (PI / 4) > 0

proof end;

Lm2: sin (- (PI / 4)) < 0

proof end;

Lm3: cos (PI / 4) > 0

proof end;

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

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)) )

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)) ) )

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 Th26: :: INTEGRA8:26

( - cos is_differentiable_on REAL & ( for x being Real st x in REAL holds

diff ((- cos),x) = sin . x ) )

diff ((- cos),x) = sin . x ) )

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

(tan `| Z) . x = 1 / ((cos . x) ^2) ) )

( tan is_differentiable_on Z & ( for x being Real st x in Z holds

(tan `| Z) . 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

(cot `| Z) . x = - (1 / ((sin . x) ^2)) ) )

( cot is_differentiable_on Z & ( for x being Real st x in Z holds

(cot `| Z) . x = - (1 / ((sin . x) ^2)) ) )

proof end;

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

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 )

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;

Lm5: dom sin = REAL

by FUNCT_2:def 1;

Lm6: dom cos = REAL

by FUNCT_2:def 1;

Lm7: dom (- sin) = REAL

by FUNCT_2:def 1;

Lm8: dom exp_R = REAL

by FUNCT_2:def 1;

Lm9: dom sinh = REAL

by FUNCT_2:def 1;

Lm10: dom cosh = REAL

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 . (upper_bound A)) - (sin . (lower_bound A))

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

integral (cos,A) = 1

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

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

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

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))

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 & (- sin) | A is bounded )

proof end;

theorem Th46: :: INTEGRA8:46

for A being non empty closed_interval Subset of REAL holds integral ((- sin),A) = (cos . (upper_bound A)) - (cos . (lower_bound A))

proof end;

theorem :: INTEGRA8:47

for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds

integral ((- sin),A) = - 1

integral ((- sin),A) = - 1

proof end;

theorem :: INTEGRA8:48

for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds

integral ((- sin),A) = - 2

integral ((- sin),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 ((- sin),A) = - 1

integral ((- sin),A) = - 1

proof end;

theorem :: INTEGRA8:50

for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds

integral ((- sin),A) = 0

integral ((- sin),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 ((- sin),A) = - 2

for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds

integral ((- sin),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 ((- sin),A) = - (2 * (cos x))

for x being Real

for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds

integral ((- sin),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) = (exp_R . (upper_bound A)) - (exp_R . (lower_bound 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

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 Lm14, Lm9, INTEGRA5:10, INTEGRA5:11;

theorem Th55: :: INTEGRA8:55

for A being non empty closed_interval Subset of REAL holds integral (sinh,A) = (cosh . (upper_bound A)) - (cosh . (lower_bound A))

proof end;

theorem :: INTEGRA8:56

for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds

integral (sinh,A) = ((number_e - 1) ^2) / (2 * number_e)

integral (sinh,A) = ((number_e - 1) ^2) / (2 * number_e)

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 Lm16, Lm10, INTEGRA5:10, INTEGRA5:11;

theorem Th57: :: INTEGRA8:57

for A being non empty closed_interval Subset of REAL holds integral (cosh,A) = (sinh . (upper_bound A)) - (sinh . (lower_bound A))

proof end;

theorem :: INTEGRA8:58

for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds

integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e)

integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e)

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 . (upper_bound A)) - (tan . (lower_bound A))

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 . (upper_bound A)) - (tan . (lower_bound A))

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 . (upper_bound A)) - (cot . (lower_bound A))

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 . (upper_bound A)) - (cot . (lower_bound A))

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 / ((cosh . x) ^2) ) & f2 | A is continuous holds

integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A))

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 / ((cosh . x) ^2) ) & f2 | A is continuous holds

integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A))

proof end;

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

by FDIFF_1:def 7, SIN_COS6:83;

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) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A))

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) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound 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) = (arccos . (upper_bound A)) - (arccos . (lower_bound A))

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) = (arccos . (upper_bound A)) - (arccos . (lower_bound 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

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)

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 . (upper_bound A)) - (f . (lower_bound A))) + (g . (upper_bound A))) - (g . (lower_bound A))

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 . (upper_bound A)) - (f . (lower_bound A))) + (g . (upper_bound A))) - (g . (lower_bound A))

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 . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A)))

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 . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A)))

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 . (upper_bound A))) - (r * (f . (lower_bound A)))

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 . (upper_bound A))) - (r * (f . (lower_bound A)))

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 ((sin + cos),A) = ((((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) + (sin . (upper_bound A))) - (sin . (lower_bound A))

proof end;

theorem :: INTEGRA8:70

for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds

integral ((sin + cos),A) = 2

integral ((sin + cos),A) = 2

proof end;

theorem :: INTEGRA8:71

for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds

integral ((sin + cos),A) = 2

integral ((sin + cos),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 ((sin + cos),A) = 0

integral ((sin + cos),A) = 0

proof end;

theorem :: INTEGRA8:73

for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds

integral ((sin + cos),A) = 0

integral ((sin + cos),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 ((sin + cos),A) = 2

for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds

integral ((sin + cos),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 ((sin + cos),A) = (2 * (cos x)) - (2 * (sin x))

for x being Real

for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds

integral ((sin + cos),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 ((sinh + cosh),A) = (((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A))) - (sinh . (lower_bound A))

proof end;

theorem :: INTEGRA8:77

for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds

integral ((sinh + cosh),A) = number_e - 1

integral ((sinh + cosh),A) = number_e - 1

proof end;

theorem Th78: :: INTEGRA8:78

for A being non empty closed_interval Subset of REAL holds integral ((sin - cos),A) = (((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) - ((sin . (upper_bound A)) - (sin . (lower_bound A)))

proof end;

theorem :: INTEGRA8:79

for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds

integral ((sin - cos),A) = 0

integral ((sin - cos),A) = 0

proof end;

theorem :: INTEGRA8:80

for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds

integral ((sin - cos),A) = 2

integral ((sin - cos),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 ((sin - cos),A) = 2

integral ((sin - cos),A) = 2

proof end;

theorem :: INTEGRA8:82

for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds

integral ((sin - cos),A) = 0

integral ((sin - cos),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 ((sin - cos),A) = 2

for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds

integral ((sin - cos),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 ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x))

for x being Real

for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds

integral ((sin - cos),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 ((r (#) sin),A) = (r * ((- cos) . (upper_bound A))) - (r * ((- cos) . (lower_bound A)))

for r being Real holds integral ((r (#) sin),A) = (r * ((- cos) . (upper_bound A))) - (r * ((- cos) . (lower_bound A)))

proof end;

theorem :: INTEGRA8:86

for A being non empty closed_interval Subset of REAL

for r being Real holds integral ((r (#) cos),A) = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A)))

for r being Real holds integral ((r (#) cos),A) = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A)))

proof end;

theorem :: INTEGRA8:87

for A being non empty closed_interval Subset of REAL

for r being Real holds integral ((r (#) sinh),A) = (r * (cosh . (upper_bound A))) - (r * (cosh . (lower_bound A)))

for r being Real holds integral ((r (#) sinh),A) = (r * (cosh . (upper_bound A))) - (r * (cosh . (lower_bound A)))

proof end;

theorem :: INTEGRA8:88

for A being non empty closed_interval Subset of REAL

for r being Real holds integral ((r (#) cosh),A) = (r * (sinh . (upper_bound A))) - (r * (sinh . (lower_bound A)))

for r being Real holds integral ((r (#) cosh),A) = (r * (sinh . (upper_bound A))) - (r * (sinh . (lower_bound A)))

proof end;

theorem :: INTEGRA8:89

for A being non empty closed_interval Subset of REAL

for r being Real holds integral ((r (#) exp_R),A) = (r * (exp_R . (upper_bound A))) - (r * (exp_R . (lower_bound A)))

for r being Real holds integral ((r (#) exp_R),A) = (r * (exp_R . (upper_bound A))) - (r * (exp_R . (lower_bound A)))

proof end;

theorem Th90: :: INTEGRA8:90

for A being non empty closed_interval Subset of REAL holds integral ((sin (#) cos),A) = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A))))

proof end;

theorem :: INTEGRA8:91

for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds

integral ((sin (#) cos),A) = 1 / 2

integral ((sin (#) cos),A) = 1 / 2

proof end;

theorem :: INTEGRA8:92

for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds

integral ((sin (#) cos),A) = 0

integral ((sin (#) cos),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 ((sin (#) cos),A) = 1 / 2

integral ((sin (#) cos),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 ((sin (#) cos),A) = 0

integral ((sin (#) cos),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 ((sin (#) cos),A) = 0

for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds

integral ((sin (#) cos),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 ((sin (#) cos),A) = 0

for x being Real

for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds

integral ((sin (#) cos),A) = 0

proof end;

Lm20: for A being non empty closed_interval Subset of REAL holds

( cos (#) cos is_integrable_on A & (cos (#) cos) | A is bounded )

proof end;

theorem :: INTEGRA8:97

for A being non empty closed_interval Subset of REAL holds integral ((sin (#) sin),A) = (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral ((cos (#) cos),A))

proof end;

theorem :: INTEGRA8:98

for A being non empty closed_interval Subset of REAL holds integral ((sinh (#) sinh),A) = (((cosh . (upper_bound A)) * (sinh . (upper_bound A))) - ((cosh . (lower_bound A)) * (sinh . (lower_bound A)))) - (integral ((cosh (#) cosh),A))

proof end;

theorem :: INTEGRA8:99

for A being non empty closed_interval Subset of REAL holds integral ((sinh (#) cosh),A) = (1 / 2) * (((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A))))

proof end;

theorem :: INTEGRA8:100

for A being non empty closed_interval Subset of REAL holds integral ((exp_R (#) exp_R),A) = (1 / 2) * (((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) ^2))

proof end;

Lm21: for A being non empty closed_interval Subset of REAL holds

( exp_R (#) (sin + cos) is_integrable_on A & (exp_R (#) (sin + cos)) | A is bounded )

proof end;

Lm22: for A being non empty closed_interval Subset of REAL holds

( exp_R (#) (cos - sin) is_integrable_on A & (exp_R (#) (cos - sin)) | A is bounded )

proof end;

theorem :: INTEGRA8:101

for A being non empty closed_interval Subset of REAL holds integral ((exp_R (#) (sin + cos)),A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A))

proof end;

theorem :: INTEGRA8:102

for A being non empty closed_interval Subset of REAL holds integral ((exp_R (#) (cos - sin)),A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A))

proof end;