:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies REAL_1, XBOOLE_0, SUBSET_1, NUMBERS, INTEGRA1, PARTFUN1, RCOMP_1, RELAT_1, ARYTM_1, SIN_COS, JGRAPH_2, CARD_1, FDIFF_1, FUNCT_1, ARYTM_3, VALUED_1, SEQ_4, ORDINAL2, INTEGRA5, XXREAL_2, TARSKI, PREPOWER, NEWTON, REALSET1, XXREAL_0, XXREAL_1, SQUARE_1, ORDINAL4, TAYLOR_1, SIN_COS4, INTEGRA9, MEASURE5; notations FUNCT_1, SIN_COS, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, VALUED_1, SEQ_4, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, RELSET_1, PARTFUN1, RFUNCT_1, RCOMP_1, MEASURE5, INTEGRA1, FCONT_1, FDIFF_9, SQUARE_1, INTEGRA5, PARTFUN2, NEWTON, PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2; constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER, INTEGRA5, PARTFUN2, LIMFUNC1, SEQ_4, RFUNCT_1, FDIFF_9, RELSET_1, SEQ_2, NEWTON, INTEGRA1, COMSEQ_2, BINOP_2, NUMBERS; registrations VALUED_1, NAT_1, XBOOLE_0, NUMBERS, MEMBERED, VALUED_0, RCOMP_1, INT_1, ORDINAL1, FUNCT_2, RELSET_1, FCONT_1, FCONT_3, MEASURE5, XREAL_0, PREPOWER, SIN_COS, SQUARE_1, NEWTON; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve r,p,x for Real; reserve n for Element of NAT; reserve A for non empty closed_interval Subset of REAL; reserve Z for open Subset of REAL; theorem :: INTEGRA9:1 -(exp_R*(AffineMap(-1,0))) is_differentiable_on REAL & for x holds ((- (exp_R*(AffineMap(-1,0))))`|REAL).x = exp_R(-x); :: f.x = (1/r)*exp_R.(r*x) theorem :: INTEGRA9:2 r<>0 implies (1/r)(#)(exp_R*(AffineMap(r,0))) is_differentiable_on REAL & for x holds (((1/r)(#)(exp_R*(AffineMap(r,0))))`| REAL).x=(exp_R*(AffineMap(r,0))).x; :: f.x = exp_R.(r*x) theorem :: INTEGRA9:3 r<>0 implies 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); :: f.x=(-1/n)*cos(n*x) theorem :: INTEGRA9:4 n<>0 implies (-1/n)(#)(cos*(AffineMap(n,0))) is_differentiable_on REAL & for x holds (((-1/n)(#)(cos*(AffineMap(n,0))))`|REAL).x =sin(n*x); :: f.x=sin(n*x) theorem :: INTEGRA9:5 n<>0 implies integral(sin*(AffineMap(n,0)),A) = ((-1/n)(#)(cos*( AffineMap(n,0)))).(upper_bound A) -((-1/n)(#)(cos*(AffineMap(n,0)))).( lower_bound A); :: f.x=(1/n)*sin(n*x) theorem :: INTEGRA9:6 n<>0 implies (1/n)(#)(sin*(AffineMap(n,0))) is_differentiable_on REAL & for x holds (((1/n)(#)(sin*(AffineMap(n,0))))`|REAL).x = cos(n*x); :: f.x=cos(n*x) theorem :: INTEGRA9:7 n<>0 implies integral(cos*(AffineMap(n,0)),A) = ((1/n)(#)(sin*( AffineMap(n,0)))).(upper_bound A) -((1/n)(#)(sin*(AffineMap(n,0)))).( lower_bound A); :: f.x=x*sin.x theorem :: INTEGRA9:8 A c= Z implies integral((id Z)(#)sin,A) = ((-id Z)(#)cos+sin).( upper_bound A)-((-id Z)(#)cos+sin).(lower_bound A); :: f.x=x*cos.x theorem :: INTEGRA9:9 A c= Z implies integral((id Z)(#)cos,A) = ((id Z)(#)sin+cos).( upper_bound A)-((id Z)(#)sin+cos).(lower_bound A); :: f.x=x*cos.x theorem :: INTEGRA9:10 (id Z)(#)cos is_differentiable_on Z & for x st x in Z holds ((( id Z)(#)cos)`|Z).x =cos.x-x*sin.x; :: f.x = -sin.x+x*cos.x theorem :: INTEGRA9:11 -sin+(id Z)(#)cos is_differentiable_on Z & for x st x in Z holds ((-sin+(id Z)(#)cos)`|Z).x =-x*sin.x; :: f.x=-x*sin.x theorem :: INTEGRA9:12 A c= Z implies integral((-id Z)(#)sin,A) = (-sin+(id Z)(#)cos).( upper_bound A)-(-sin+(id Z)(#)cos).(lower_bound A); :: f.x = -cos.x-x*sin.x theorem :: INTEGRA9:13 -cos-(id Z)(#)sin is_differentiable_on Z & for x st x in Z holds ((-cos-(id Z)(#)sin)`|Z).x =-x*cos.x; :: f.x = -x*cos.x theorem :: INTEGRA9:14 A c= Z implies integral((-id Z)(#)cos,A) = (-cos-(id Z)(#)sin).( upper_bound A)-(-cos-(id Z)(#)sin).(lower_bound A); :: f.x=sin.x+x*cos.x theorem :: INTEGRA9:15 A c= Z implies integral(sin+(id Z)(#)cos,A) = ((id Z)(#)sin).( upper_bound A)-((id Z)(#)sin).(lower_bound A); :: f.x=-cos.x+x*sin.x theorem :: INTEGRA9:16 A c= Z implies integral(-cos+(id Z)(#)sin,A) = ((-id Z)(#)cos).( upper_bound A)-((-id Z)(#)cos).(lower_bound A); :: f.x = x*(exp_R.x) theorem :: INTEGRA9:17 integral((AffineMap(1,0))(#)exp_R,A) = (exp_R(#)(AffineMap(1,-1))).( upper_bound A) -(exp_R(#)(AffineMap(1,-1))).(lower_bound A); :: f.x = (1/(n+1))*x^(n+1) theorem :: INTEGRA9:18 (1/(n+1))(#)( #Z (n+1)) is_differentiable_on REAL & for x holds (((1/(n+1))(#)( #Z (n+1)))`|REAL).x = x #Z n; :: f.x = x^n theorem :: INTEGRA9:19 integral( #Z n,A) = ((1/(n+1))*((upper_bound A) |^ (n+1))) - ((1/(n+1) )*((lower_bound A) |^ (n+1))); begin theorem :: INTEGRA9:20 for f,g being PartFunc of REAL,REAL, C being non empty Subset of REAL holds (f-g)||C = f||C - g||C; theorem :: INTEGRA9:21 for f1,f2,g being PartFunc of REAL,REAL, C being non empty Subset of REAL holds ((f1+f2)||C)(#)(g||C)=(f1(#)g+f2(#)g)||C; theorem :: INTEGRA9:22 for f1,f2,g being PartFunc of REAL,REAL, C being non empty Subset of REAL holds ((f1-f2)||C)(#)(g||C)=(f1(#)g-f2(#)g)||C; theorem :: INTEGRA9:23 for f1,f2,g being PartFunc of REAL,REAL, C being non empty Subset of REAL holds ((f1(#)f2)||C)(#)(g||C)=(f1||C)(#)((f2(#)g)||C); 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); end; theorem :: INTEGRA9:24 for f,g being PartFunc of REAL,REAL, 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, 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)|||; theorem :: INTEGRA9:26 for f1,f2,g being PartFunc of REAL,REAL, 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)|||; theorem :: INTEGRA9:27 for f,g being PartFunc of REAL,REAL, 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)|||; theorem :: INTEGRA9:28 for f,g being PartFunc of REAL,REAL, 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)|||; theorem :: INTEGRA9:29 for f,g being PartFunc of REAL,REAL, 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)|||; theorem :: INTEGRA9:30 for f,g,h being PartFunc of REAL,REAL, A being non empty closed_interval Subset of REAL holds |||((f(#)g),h,A)||| = |||(f,(g(#)h),A)|||; theorem :: INTEGRA9:31 for f,g being PartFunc of REAL,REAL, 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)|||; begin :: Orthogonal polynomials 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; theorem :: INTEGRA9:32 for f,g being PartFunc of REAL,REAL, 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)|||; theorem :: INTEGRA9:33 for f being PartFunc of REAL,REAL, 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 st x in A holds (f(#)f)||A.x >= 0) holds |||(f,f,A)||| >= 0 ; theorem :: INTEGRA9:34 A = [.0,PI.] implies sin is_orthogonal_with cos,A; theorem :: INTEGRA9:35 A = [.0,PI*2.] implies sin is_orthogonal_with cos,A; theorem :: INTEGRA9:36 A = [.2*n*PI,(2*n+1)*PI.] implies sin is_orthogonal_with cos,A; theorem :: INTEGRA9:37 A = [.x+2*n*PI,x+(2*n+1)*PI.] implies sin is_orthogonal_with cos,A; theorem :: INTEGRA9:38 A = [.-PI,PI.] implies sin is_orthogonal_with cos,A; theorem :: INTEGRA9:39 A = [.-PI/2,PI/2.] implies sin is_orthogonal_with cos,A; theorem :: INTEGRA9:40 A = [.-2*PI,2*PI.] implies sin is_orthogonal_with cos,A; theorem :: INTEGRA9:41 A = [.-2*n*PI,2*n*PI.] implies sin is_orthogonal_with cos,A; theorem :: INTEGRA9:42 A = [.x-2*n*PI,x+2*n*PI.] implies sin is_orthogonal_with cos,A; begin :: Definition and properties of norm function 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)|||); end; theorem :: INTEGRA9:43 for f being PartFunc of REAL,REAL, A being non empty closed_interval Subset of REAL st (f(#)f)||A is total & (f(#)f)||A|A is bounded & (for x st x in A holds (f(#)f)||A.x >= 0) holds 0 <= ||..f,A..||; theorem :: INTEGRA9:44 for f being PartFunc of REAL,REAL, A being non empty closed_interval Subset of REAL holds ||..(1(#)f),A..|| = ||..f,A..||; theorem :: INTEGRA9:45 for f,g being PartFunc of REAL,REAL, 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 st x in A holds (f(#)f)||A.x >= 0) & (for x st x in A holds (g(#)g)||A.x >= 0) holds ||..(f+g),A..||^2 = ||..f,A..||^2 + ||..g,A..||^2; begin :: To be revised reserve a,b,x for Real; reserve n for Element of NAT; reserve A for non empty closed_interval Subset of REAL; reserve f,f1,f2 for PartFunc of REAL,REAL; reserve Z for open Subset of REAL; :: f.x = 1/(a+x) theorem :: INTEGRA9:46 not -a in A implies (AffineMap (1,a))^|A is continuous; :: f.x=-1/(a+x)^2 theorem :: INTEGRA9:47 A c= Z & (for x st x in Z holds f.x = a+x & f.x<>0) & Z = dom f & dom f = dom f2 & (for x st x in Z holds f2.x = -1/(a+x)^2 ) & f2|A is continuous implies integral(f2,A) = f^.(upper_bound A)-f^.(lower_bound A); :: f.x=1/(a+x)^2 theorem :: INTEGRA9:48 A c= Z & (for x st x in Z holds f.x = a+x & f.x<>0) & dom((-1)(#)(f^)) =Z & dom((-1)(#)(f^))=dom f2 & (for x st x in Z holds f2.x = 1/(a+x)^2 ) & f2|A is continuous implies integral(f2,A) = ((-1)(#)(f^)).(upper_bound A)-((-1)(#)(f ^)).(lower_bound A); :: f.x=1/(a-x)^2 theorem :: INTEGRA9:49 A c= Z & (for x st x in Z holds f.x = a-x & f.x<>0) & dom f = Z & dom f = dom f2 & (for x st x in Z holds f2.x = 1/(a-x)^2 ) & f2|A is continuous implies integral(f2,A) = f^.(upper_bound A)-f^.(lower_bound A); :: f.x=1/(a+x) theorem :: INTEGRA9:50 A c= Z & (for x st x in Z holds f.x = a+x & f.x > 0) & dom (ln*f) = Z & dom (ln*f) = dom f2 & (for x st x in Z holds f2.x = 1/(a+x) ) & f2|A is continuous implies integral(f2,A) = (ln*f).(upper_bound A)-(ln*f).(lower_bound A); :: f.x=1/(x-a) theorem :: INTEGRA9:51 A c= Z & (for x st x in Z holds f.x = x-a & f.x > 0) & dom (ln*f) = Z & dom (ln*f) = dom f2 & (for x st x in Z holds f2.x = 1/(x-a) ) & f2|A is continuous implies integral(f2,A) = (ln*f).(upper_bound A)-(ln*f).(lower_bound A); :: f.x=1/(a-x) theorem :: INTEGRA9:52 A c= Z & (for x st x in Z holds f.x = a-x & f.x > 0) & dom (-(ln*f)) = Z & dom (-(ln*f)) = dom f2 & (for x st x in Z holds f2.x = 1/(a-x) ) & f2|A is continuous implies integral(f2,A) = (-(ln*f)).(upper_bound A)-(-(ln*f)).( lower_bound A); :: f.x= x/(a+x) theorem :: INTEGRA9:53 A c= Z & f = ln*f1 & (for x st x in Z holds f1.x=a+x & f1.x>0) & dom ( id Z - a(#)f) = Z & Z = dom f2 & (for x st x in Z holds f2.x = x/(a+x) ) & f2|A is continuous implies integral(f2,A) = (id Z - a(#)f).(upper_bound A)-(id Z - a (#)f).(lower_bound A); :: f.x= (a-x)/(a+x) theorem :: INTEGRA9:54 A c= Z & f = ln*f1 & (for x st x in Z holds f1.x=a+x & f1.x>0) & dom ( (2*a)(#)f - id Z) = Z & Z = dom f2 & (for x st x in Z holds f2.x = (a-x)/(a+x)) & f2|A is continuous implies integral(f2,A) = ((2*a)(#)f - id Z).(upper_bound A )-((2*a)(#)f - id Z).(lower_bound A); :: f.x= (x-a)/(x+a) theorem :: INTEGRA9:55 A c= Z & f = ln*f1 & (for x st x in Z holds f1.x=x+a & f1.x>0) & dom ( id Z -(2*a)(#)f) = Z & Z = dom f2 & (for x st x in Z holds f2.x = (x-a)/(x+a)) & f2|A is continuous implies integral(f2,A) = (id Z -(2*a)(#)f).(upper_bound A) -(id Z -(2*a)(#)f).(lower_bound A); :: f.x= (x+a)/(x-a) theorem :: INTEGRA9:56 A c= Z & f = ln*f1 & (for x st x in Z holds f1.x=x-a & f1.x>0) & dom ( id Z + (2*a)(#)f) = Z & Z = dom f2 & (for x st x in Z holds f2.x = (x+a)/(x-a)) & f2|A is continuous implies integral(f2,A) = (id Z + (2*a)(#)f).(upper_bound A )-(id Z + (2*a)(#)f).(lower_bound A); :: f.x= (x+a)/(x+b) theorem :: INTEGRA9:57 A c= Z & f = ln*f1 & (for x st x in Z holds f1.x=x+b & f1.x>0) & dom ( id Z + (a-b)(#)f) = Z & Z = dom f2 & (for x st x in Z holds f2.x = (x+a)/(x+b)) & f2|A is continuous implies integral(f2,A) = (id Z + (a-b)(#)f).(upper_bound A )-(id Z + (a-b)(#)f).(lower_bound A); :: f.x= (x+a)/(x-b) theorem :: INTEGRA9:58 A c= Z & f = ln*f1 & (for x st x in Z holds f1.x=x-b & f1.x>0) & dom ( id Z + (a+b)(#)f) = Z & Z = dom f2 & (for x st x in Z holds f2.x = (x+a)/(x-b)) & f2|A is continuous implies integral(f2,A) = (id Z + (a+b)(#)f).(upper_bound A )-(id Z + (a+b)(#)f).(lower_bound A); :: f.x= (x-a)/(x+b) theorem :: INTEGRA9:59 A c= Z & f = ln*f1 & (for x st x in Z holds f1.x=x+b & f1.x>0) & dom ( id Z - (a+b)(#)f) = Z & Z = dom f2 & (for x st x in Z holds f2.x = (x-a)/(x+b)) & f2|A is continuous implies integral(f2,A) = (id Z - (a+b)(#)f).(upper_bound A )-(id Z - (a+b)(#)f).(lower_bound A); :: f.x= (x-a)/(x-b) theorem :: INTEGRA9:60 A c= Z & f = ln*f1 & (for x st x in Z holds f1.x=x-b & f1.x>0) & dom ( id Z + (b-a)(#)f) = Z & Z = dom f2 & (for x st x in Z holds f2.x = (x-a)/(x-b)) & f2|A is continuous implies integral(f2,A) = (id Z + (b-a)(#)f).(upper_bound A )-(id Z + (b-a)(#)f).(lower_bound A); :: f.x=1/x theorem :: INTEGRA9:61 A c= Z & dom ln = Z & Z = dom ((id Z)^) & (id Z)^|A is continuous implies integral((id Z)^,A) = ln.(upper_bound A)-ln.(lower_bound A); :: f.x=n/x theorem :: INTEGRA9:62 A c= Z & (for x st x in Z holds x > 0) & dom (ln*( #Z n)) = Z & dom ( ln*( #Z n)) = dom f2 & (for x st x in Z holds f2.x = n/x ) & f2|A is continuous implies integral(f2,A) = (ln*( #Z n)).(upper_bound A)-(ln*( #Z n)).(lower_bound A); :: f.x=-1/x theorem :: INTEGRA9:63 not 0 in Z & A c= Z & dom (ln*((id Z)^)) = Z & dom (ln*((id Z)^)) = dom f2 & (for x st x in Z holds f2.x = -1/x) & f2|A is continuous implies integral(f2,A) = (ln*((id Z)^)).(upper_bound A)-(ln*((id Z)^)).(lower_bound A); :: irrational function :: f.x = (a+x) #R (1/2) theorem :: INTEGRA9:64 A c= Z & (for x 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 st x in Z holds f2.x = (a+x) #R (1/2)) & f2|A is continuous implies integral(f2,A) = ((2/ 3)(#)(( #R (3/2))*f)).(upper_bound A) -((2/3)(#)(( #R (3/2))*f)).(lower_bound A ); :: f.x = (a-x) #R (1/2) theorem :: INTEGRA9:65 A c= Z & (for x 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 st x in Z holds f2.x = (a-x) #R (1/2)) & f2|A is continuous implies integral(f2,A) = ((-2 /3)(#)(( #R (3/2))*f)).(upper_bound A) -((-2/3)(#)(( #R (3/2))*f)).(lower_bound A); :: f.x = (a+x) #R (-1/2) theorem :: INTEGRA9:66 A c= Z & (for x 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 st x in Z holds f2.x = (a+x) #R (-1/2)) & f2|A is continuous implies integral(f2,A) = (2(#)(( #R (1/2) )*f)).(upper_bound A) -(2(#)(( #R (1/2))*f)).(lower_bound A); :: f.x = (a-x) #R (-1/2) theorem :: INTEGRA9:67 A c= Z & (for x 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 st x in Z holds f2.x = (a-x) #R (-1/2)) & f2|A is continuous implies integral(f2,A) = ((-2)(#)( ( #R (1/2))*f)).(upper_bound A) -((-2)(#)(( #R (1/2))*f)).(lower_bound A); :: f.x=-x*cos.x+sin.x theorem :: INTEGRA9:68 A c= Z & dom ((-id Z)(#)cos+sin) = Z & (for x st x in Z holds f.x =x* sin.x) & Z = dom f & f|A is continuous implies integral(f,A) = ((-id Z)(#)cos+ sin).(upper_bound A)-((-id Z)(#)cos+sin).(lower_bound A); :: f.x=sin.x/(cos.x)^2 theorem :: INTEGRA9:69 A c= Z & dom sec = Z & (for x st x in Z holds f.x =sin.x/(cos.x)^2) & Z = dom f & f|A is continuous implies integral(f,A) = sec.(upper_bound A)-sec.( lower_bound A); :: f.x = (-cosec).x theorem :: INTEGRA9:70 Z c= dom (-cosec) implies -cosec is_differentiable_on Z & for x st x in Z holds ( (-cosec)`|Z).x = cos.x/(sin.x)^2; :: f.x=cos.x/(sin.x)^2 theorem :: INTEGRA9:71 A c= Z & dom (-cosec) = Z & (for x st x in Z holds f.x =cos.x/(sin.x) ^2) & Z = dom f & f|A is continuous implies integral(f,A) = (-cosec).( upper_bound A)-(-cosec).(lower_bound A);