:: Integrability Formulas -- Part {II}
:: by Bo Li , Na Ma and Xiquan Liang
::
:: 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: right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;

Lm3: ( - 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 Th7: :: 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 Th9: :: 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 Th23: :: 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 Th27: :: 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 Th31: :: 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 Th34: :: 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 Th40: :: 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 Th44: :: 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 Th50: :: 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 Th54: :: 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 Th55: :: 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;