:: Several Integrability Formulas of Special Functions -- Part {II}
:: by Bo Li , Yanping Zhuang , Yanhong Men and Xiquan Liang
::
:: Received October 14, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users

begin

Lm1: [#] REAL = dom (AffineMap ((1 / 2),0))
by FUNCT_2:def 1;

Lm2: [#] REAL = dom (sin * (AffineMap (2,0)))
by FUNCT_2:def 1;

Lm3: dom ((1 / 4) (#) (sin * (AffineMap (2,0)))) = [#] REAL
by FUNCT_2:def 1;

theorem Th1: :: INTEGR11:1

( (AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0)))) is_differentiable_on REAL & ( for x being Real holds (((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (sin . x) ^2 ) )

proof end;

theorem Th2: :: INTEGR11:2

( (AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0)))) is_differentiable_on REAL & ( for x being Real holds (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos . x) ^2 ) )

proof end;

theorem Th3: :: INTEGR11:3

for n being Element of NAT holds
( (1 / (n + 1)) (#) ((#Z (n + 1)) * sin) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x) ) )

proof end;

theorem Th4: :: INTEGR11:4

for n being Element of NAT holds
( (- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos) is_differentiable_on REAL & ( for x being Real holds (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) `| REAL) . x = ((cos . x) #Z n) * (sin . x) ) )

proof end;

theorem Th5: :: INTEGR11:5

for m, n being Element of NAT st m + n <> 0 & m - n <> 0 holds
( ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) `| REAL) . x = (cos . (m * x)) * (cos . (n * x)) ) )

proof end;

theorem Th6: :: INTEGR11:6

for m, n being Element of NAT st m + n <> 0 & m - n <> 0 holds
( ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0))))) `| REAL) . x = (sin . (m * x)) * (sin . (n * x)) ) )

proof end;

theorem Th7: :: INTEGR11:7

for m, n being Element of NAT st m + n <> 0 & m - n <> 0 holds
( (- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) is_differentiable_on REAL & ( for x being Real holds (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) `| REAL) . x = (sin . (m * x)) * (cos . (n * x)) ) )

proof end;

theorem Th8: :: INTEGR11:8

for n being Element of NAT st n <> 0 holds
( ((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) . x = x * (sin . (n * x)) ) )

proof end;

theorem Th9: :: INTEGR11:9

for n being Element of NAT st n <> 0 holds
( ((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x)) ) )

proof end;

theorem Th10: :: INTEGR11:10

( ((AffineMap (1,0)) (#) cosh) - sinh is_differentiable_on REAL & ( for x being Real holds ((((AffineMap (1,0)) (#) cosh) - sinh) `| REAL) . x = x * (sinh . x) ) )

proof end;

theorem Th11: :: INTEGR11:11

( ((AffineMap (1,0)) (#) sinh) - cosh is_differentiable_on REAL & ( for x being Real holds ((((AffineMap (1,0)) (#) sinh) - cosh) `| REAL) . x = x * (cosh . x) ) )

proof end;

theorem Th12: :: INTEGR11:12

for a, b being Real
for n being Element of NAT st a * (n + 1) <> 0 holds
( (1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b))) is_differentiable_on REAL & ( for x being Real holds (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n ) )

proof end;

begin

theorem Th13: :: INTEGR11:13

for A being closed-interval Subset of REAL holds integral ((sin ^2),A) = (((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (upper_bound A)) - (((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (lower_bound A))

proof end;

Lm4: dom (AffineMap (2,0)) = [#] REAL
by FUNCT_2:def 1;

Lm5: dom ((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) = REAL
by FUNCT_2:def 1;

theorem :: INTEGR11:14

for A being closed-interval Subset of REAL st A = [.0,PI.] holds
integral ((sin ^2),A) = PI / 2

proof end;

theorem :: INTEGR11:15

for A being closed-interval Subset of REAL st A = [.0,(2 * PI).] holds
integral ((sin ^2),A) = PI

proof end;

theorem Th16: :: INTEGR11:16

for A being closed-interval Subset of REAL holds integral ((cos ^2),A) = (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (upper_bound A)) - (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (lower_bound A))

proof end;

theorem :: INTEGR11:17

for A being closed-interval Subset of REAL st A = [.0,PI.] holds
integral ((cos ^2),A) = PI / 2

proof end;

theorem :: INTEGR11:18

for A being closed-interval Subset of REAL st A = [.0,(2 * PI).] holds
integral ((cos ^2),A) = PI

proof end;

theorem Th19: :: INTEGR11:19

for n being Element of NAT
for A being closed-interval Subset of REAL holds integral ((((#Z n) * sin) (#) cos),A) = (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) . (upper_bound A)) - (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) . (lower_bound A))

proof end;

theorem :: INTEGR11:20

for n being Element of NAT
for A being closed-interval Subset of REAL st A = [.0,PI.] holds
integral ((((#Z n) * sin) (#) cos),A) = 0

proof end;

theorem :: INTEGR11:21

for n being Element of NAT
for A being closed-interval Subset of REAL st A = [.0,(2 * PI).] holds
integral ((((#Z n) * sin) (#) cos),A) = 0

proof end;

theorem Th22: :: INTEGR11:22

for n being Element of NAT
for A being closed-interval Subset of REAL holds integral ((((#Z n) * cos) (#) sin),A) = (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . (upper_bound A)) - (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . (lower_bound A))

proof end;

theorem :: INTEGR11:23

for n being Element of NAT
for A being closed-interval Subset of REAL st A = [.0,(2 * PI).] holds
integral ((((#Z n) * cos) (#) sin),A) = 0

proof end;

theorem :: INTEGR11:24

for n being Element of NAT
for A being closed-interval Subset of REAL st A = [.(- (PI / 2)),(PI / 2).] holds
integral ((((#Z n) * cos) (#) sin),A) = 0

proof end;

theorem :: INTEGR11:25

for m, n being Element of NAT
for A being closed-interval Subset of REAL st m + n <> 0 & m - n <> 0 holds
integral (((cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0)))),A) = ((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) . (upper_bound A)) - ((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) . (lower_bound A))

proof end;

theorem :: INTEGR11:26

for m, n being Element of NAT
for A being closed-interval Subset of REAL st m + n <> 0 & m - n <> 0 holds
integral (((sin * (AffineMap (m,0))) (#) (sin * (AffineMap (n,0)))),A) = ((((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0))))) . (upper_bound A)) - ((((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0))))) . (lower_bound A))

proof end;

theorem :: INTEGR11:27

for m, n being Element of NAT
for A being closed-interval Subset of REAL st m + n <> 0 & m - n <> 0 holds
integral (((sin * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0)))),A) = (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) . (upper_bound A)) - (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0))))) . (lower_bound A))

proof end;

theorem :: INTEGR11:28

for n being Element of NAT
for A being closed-interval Subset of REAL st n <> 0 holds
integral (((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))),A) = ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (upper_bound A)) - ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (lower_bound A))

proof end;

theorem :: INTEGR11:29

for n being Element of NAT
for A being closed-interval Subset of REAL st n <> 0 holds
integral (((AffineMap (1,0)) (#) (cos * (AffineMap (n,0)))),A) = ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) . (upper_bound A)) - ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) . (lower_bound A))

proof end;

theorem :: INTEGR11:30

for A being closed-interval Subset of REAL holds integral (((AffineMap (1,0)) (#) sinh),A) = ((((AffineMap (1,0)) (#) cosh) - sinh) . (upper_bound A)) - ((((AffineMap (1,0)) (#) cosh) - sinh) . (lower_bound A))

proof end;

theorem :: INTEGR11:31

for A being closed-interval Subset of REAL holds integral (((AffineMap (1,0)) (#) cosh),A) = ((((AffineMap (1,0)) (#) sinh) - cosh) . (upper_bound A)) - ((((AffineMap (1,0)) (#) sinh) - cosh) . (lower_bound A))

proof end;

theorem :: INTEGR11:32

for a, b being Real
for n being Element of NAT
for A being closed-interval Subset of REAL st a * (n + 1) <> 0 holds
integral (((#Z n) * (AffineMap (a,b))),A) = (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (upper_bound A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) . (lower_bound A))

proof end;

begin

theorem Th33: :: INTEGR11:33

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) f) & f = #Z 2 holds
( (1 / 2) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) f) `| Z) . x = x ) )

proof end;

theorem :: INTEGR11:34

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & f = #Z 2 & Z = dom ((1 / 2) (#) f) holds
integral ((id Z),A) = (((1 / 2) (#) f) . (upper_bound A)) - (((1 / 2) (#) f) . (lower_bound A))

proof end;

theorem :: INTEGR11:35

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st not 0 in Z & A c= Z & ( for x being Real st x in Z holds
( x <> 0 & f . x = - (1 / (x ^2)) ) ) & dom f = Z & f | A is continuous holds
integral (f,A) = (((id Z) ^) . (upper_bound A)) - (((id Z) ^) . (lower_bound A))

proof end;

theorem :: INTEGR11:36

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f1, f2, f being PartFunc of REAL,REAL st A c= Z & f1 = #Z 2 & ( for x being Real st x in Z holds
( f2 . x = 1 & x <> 0 & f . x = (2 * x) / ((1 + (x ^2)) ^2) ) ) & dom (f1 / (f2 + f1)) = Z & Z = dom f & f | A is continuous holds
integral (f,A) = ((f1 / (f2 + f1)) . (upper_bound A)) - ((f1 / (f2 + f1)) . (lower_bound A))

proof end;

theorem Th37: :: INTEGR11:37

for Z being open Subset of REAL st Z c= dom (tan + sec) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( tan + sec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan + sec) `| Z) . x = 1 / (1 - (sin . x)) ) )

proof end;

theorem :: INTEGR11:38

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 & f . x = 1 / (1 - (sin . x)) ) ) & dom (tan + sec) = Z & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan + sec) . (upper_bound A)) - ((tan + sec) . (lower_bound A))

proof end;

theorem Th39: :: INTEGR11:39

for Z being open Subset of REAL st Z c= dom (tan - sec) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( tan - sec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - sec) `| Z) . x = 1 / (1 + (sin . x)) ) )

proof end;

theorem :: INTEGR11:40

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 & f . x = 1 / (1 + (sin . x)) ) ) & dom (tan - sec) = Z & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan - sec) . (upper_bound A)) - ((tan - sec) . (lower_bound A))

proof end;

theorem Th41: :: INTEGR11:41

for Z being open Subset of REAL st Z c= dom ((- cot) + cosec) & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 ) ) holds
( (- cot) + cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) + cosec) `| Z) . x = 1 / (1 + (cos . x)) ) )

proof end;

theorem :: INTEGR11:42

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 & f . x = 1 / (1 + (cos . x)) ) ) & dom ((- cot) + cosec) = Z & Z = dom f & f | A is continuous holds
integral (f,A) = (((- cot) + cosec) . (upper_bound A)) - (((- cot) + cosec) . (lower_bound A))

proof end;

theorem Th43: :: INTEGR11:43

for Z being open Subset of REAL st Z c= dom ((- cot) - cosec) & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 ) ) holds
( (- cot) - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) - cosec) `| Z) . x = 1 / (1 - (cos . x)) ) )

proof end;

theorem :: INTEGR11:44

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 & f . x = 1 / (1 - (cos . x)) ) ) & dom ((- cot) - cosec) = Z & Z = dom f & f | A is continuous holds
integral (f,A) = (((- cot) - cosec) . (upper_bound A)) - (((- cot) - cosec) . (lower_bound A))

proof end;

theorem :: INTEGR11:45

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = 1 / (1 + (x ^2)) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (arctan . (upper_bound A)) - (arctan . (lower_bound A))

proof end;

theorem :: INTEGR11:46

for r being Real
for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = r / (1 + (x ^2)) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((r (#) arctan) . (upper_bound A)) - ((r (#) arctan) . (lower_bound A))

proof end;

theorem :: INTEGR11:47

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = - (1 / (1 + (x ^2))) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (arccot . (upper_bound A)) - (arccot . (lower_bound A))

proof end;

theorem :: INTEGR11:48

for r being Real
for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = - (r / (1 + (x ^2))) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((r (#) arccot) . (upper_bound A)) - ((r (#) arccot) . (lower_bound A))

proof end;

theorem Th49: :: INTEGR11:49

for Z being open Subset of REAL st Z c= dom (((id Z) + cot) - cosec) & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 ) ) holds
( ((id Z) + cot) - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) + cot) - cosec) `| Z) . x = (cos . x) / (1 + (cos . x)) ) )

proof end;

theorem :: INTEGR11:50

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 & f . x = (cos . x) / (1 + (cos . x)) ) ) & dom (((id Z) + cot) - cosec) = Z & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) + cot) - cosec) . (upper_bound A)) - ((((id Z) + cot) - cosec) . (lower_bound A))

proof end;

theorem Th51: :: INTEGR11:51

for Z being open Subset of REAL st Z c= dom (((id Z) + cot) + cosec) & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 ) ) holds
( ((id Z) + cot) + cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) + cot) + cosec) `| Z) . x = (cos . x) / ((cos . x) - 1) ) )

proof end;

theorem :: INTEGR11:52

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 & f . x = (cos . x) / ((cos . x) - 1) ) ) & dom (((id Z) + cot) + cosec) = Z & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) + cot) + cosec) . (upper_bound A)) - ((((id Z) + cot) + cosec) . (lower_bound A))

proof end;

theorem Th53: :: INTEGR11:53

for Z being open Subset of REAL st Z c= dom (((id Z) - tan) + sec) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( ((id Z) - tan) + sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) - tan) + sec) `| Z) . x = (sin . x) / ((sin . x) + 1) ) )

proof end;

theorem :: INTEGR11:54

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 & f . x = (sin . x) / (1 + (sin . x)) ) ) & Z c= dom (((id Z) - tan) + sec) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) - tan) + sec) . (upper_bound A)) - ((((id Z) - tan) + sec) . (lower_bound A))

proof end;

theorem Th55: :: INTEGR11:55

for Z being open Subset of REAL st Z c= dom (((id Z) - tan) - sec) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( ((id Z) - tan) - sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) - tan) - sec) `| Z) . x = (sin . x) / ((sin . x) - 1) ) )

proof end;

theorem :: INTEGR11:56

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 & f . x = (sin . x) / ((sin . x) - 1) ) ) & Z c= dom (((id Z) - tan) - sec) & Z = dom f & f | A is continuous holds
integral (f,A) = ((((id Z) - tan) - sec) . (upper_bound A)) - ((((id Z) - tan) - sec) . (lower_bound A))

proof end;

theorem Th57: :: INTEGR11:57

for Z being open Subset of REAL st Z c= dom (tan - (id Z)) holds
( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2 ) )

proof end;

theorem :: INTEGR11:58

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( cos . x > 0 & f . x = (tan . x) ^2 ) ) & Z c= dom (tan - (id Z)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((tan - (id Z)) . (upper_bound A)) - ((tan - (id Z)) . (lower_bound A))

proof end;

theorem Th59: :: INTEGR11:59

for Z being open Subset of REAL st Z c= dom ((- cot) - (id Z)) holds
( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) - (id Z)) `| Z) . x = (cot . x) ^2 ) )

proof end;

theorem :: INTEGR11:60

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( sin . x > 0 & f . x = (cot . x) ^2 ) ) & Z c= dom ((- cot) - (id Z)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((- cot) - (id Z)) . (upper_bound A)) - (((- cot) - (id Z)) . (lower_bound A))

proof end;

theorem :: INTEGR11:61

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = 1 / ((cos . x) ^2) & cos . x <> 0 ) ) & dom tan = Z & Z = dom f & f | A is continuous holds
integral (f,A) = (tan . (upper_bound A)) - (tan . (lower_bound A))

proof end;

theorem :: INTEGR11:62

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = - (1 / ((sin . x) ^2)) & sin . x <> 0 ) ) & dom cot = Z & Z = dom f & f | A is continuous holds
integral (f,A) = (cot . (upper_bound A)) - (cot . (lower_bound A))

proof end;

theorem :: INTEGR11:63

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
f . x = ((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) ) & Z c= dom (sec - (id Z)) & Z = dom f & f | A is continuous holds
integral (f,A) = ((sec - (id Z)) . (upper_bound A)) - ((sec - (id Z)) . (lower_bound A))

proof end;

theorem :: INTEGR11:64

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
f . x = ((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) ) & Z c= dom ((- cosec) - (id Z)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((- cosec) - (id Z)) . (upper_bound A)) - (((- cosec) - (id Z)) . (lower_bound A))

proof end;

theorem :: INTEGR11:65

for A being closed-interval Subset of REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
sin . x > 0 ) & Z c= dom (ln * sin) & Z = dom cot & cot | A is continuous holds
integral (cot,A) = ((ln * sin) . (upper_bound A)) - ((ln * sin) . (lower_bound A))

proof end;

theorem :: INTEGR11:66

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = (arcsin . x) / (sqrt (1 - (x ^2))) ) & Z c= dom ((1 / 2) (#) ((#Z 2) * arcsin)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / 2) (#) ((#Z 2) * arcsin)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arcsin)) . (lower_bound A))

proof end;

theorem :: INTEGR11:67

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = - ((arccos . x) / (sqrt (1 - (x ^2)))) ) & Z c= dom ((1 / 2) (#) ((#Z 2) * arccos)) & Z = dom f & f | A is continuous holds
integral (f,A) = (((1 / 2) (#) ((#Z 2) * arccos)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccos)) . (lower_bound A))

proof end;

theorem :: INTEGR11:68

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st A c= Z & 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 ) ) & dom arcsin = Z & Z c= dom (((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) holds
integral (arcsin,A) = ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (lower_bound A))

proof end;

theorem :: INTEGR11:69

for a being Real
for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f, f1, f2, f3 being PartFunc of REAL,REAL st A c= Z & 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 ) ) & dom (arcsin * f3) = Z & Z c= dom (((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) & (arcsin * f3) | A is continuous holds
integral ((arcsin * f3),A) = ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) . (lower_bound A))

proof end;

theorem :: INTEGR11:70

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st A c= Z & 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 ) ) & dom arccos = Z & Z c= dom (((id Z) (#) arccos) - ((#R (1 / 2)) * f)) holds
integral (arccos,A) = ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) . (lower_bound A))

proof end;

theorem :: INTEGR11:71

for a being Real
for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f, f1, f2, f3 being PartFunc of REAL,REAL st A c= Z & 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 ) ) & dom (arccos * f3) = Z & Z = dom (((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) & (arccos * f3) | A is continuous holds
integral ((arccos * f3),A) = ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) . (lower_bound A))

proof end;

theorem :: INTEGR11:72

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f2, f1 being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom arctan & Z = dom (((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2)))) holds
integral (arctan,A) = ((((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2)))) . (upper_bound A)) - ((((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2)))) . (lower_bound A))

proof end;

theorem :: INTEGR11:73

for A being closed-interval Subset of REAL
for Z being open Subset of REAL
for f2, f1 being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) & dom arccot = Z & Z = dom (((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2)))) holds
integral (arccot,A) = ((((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2)))) . (upper_bound A)) - ((((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2)))) . (lower_bound A))

proof end;