:: 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-2012 Association of Mizar Users begin Lm1: dom (- (exp_R * (AffineMap ((- 1),0)))) = [#] REAL by FUNCT_2:def_1; :: f.x = -exp_R.(-x) 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) ) ) proofend; :: 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 ) ) proofend; :: 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)) proofend; :: 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) ) ) proofend; :: 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)) proofend; :: 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) ) ) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) ) ) proofend; Lm2: for x being Real holds ( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) ) proofend; :: 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)) ) ) proofend; :: 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)) proofend; :: 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)) ) ) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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 ) ) proofend; :: 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))) proofend; begin 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) proofend; 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 proofend; 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 proofend; 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) proofend; 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)||| proofend; 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)||| proofend; 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)||| proofend; 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)||| proofend; 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)||| proofend; 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)||| proofend; begin definition let A be non empty closed_interval Subset of REAL; let f, g be PartFunc of REAL,REAL; predf is_orthogonal_with g,A means :Def2: :: INTEGRA9:def 2 |||(f,g,A)||| = 0 ; end; :: deftheorem Def2 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)||| proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem :: INTEGRA9:38 for A being non empty closed_interval Subset of REAL st A = [.(- PI),PI.] holds sin is_orthogonal_with cos ,A proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; begin 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..|| proofend; 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) proofend; begin :: 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 proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: f.x= (x+a)/(x+b) theorem :: INTEGRA9:57 for b, 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 + 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)) proofend; :: f.x= (x+a)/(x-b) theorem :: INTEGRA9:58 for b, 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 - 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)) proofend; :: f.x= (x-a)/(x+b) theorem :: INTEGRA9:59 for b, 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 + 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)) proofend; :: f.x= (x-a)/(x-b) theorem :: INTEGRA9:60 for b, 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 - 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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) ) ) proofend; :: 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)) proofend;