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

begin

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

proof end;

A: - 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;