:: Integrability Formulas -- Part {II}
:: by Bo Li , Na Ma and Xiquan Liang
::
:: 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;

Lm1: right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;

A: ( - 1 is Real & - (1 / 2) is Real & 1 / 2 is Real )
by XREAL_0:def 1;

theorem :: INTEGR13:1

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 = (sin (#) cos ) ^ & Z c= dom (ln * tan ) & Z = dom f & f | A is continuous holds
integral f,A = ((ln * tan ) . (upper_bound A)) - ((ln * tan ) . (lower_bound A))

proof end;

theorem :: INTEGR13:2

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 = - ((sin (#) cos ) ^ ) & Z c= dom (ln * cot ) & Z = dom f & f | A is continuous holds
integral f,A = ((ln * cot ) . (upper_bound A)) - ((ln * cot ) . (lower_bound A))

proof end;

theorem :: INTEGR13:3

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 = 2 (#) (exp_R (#) sin ) & Z c= dom (exp_R (#) (sin - cos )) & Z = dom f & f | A is continuous holds
integral f,A = ((exp_R (#) (sin - cos )) . (upper_bound A)) - ((exp_R (#) (sin - cos )) . (lower_bound A))

proof end;

theorem :: INTEGR13:4

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 = 2 (#) (exp_R (#) cos ) & Z c= dom (exp_R (#) (sin + cos )) & Z = dom f & f | A is continuous holds
integral f,A = ((exp_R (#) (sin + cos )) . (upper_bound A)) - ((exp_R (#) (sin + cos )) . (lower_bound A))

proof end;

theorem :: INTEGR13:5

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

proof end;

theorem :: INTEGR13:6

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

proof end;

theorem Th1: :: INTEGR13:7

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

proof end;

theorem :: INTEGR13:8

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 = sin / exp_R & Z c= dom ((- (1 / 2)) (#) ((sin + cos ) / exp_R )) & Z = dom f & f | A is continuous holds
integral f,A = (((- (1 / 2)) (#) ((sin + cos ) / exp_R )) . (upper_bound A)) - (((- (1 / 2)) (#) ((sin + cos ) / exp_R )) . (lower_bound A))

proof end;

theorem Th2: :: INTEGR13:9

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

proof end;

theorem :: INTEGR13:10

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 = cos / exp_R & Z c= dom ((1 / 2) (#) ((sin - cos ) / exp_R )) & Z = dom f & f | A is continuous holds
integral f,A = (((1 / 2) (#) ((sin - cos ) / exp_R )) . (upper_bound A)) - (((1 / 2) (#) ((sin - cos ) / exp_R )) . (lower_bound A))

proof end;

theorem :: INTEGR13:11

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 (#) (sin + cos ) & Z c= dom (exp_R (#) sin ) & Z = dom f & f | A is continuous holds
integral f,A = ((exp_R (#) sin ) . (upper_bound A)) - ((exp_R (#) sin ) . (lower_bound A))

proof end;

theorem :: INTEGR13:12

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 (#) (cos - sin ) & Z c= dom (exp_R (#) cos ) & Z = dom f & f | A is continuous holds
integral f,A = ((exp_R (#) cos ) . (upper_bound A)) - ((exp_R (#) cos ) . (lower_bound A))

proof end;

theorem :: INTEGR13:13

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

proof end;

theorem :: INTEGR13:14

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 & f = (- ((cos / sin ) / f1)) - (((id Z) ^ ) / (sin ^2 )) & f1 = #Z 2 & Z c= dom (((id Z) ^ ) (#) cot ) & Z = dom f & f | A is continuous holds
integral f,A = ((((id Z) ^ ) (#) cot ) . (upper_bound A)) - ((((id Z) ^ ) (#) cot ) . (lower_bound A))

proof end;

theorem :: INTEGR13: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 & f = ((sin / cos ) / (id Z)) + (ln / (cos ^2 )) & Z c= dom (ln (#) tan ) & Z = dom f & f | A is continuous holds
integral f,A = ((ln (#) tan ) . (upper_bound A)) - ((ln (#) tan ) . (lower_bound A))

proof end;

theorem :: INTEGR13: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 & f = ((cos / sin ) / (id Z)) - (ln / (sin ^2 )) & Z c= dom (ln (#) cot ) & Z = dom f & f | A is continuous holds
integral f,A = ((ln (#) cot ) . (upper_bound A)) - ((ln (#) cot ) . (lower_bound A))

proof end;

theorem :: INTEGR13: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 & f = (tan / (id Z)) + (ln / (cos ^2 )) & Z c= dom (ln (#) tan ) & Z c= dom tan & Z = dom f & f | A is continuous holds
integral f,A = ((ln (#) tan ) . (upper_bound A)) - ((ln (#) tan ) . (lower_bound A))

proof end;

theorem :: INTEGR13: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 & f = (cot / (id Z)) - (ln / (sin ^2 )) & Z c= dom (ln (#) cot ) & Z c= dom cot & Z = dom f & f | A is continuous holds
integral f,A = ((ln (#) cot ) . (upper_bound A)) - ((ln (#) cot ) . (lower_bound A))

proof end;

theorem :: INTEGR13:19

for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = (arctan / (id Z)) + (ln / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral f,A = ((ln (#) arctan ) . (upper_bound A)) - ((ln (#) arctan ) . (lower_bound A))

proof end;

theorem :: INTEGR13:20

for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = (arccot / (id Z)) - (ln / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral f,A = ((ln (#) arccot ) . (upper_bound A)) - ((ln (#) arccot ) . (lower_bound A))

proof end;

theorem :: INTEGR13: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 * tan ) / (cos ^2 ) & Z = dom f & f | A is continuous holds
integral f,A = ((exp_R * tan ) . (upper_bound A)) - ((exp_R * tan ) . (lower_bound A))

proof end;

theorem :: INTEGR13: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 * cot ) / (sin ^2 )) & Z = dom f & f | A is continuous holds
integral f,A = ((exp_R * cot ) . (upper_bound A)) - ((exp_R * cot ) . (lower_bound A))

proof end;

theorem Th3: :: INTEGR13:23

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

proof end;

theorem :: INTEGR13:24

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 * cot ) / (sin ^2 ) & Z = dom f & f | A is continuous holds
integral f,A = ((- (exp_R * cot )) . (upper_bound A)) - ((- (exp_R * cot )) . (lower_bound A))

proof end;

theorem :: INTEGR13:25

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 = ((id Z) (#) ((cos * ln ) ^2 )) ^ & Z c= dom (tan * ln ) & Z = dom f & f | A is continuous holds
integral f,A = ((tan * ln ) . (upper_bound A)) - ((tan * ln ) . (lower_bound A))

proof end;

theorem :: INTEGR13:26

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 = - (((id Z) (#) ((sin * ln ) ^2 )) ^ ) & Z c= dom (cot * ln ) & Z = dom f & f | A is continuous holds
integral f,A = ((cot * ln ) . (upper_bound A)) - ((cot * ln ) . (lower_bound A))

proof end;

theorem Th4: :: INTEGR13:27

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

proof end;

theorem :: INTEGR13: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 & f = ((id Z) (#) ((sin * ln ) ^2 )) ^ & Z c= dom (cot * ln ) & Z = dom f & f | A is continuous holds
integral f,A = ((- (cot * ln )) . (upper_bound A)) - ((- (cot * ln )) . (lower_bound A))

proof end;

theorem :: INTEGR13: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 & f = exp_R / ((cos * exp_R ) ^2 ) & Z c= dom (tan * exp_R ) & Z = dom f & f | A is continuous holds
integral f,A = ((tan * exp_R ) . (upper_bound A)) - ((tan * exp_R ) . (lower_bound A))

proof end;

theorem :: INTEGR13:30

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 / ((sin * exp_R ) ^2 )) & Z c= dom (cot * exp_R ) & Z = dom f & f | A is continuous holds
integral f,A = ((cot * exp_R ) . (upper_bound A)) - ((cot * exp_R ) . (lower_bound A))

proof end;

theorem Th5: :: INTEGR13:31

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

proof end;

theorem :: INTEGR13: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 & f = exp_R / ((sin * exp_R ) ^2 ) & Z c= dom (cot * exp_R ) & Z = dom f & f | A is continuous holds
integral f,A = ((- (cot * exp_R )) . (upper_bound A)) - ((- (cot * exp_R )) . (lower_bound A))

proof end;

theorem :: INTEGR13: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 / ((x ^2 ) * ((cos . (1 / 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 Th6: :: INTEGR13:34

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 = 1 / ((x ^2 ) * ((cos . (1 / x)) ^2 )) ) )

proof end;

theorem :: INTEGR13: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 / ((x ^2 ) * ((cos . (1 / 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 :: INTEGR13: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 = 1 / ((x ^2 ) * ((sin . (1 / 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 :: INTEGR13:37

for A being closed-interval Subset of REAL
for f1, 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
( f1 . x = 1 & arctan . x > 0 ) ) & f = ((f1 + (#Z 2)) (#) arctan ) ^ & Z c= ].(- 1),1.[ & Z c= dom (ln * arctan ) & Z = dom f & f | A is continuous holds
integral f,A = ((ln * arctan ) . (upper_bound A)) - ((ln * arctan ) . (lower_bound A))

proof end;

theorem :: INTEGR13:38

for n being Element of NAT
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 & f = n (#) (((#Z (n - 1)) * arctan ) / (f1 + (#Z 2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z c= dom ((#Z n) * arctan ) & Z = dom f & f | A is continuous holds
integral f,A = (((#Z n) * arctan ) . (upper_bound A)) - (((#Z n) * arctan ) . (lower_bound A))

proof end;

theorem :: INTEGR13:39

for n being Element of NAT
for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = - (n (#) (((#Z (n - 1)) * arccot ) / (f1 + (#Z 2)))) & Z c= ].(- 1),1.[ & Z c= dom ((#Z n) * arccot ) & Z = dom f & f | A is continuous holds
integral f,A = (((#Z n) * arccot ) . (upper_bound A)) - (((#Z n) * arccot ) . (lower_bound A))

proof end;

theorem Th7: :: INTEGR13:40

for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((#Z n) * arccot ) & Z c= ].(- 1),1.[ holds
( - ((#Z n) * arccot ) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * arccot )) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2 )) ) )

proof end;

theorem :: INTEGR13:41

for n being Element of NAT
for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = n (#) (((#Z (n - 1)) * arccot ) / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z c= dom ((#Z n) * arccot ) & Z = dom f & f | A is continuous holds
integral f,A = ((- ((#Z n) * arccot )) . (upper_bound A)) - ((- ((#Z n) * arccot )) . (lower_bound A))

proof end;

theorem :: INTEGR13:42

for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = arctan / (f1 + (#Z 2)) & Z c= ].(- 1),1.[ & Z c= dom ((#Z 2) * arctan ) & Z = dom f & f | A is continuous holds
integral f,A = (((1 / 2) (#) ((#Z 2) * arctan )) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arctan )) . (lower_bound A))

proof end;

theorem :: INTEGR13:43

for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = - (arccot / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z c= dom ((#Z 2) * arccot ) & Z = dom f & f | A is continuous holds
integral f,A = (((1 / 2) (#) ((#Z 2) * arccot )) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccot )) . (lower_bound A))

proof end;

theorem Th8: :: INTEGR13:44

for Z being open Subset of REAL st Z c= dom ((#Z 2) * arccot ) & Z c= ].(- 1),1.[ holds
( - ((1 / 2) (#) ((#Z 2) * arccot )) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((1 / 2) (#) ((#Z 2) * arccot ))) `| Z) . x = (arccot . x) / (1 + (x ^2 )) ) )

proof end;

theorem :: INTEGR13:45

for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = arccot / (f1 + (#Z 2)) & Z c= ].(- 1),1.[ & Z c= dom ((#Z 2) * arccot ) & Z = dom f & f | A is continuous holds
integral f,A = ((- ((1 / 2) (#) ((#Z 2) * arccot ))) . (upper_bound A)) - ((- ((1 / 2) (#) ((#Z 2) * arccot ))) . (lower_bound A))

proof end;

theorem :: INTEGR13:46

for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = arctan + ((id Z) / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral f,A = (((id Z) (#) arctan ) . (upper_bound A)) - (((id Z) (#) arctan ) . (lower_bound A))

proof end;

theorem :: INTEGR13:47

for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = arccot - ((id Z) / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral f,A = (((id Z) (#) arccot ) . (upper_bound A)) - (((id Z) (#) arccot ) . (lower_bound A))

proof end;

theorem :: INTEGR13:48

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 & Z c= ].(- 1),1.[ & f = (exp_R * arctan ) / (f1 + (#Z 2)) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous holds
integral f,A = ((exp_R * arctan ) . (upper_bound A)) - ((exp_R * arctan ) . (lower_bound A))

proof end;

theorem :: INTEGR13:49

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 & Z c= ].(- 1),1.[ & f = - ((exp_R * arccot ) / (f1 + (#Z 2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous holds
integral f,A = ((exp_R * arccot ) . (upper_bound A)) - ((exp_R * arccot ) . (lower_bound A))

proof end;

theorem Th9: :: INTEGR13:50

for Z being open Subset of REAL st Z c= dom (exp_R * arccot ) & Z c= ].(- 1),1.[ holds
( - (exp_R * arccot ) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * arccot )) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2 )) ) )

proof end;

theorem :: INTEGR13:51

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 & Z c= ].(- 1),1.[ & f = (exp_R * arccot ) / (f1 + (#Z 2)) & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & f | A is continuous holds
integral f,A = ((- (exp_R * arccot )) . (upper_bound A)) - ((- (exp_R * arccot )) . (lower_bound A))

proof end;

theorem :: INTEGR13:52

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

proof end;

theorem :: INTEGR13:53

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

proof end;

theorem Th10: :: INTEGR13:54

for Z being open Subset of REAL st Z c= dom (((id Z) ^ ) (#) arctan ) & Z c= ].(- 1),1.[ holds
( - (((id Z) ^ ) (#) arctan ) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^ ) (#) arctan )) `| Z) . x = ((arctan . x) / (x ^2 )) - (1 / (x * (1 + (x ^2 )))) ) )

proof end;

theorem Th11: :: INTEGR13:55

for Z being open Subset of REAL st Z c= dom (((id Z) ^ ) (#) arccot ) & Z c= ].(- 1),1.[ holds
( - (((id Z) ^ ) (#) arccot ) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (((id Z) ^ ) (#) arccot )) `| Z) . x = ((arccot . x) / (x ^2 )) + (1 / (x * (1 + (x ^2 )))) ) )

proof end;

theorem :: INTEGR13:56

for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = (arctan / (#Z 2)) - (((id Z) (#) (f1 + (#Z 2))) ^ ) & Z c= dom (((id Z) ^ ) (#) arctan ) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral f,A = ((- (((id Z) ^ ) (#) arctan )) . (upper_bound A)) - ((- (((id Z) ^ ) (#) arctan )) . (lower_bound A))

proof end;

theorem :: INTEGR13:57

for A being closed-interval Subset of REAL
for f1, 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
f1 . x = 1 ) & f = (arccot / (#Z 2)) + (((id Z) (#) (f1 + (#Z 2))) ^ ) & Z c= dom (((id Z) ^ ) (#) arccot ) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds
integral f,A = ((- (((id Z) ^ ) (#) arccot )) . (upper_bound A)) - ((- (((id Z) ^ ) (#) arccot )) . (lower_bound A))

proof end;