:: Several Integrability Formulas of Some Functions, Orthogonal Polynomials and Norm Functions
:: by Bo Li , Yanping Zhuang , Bing Xie and Pan Wang
::
:: Received October 14, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users

Lm1: dom (- (exp_R * (AffineMap ((- 1),0)))) = [#] REAL
by FUNCT_2:def 1;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem :: INTEGRA9:1

( - (exp_R * (AffineMap ((- 1),0))) is_differentiable_on REAL & ( for x being Real holds ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ) )

proof end;

:: f.x = (1/r)*exp_R.(r*x)

theorem Th2: :: INTEGRA9:2

for r being Real st r <> 0 holds
( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) )

proof end;

:: f.x = exp_R.(r*x)

theorem :: INTEGRA9:3

for r being Real
for A being non empty closed_interval Subset of REAL st r <> 0 holds
integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A))

proof end;

:: f.x=(-1/n)*cos(n*x)

theorem Th4: :: INTEGRA9:4

for n being Element of NAT st n <> 0 holds
( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) )

proof end;

:: f.x=sin(n*x)

theorem :: INTEGRA9:5

for n being Element of NAT
for A being non empty closed_interval Subset of REAL st n <> 0 holds
integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A))

proof end;

:: f.x=(1/n)*sin(n*x)

theorem Th6: :: INTEGRA9:6

for n being Element of NAT st n <> 0 holds
( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) )

proof end;

:: f.x=cos(n*x)

theorem :: INTEGRA9:7

for n being Element of NAT
for A being non empty closed_interval Subset of REAL st n <> 0 holds
integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A))

proof end;

:: f.x=x*sin.x

theorem :: INTEGRA9:8

for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A))

proof end;

:: f.x=x*cos.x

theorem :: INTEGRA9:9

for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A))

proof end;

:: f.x=x*cos.x

theorem Th10: :: INTEGRA9:10

for Z being open Subset of REAL holds
( (id Z) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) ) )

proof end;

Lm2: for x being Real holds
( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) )

proof end;

:: f.x = -sin.x+x*cos.x

theorem Th11: :: INTEGRA9:11

for Z being open Subset of REAL holds
( (- sin) + ((id Z) (#) cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) ) )

proof end;

:: f.x=-x*sin.x

theorem :: INTEGRA9:12

for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A))

proof end;

:: f.x = -cos.x-x*sin.x

theorem Th13: :: INTEGRA9:13

for Z being open Subset of REAL holds
( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) )

proof end;

:: f.x = -x*cos.x

theorem :: INTEGRA9:14

for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A))

proof end;

:: f.x=sin.x+x*cos.x

theorem :: INTEGRA9:15

for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A))

proof end;

:: f.x=-cos.x+x*sin.x

theorem :: INTEGRA9:16

for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z holds
integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A))

proof end;

:: f.x = x*(exp_R.x)

theorem :: INTEGRA9:17

for A being non empty closed_interval Subset of REAL holds integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A))

proof end;

:: f.x = (1/(n+1))*x^(n+1)

theorem Th18: :: INTEGRA9:18

for n being Element of NAT holds
( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ) )

proof end;

:: f.x = x^n

theorem :: INTEGRA9:19

for n being Element of NAT
for A being non empty closed_interval Subset of REAL holds integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1)))

proof end;

theorem Th20: :: INTEGRA9:20

for f, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds (f - g) || C = (f || C) - (g || C)

proof end;

theorem Th21: :: INTEGRA9:21

for f1, f2, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C

proof end;

theorem Th22: :: INTEGRA9:22

for f1, f2, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds ((f1 - f2) || C) (#) (g || C) = ((f1 (#) g) - (f2 (#) g)) || C

proof end;

theorem :: INTEGRA9:23

for f1, f2, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C)

proof end;

definition

let A be non empty closed_interval Subset of REAL;
let f, g be PartFunc of REAL,REAL;

func |||(f,g,A)||| -> Real equals :: INTEGRA9:def 1
integral ((f (#) g),A);

correctness
coherence
integral ((f (#) g),A) is Real;
;

end;

:: deftheorem defines |||( INTEGRA9:def 1 :
for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL holds |||(f,g,A)||| = integral ((f (#) g),A);

theorem :: INTEGRA9:24

for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL holds |||(f,g,A)||| = |||(g,f,A)||| ;

theorem :: INTEGRA9:25

for f1, f2, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable holds
|||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)|||

proof end;

theorem :: INTEGRA9:26

for f1, f2, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable holds
|||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)|||

proof end;

theorem :: INTEGRA9:27

for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds
|||((- f),g,A)||| = - |||(f,g,A)|||

proof end;

theorem :: INTEGRA9:28

for r being Real
for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds
|||((r (#) f),g,A)||| = r * |||(f,g,A)|||

proof end;

theorem :: INTEGRA9:29

for r, p being Real
for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds
|||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)|||

proof end;

theorem :: INTEGRA9:30

for f, g, h being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL holds |||((f (#) g),h,A)||| = |||(f,(g (#) h),A)||| by RFUNCT_1:9;

theorem Th31: :: INTEGRA9:31

for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A holds
|||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)|||

proof end;

definition

let A be non empty closed_interval Subset of REAL;
let f, g be PartFunc of REAL,REAL;

pred f is_orthogonal_with g,A means :: INTEGRA9:def 2
|||(f,g,A)||| = 0 ;

end;

:: deftheorem defines is_orthogonal_with INTEGRA9:def 2 :
for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL holds
( f is_orthogonal_with g,A iff |||(f,g,A)||| = 0 );

theorem Th32: :: INTEGRA9:32

for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A holds
|||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)|||

proof end;

theorem :: INTEGRA9:33

for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & (f (#) f) || A is integrable & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
|||(f,f,A)||| >= 0 by INTEGRA2:32;

theorem :: INTEGRA9:34

for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds
sin is_orthogonal_with cos ,A by INTEGRA8:92;

theorem :: INTEGRA9:35

for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds
sin is_orthogonal_with cos ,A by INTEGRA8:94;

theorem :: INTEGRA9:36

for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
sin is_orthogonal_with cos ,A by INTEGRA8:95;

theorem :: INTEGRA9:37

for x being Real
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
sin is_orthogonal_with cos ,A by INTEGRA8:96;

theorem :: INTEGRA9:38

for A being non empty closed_interval Subset of REAL st A = [.(- PI),PI.] holds
sin is_orthogonal_with cos ,A

proof end;

theorem :: INTEGRA9:39

for A being non empty closed_interval Subset of REAL st A = [.(- (PI / 2)),(PI / 2).] holds
sin is_orthogonal_with cos ,A

proof end;

theorem :: INTEGRA9:40

for A being non empty closed_interval Subset of REAL st A = [.(- (2 * PI)),(2 * PI).] holds
sin is_orthogonal_with cos ,A

proof end;

theorem :: INTEGRA9:41

for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(- ((2 * n) * PI)),((2 * n) * PI).] holds
sin is_orthogonal_with cos ,A

proof end;

theorem :: INTEGRA9:42

for x being Real
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds
sin is_orthogonal_with cos ,A

proof end;

definition

let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;

func ||..f,A..|| -> Real equals :: INTEGRA9:def 3
sqrt |||(f,f,A)|||;

correctness
coherence
sqrt |||(f,f,A)||| is Real;
;

end;

:: deftheorem defines ||.. INTEGRA9:def 3 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL holds ||..f,A..|| = sqrt |||(f,f,A)|||;

theorem :: INTEGRA9:43

for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) holds
0 <= ||..f,A..||

proof end;

theorem :: INTEGRA9:44

for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL holds ||..(1 (#) f),A..|| = ||..f,A..|| by RFUNCT_1:21;

theorem :: INTEGRA9:45

for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A & ( for x being Real st x in A holds
((f (#) f) || A) . x >= 0 ) & ( for x being Real st x in A holds
((g (#) g) || A) . x >= 0 ) holds
||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2)

proof end;

:: f.x = 1/(a+x)

theorem :: INTEGRA9:46

for a being Real
for A being non empty closed_interval Subset of REAL st not - a in A holds
((AffineMap (1,a)) ^) | A is continuous

proof end;

:: f.x=-1/(a+x)^2

theorem :: INTEGRA9:47

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))

proof end;

:: f.x=1/(a+x)^2

theorem :: INTEGRA9:48

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A))

proof end;

:: f.x=1/(a-x)^2

theorem :: INTEGRA9:49

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds
integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A))

proof end;

:: f.x=1/(a+x)

theorem :: INTEGRA9:50

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a + x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))

proof end;

:: f.x=1/(x-a)

theorem :: INTEGRA9:51

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (x - a) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A))

proof end;

:: f.x=1/(a-x)

theorem :: INTEGRA9:52

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = 1 / (a - x) ) & f2 | A is continuous holds
integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A))

proof end;

:: f.x= x/(a+x)

theorem :: INTEGRA9:53

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

proof end;

:: f.x= (a-x)/(a+x)

theorem :: INTEGRA9:54

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

proof end;

:: f.x= (x-a)/(x+a)

theorem :: INTEGRA9:55

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

proof end;

:: f.x= (x+a)/(x-a)

theorem :: INTEGRA9:56

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

proof end;

:: f.x= (x+a)/(x+b)

theorem :: INTEGRA9:57

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

proof end;

:: f.x= (x+a)/(x-b)

theorem :: INTEGRA9:58

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

proof end;

:: f.x= (x-a)/(x+b)

theorem :: INTEGRA9:59

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

proof end;

:: f.x= (x-a)/(x-b)

theorem :: INTEGRA9:60

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

proof end;

:: f.x=1/x

theorem :: INTEGRA9:61

for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z & dom ln = Z & Z = dom ((id Z) ^) & ((id Z) ^) | A is continuous holds
integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A))

proof end;

:: f.x=n/x

theorem :: INTEGRA9:62

for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f2 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
x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = n / x ) & f2 | A is continuous holds
integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A))

proof end;

:: f.x=-1/x

theorem :: INTEGRA9:63

for A being non empty closed_interval Subset of REAL
for f2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = - (1 / x) ) & f2 | A is continuous holds
integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A))

proof end;

:: irrational function
:: f.x = (a+x) #R (1/2)

theorem :: INTEGRA9:64

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A))

proof end;

:: f.x = (a-x) #R (1/2)

theorem :: INTEGRA9:65

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds
integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A))

proof end;

:: f.x = (a+x) #R (-1/2)

theorem :: INTEGRA9:66

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A))

proof end;

:: f.x = (a-x) #R (-1/2)

theorem :: INTEGRA9:67

for a being Real
for A being non empty closed_interval Subset of REAL
for f, f2 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 = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds
f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds
integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A))

proof end;

:: f.x=-x*cos.x+sin.x

theorem :: INTEGRA9:68

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

proof end;

:: f.x=sin.x/(cos.x)^2

theorem :: INTEGRA9:69

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

proof end;

:: f.x = (-cosec).x

theorem Th70: :: INTEGRA9:70

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

proof end;

:: f.x=cos.x/(sin.x)^2

theorem :: INTEGRA9:71

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

proof end;