:: Integrability Formulas -- Part {III}
:: by Bo Li and Na Ma
::
:: Received February 4, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users

begin

Lm1: for Z being open Subset of REAL st 0 in Z holds
(id Z) " {0} = {0}

proof end;

Lm2: - 1 is Real
by XREAL_0:def 1;

theorem Th1: :: INTEGR14:1

for Z being open Subset of REAL st Z c= dom (sec * ((id Z) ^)) holds
( - (sec * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) )

proof end;

theorem Th2: :: INTEGR14:2

for Z being open Subset of REAL st Z c= dom (cosec * exp_R) holds
( - (cosec * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) )

proof end;

theorem Th3: :: INTEGR14:3

for Z being open Subset of REAL st Z c= dom (cosec * ln) holds
( - (cosec * ln) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) )

proof end;

theorem Th4: :: INTEGR14:4

for Z being open Subset of REAL st Z c= dom (exp_R * cosec) holds
( - (exp_R * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) )

proof end;

theorem Th5: :: INTEGR14:5

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

proof end;

theorem Th6: :: INTEGR14:6

for n being Nat
for Z being open Subset of REAL st Z c= dom ((#Z n) * cosec) & 1 <= n holds
( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) )

proof end;

theorem Th7: :: INTEGR14:7

for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) sec) holds
( - (((id Z) ^) (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) )

proof end;

theorem Th8: :: INTEGR14:8

for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) cosec) holds
( - (((id Z) ^) (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) )

proof end;

theorem Th9: :: INTEGR14:9

for Z being open Subset of REAL st Z c= dom (cosec * sin) holds
( - (cosec * sin) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) )

proof end;

theorem Th10: :: INTEGR14:10

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

proof end;

theorem Th11: :: INTEGR14:11

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

proof end;

theorem Th12: :: INTEGR14:12

for Z being open Subset of REAL st Z c= dom (cot (#) sec) holds
( - (cot (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) )

proof end;

theorem Th13: :: INTEGR14:13

for Z being open Subset of REAL st Z c= dom (cot (#) cosec) holds
( - (cot (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) )

proof end;

theorem Th14: :: INTEGR14:14

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

proof end;

begin

theorem :: INTEGR14:15

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / 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 :: INTEGR14:16

for A being closed-interval Subset of REAL
for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / 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 :: INTEGR14:17

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

proof end;

theorem :: INTEGR14:18

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

proof end;

theorem :: INTEGR14:19

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

proof end;

theorem :: INTEGR14:20

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

proof end;

theorem :: INTEGR14:21

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

proof end;

theorem :: INTEGR14:22

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

proof end;

theorem :: INTEGR14:23

for A being closed-interval Subset of REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (ln * sec) & Z = dom tan & tan | A is continuous holds
integral (tan,A) = ((ln * sec) . (upper_bound A)) - ((ln * sec) . (lower_bound A))

proof end;

theorem :: INTEGR14:24

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

proof end;

theorem :: INTEGR14:25

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

proof end;

theorem :: INTEGR14:26

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

proof end;

theorem :: INTEGR14:27

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

proof end;

theorem :: INTEGR14:28

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

proof end;

theorem :: INTEGR14:29

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

proof end;

theorem :: INTEGR14:30

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

proof end;

theorem :: INTEGR14:31

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

proof end;

theorem :: INTEGR14:32

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

proof end;

theorem :: INTEGR14:33

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

proof end;

theorem :: INTEGR14:34

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

proof end;

theorem :: INTEGR14:35

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

proof end;

theorem :: INTEGR14:36

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

proof end;

theorem :: INTEGR14:37

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

proof end;

theorem :: INTEGR14:38

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

proof end;

theorem :: INTEGR14:39

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

proof end;

theorem :: INTEGR14:40

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

proof end;

theorem :: INTEGR14:41

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

proof end;

theorem :: INTEGR14:42

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

proof end;

theorem :: INTEGR14:43

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

proof end;

theorem :: INTEGR14:44

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

proof end;

theorem :: INTEGR14:45

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

proof end;

theorem :: INTEGR14:46

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

proof end;

theorem :: INTEGR14:47

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

proof end;

theorem :: INTEGR14:48

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

proof end;

theorem :: INTEGR14:49

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

proof end;

theorem :: INTEGR14:50

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

proof end;

theorem :: INTEGR14:51

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

proof end;

theorem :: INTEGR14:52

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

proof end;

theorem :: INTEGR14:53

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

proof end;

theorem :: INTEGR14:54

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

proof end;

theorem :: INTEGR14:55

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

proof end;

theorem :: INTEGR14:56

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

proof end;

theorem :: INTEGR14:57

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

proof end;

theorem :: INTEGR14:58

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

proof end;

theorem :: INTEGR14:59

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

proof end;