:: 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 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 )))) . (sup A)) - (((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) . (inf 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 )))) . (sup A)) - (((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) . (inf 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 )) . (sup A)) - (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin )) . (inf 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 )) . (sup A)) - (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) . (inf 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 )))) . (sup A)) - ((((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 )))) . (inf 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 )))) . (sup A)) - ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) . (inf 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 )))) . (sup A)) - (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 )))) . (inf 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 )))) . (sup A)) - ((((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 )))) . (inf 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 )))) . (sup A)) - ((((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) + ((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 )))) . (inf 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 ) . (sup A)) - ((((AffineMap 1,0 ) (#) cosh ) - sinh ) . (inf 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 ) . (sup A)) - ((((AffineMap 1,0 ) (#) sinh ) - cosh ) . (inf 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))) . (sup A)) - (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) . (inf 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) . (sup A)) - (((1 / 2) (#) f) . (inf 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) ^ ) . (sup A)) - (((id Z) ^ ) . (inf 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)) . (sup A)) - ((f1 / (f2 + f1)) . (inf 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 ) . (sup A)) - ((tan + sec ) . (inf 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 ) . (sup A)) - ((tan - sec ) . (inf 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 ) . (sup A)) - (((- cot ) + cosec ) . (inf 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 ) . (sup A)) - (((- cot ) - cosec ) . (inf 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 . (sup A)) - (arctan . (inf 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 ) . (sup A)) - ((r (#) arctan ) . (inf 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 . (sup A)) - (arccot . (inf 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 ) . (sup A)) - ((r (#) arccot ) . (inf 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 ) . (sup A)) - ((((id Z) + cot ) - cosec ) . (inf 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 ) . (sup A)) - ((((id Z) + cot ) + cosec ) . (inf 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 ) . (sup A)) - ((((id Z) - tan ) + sec ) . (inf 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 ) . (sup A)) - ((((id Z) - tan ) - sec ) . (inf 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)) . (sup A)) - ((tan - (id Z)) . (inf 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)) . (sup A)) - (((- cot ) - (id Z)) . (inf 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 . (sup A)) - (tan . (inf 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 . (sup A)) - (cot . (inf 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)) . (sup A)) - ((sec - (id Z)) . (inf 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)) . (sup A)) - (((- cosec ) - (id Z)) . (inf 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 ) . (sup A)) - ((ln * sin ) . (inf 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 )) . (sup A)) - (((1 / 2) (#) ((#Z 2) * arcsin )) . (inf 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 )) . (sup A)) - (((1 / 2) (#) ((#Z 2) * arccos )) . (inf 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)) . (sup A)) - ((((id Z) (#) arcsin ) + ((#R (1 / 2)) * f)) . (inf 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)) . (sup A)) - ((((id Z) (#) (arcsin * f3)) + ((#R (1 / 2)) * f)) . (inf 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)) . (sup A)) - ((((id Z) (#) arccos ) - ((#R (1 / 2)) * f)) . (inf 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)) . (sup A)) - ((((id Z) (#) (arccos * f3)) - ((#R (1 / 2)) * f)) . (inf 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)))) . (sup A)) - ((((id Z) (#) arctan ) - ((1 / 2) (#) (ln * (f1 + f2)))) . (inf 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)))) . (sup A)) - ((((id Z) (#) arccot ) + ((1 / 2) (#) (ln * (f1 + f2)))) . (inf A))

proof end;