:: Integrability Formulas -- Part {I} :: by Bo Li and Na Ma :: :: Received November 7, 2009 :: Copyright (c) 2009-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 RELAT_1, FUNCT_1, ARYTM_1, SIN_COS, INTEGRA1, FDIFF_1, XBOOLE_0, SQUARE_1, ARYTM_3, ORDINAL2, RCOMP_1, PREPOWER, NEWTON, NUMBERS, REAL_1, SUBSET_1, XXREAL_0, XXREAL_1, PARTFUN1, TAYLOR_1, SIN_COS6, SIN_COS9, LIMFUNC1, TARSKI, VALUED_1, CARD_1, ORDINAL4, INTEGRA5, NAT_1, XXREAL_2, SEQ_4, MEASURE5; notations TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS, VALUED_1, XCMPLX_0, NAT_1, XXREAL_0, XREAL_0, REAL_1, RELSET_1, PARTFUN1, PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, MEASURE6, INTEGRA1, FCONT_1, SQUARE_1, INTEGRA5, TAYLOR_1, FDIFF_1, SEQ_2, SEQ_4, SIN_COS6, SIN_COS9, NEWTON, LIMFUNC1, PREPOWER; constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, MEASURE6, BINOP_2, SQUARE_1, PREPOWER, INTEGRA5, SEQ_4, XXREAL_3, XBOOLE_0, SEQ_2, LIMFUNC1, NAT_1, POWER, RELSET_1, TARSKI, SIN_COS9, PARTFUN1, PARTFUN2, FUNCT_1, RCOMP_1, RELAT_1, SIN_COS6, RFUNCT_1, VALUED_1, FDIFF_9, NEWTON, INTEGRA1, COMSEQ_2; registrations NAT_1, NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1, ORDINAL1, FUNCT_2, RCOMP_1, RELSET_1, XREAL_0, NEWTON, SQUARE_1, MEASURE5, PREPOWER; requirements NUMERALS, SUBSET, ARITHM, REAL; begin reserve a,b,x,r for Real; reserve y for set; reserve n for Element of NAT; reserve A for non empty closed_interval Subset of REAL; reserve f,g,f1,f2,g1,g2 for PartFunc of REAL,REAL; reserve Z for open Subset of REAL; theorem :: INTEGR12:1 Z c= dom ((f1+f2)^) & (for x st x in Z holds f1.x=1) & f2=#Z 2 implies (f1+f2)^ is_differentiable_on Z & for x st x in Z holds (((f1+f2)^)`|Z).x = -2*x/(1+x |^2)^2; ::f.x=1/((1+x^2)*arccot.x) theorem :: INTEGR12:2 A c= Z & f = ((g1+g2)^)/f2 & f2 = arccot & Z c= ]. -1,1 .[ & g2=#Z 2 & (for x st x in Z holds g1.x=1 & f2.x>0) & Z = dom f implies integral(f,A)=(-ln*arccot).(upper_bound A)-(-ln*arccot).(lower_bound A); ::f.x=exp_R.x/(1+(exp_R.x)^2) theorem :: INTEGR12:3 A c= Z & (for x st x in Z holds exp_R.x < 1 & f1.x=1) & Z c= dom (arctan*exp_R) & Z = dom f & f=exp_R/(f1+(exp_R)^2) implies integral(f,A)=(arctan*exp_R).(upper_bound A) -(arctan*exp_R).(lower_bound A); ::f.x=-exp_R.x/(1+(exp_R.x)^2) theorem :: INTEGR12:4 A c= Z & (for x st x in Z holds exp_R.x < 1 & f1.x=1) & Z c= dom (arccot*exp_R) & Z = dom f & f=(-exp_R)/(f1+(exp_R)^2) implies integral(f,A)=(arccot*exp_R).(upper_bound A) -(arccot*exp_R).(lower_bound A); ::f.x=exp_R.x*sin.x/cos.x+exp_R.x/(cos.x)^2 theorem :: INTEGR12:5 A c= Z & Z = dom f & f=exp_R(#)(sin/cos)+exp_R/cos^2 implies integral(f,A)=(exp_R(#)tan).(upper_bound A)-(exp_R(#)tan).(lower_bound A); ::f.x=exp_R.x*cos.x/sin.x-exp_R.x/(sin.x)^2 theorem :: INTEGR12:6 A c= Z & Z = dom f & f=exp_R(#)(cos/sin)-exp_R/sin^2 implies integral(f,A)=(exp_R(#)cot).(upper_bound A)-(exp_R(#)cot).(lower_bound A); ::f.x=exp_R.x*arctan.x+exp_R.x/(1+x^2) theorem :: INTEGR12:7 A c= Z & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z = dom f & f=exp_R(#)arctan+exp_R/(f1+#Z 2) implies integral(f,A )=(exp_R(#)arctan).(upper_bound A)-(exp_R(#)arctan).(lower_bound A); ::f.x=exp_R.x*arccot.x-exp_R.x/(1+x^2) theorem :: INTEGR12:8 A c= Z & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z = dom f & f=exp_R(#)arccot-exp_R/(f1+#Z 2) implies integral(f,A) =(exp_R(#)arccot).(upper_bound A)-(exp_R(#)arccot).(lower_bound A); ::f.x=exp_R.(sin.x) * cos.x theorem :: INTEGR12:9 A c= Z & Z = dom f & f=(exp_R*sin)(#)cos implies integral(f,A)=(exp_R*sin).(upper_bound A)-(exp_R*sin).(lower_bound A); ::f.x=exp_R.(cos.x) * sin.x theorem :: INTEGR12:10 A c= Z & Z = dom f & f=(exp_R*cos)(#)sin implies integral(f,A)=(-exp_R*cos).(upper_bound A)-(-exp_R*cos).(lower_bound A); ::f.x=cos.(ln.x)/x theorem :: INTEGR12:11 A c= Z & (for x st x in Z holds x>0) & Z = dom f & f=(cos*ln)(#)((id Z)^) implies integral(f,A)=(sin*ln).(upper_bound A)-(sin*ln).(lower_bound A); ::f.x=sin.(ln.x)/x theorem :: INTEGR12:12 A c= Z & (for x st x in Z holds x>0) & Z = dom f & f=(sin*ln)(#)((id Z)^) implies integral(f,A)=(-cos*ln).(upper_bound A)-(-cos*ln).(lower_bound A); ::f.x=exp_R.x * cos.(exp_R.x) theorem :: INTEGR12:13 A c= Z & Z = dom f & f=exp_R(#)(cos*exp_R) implies integral(f,A)=(sin*exp_R).(upper_bound A)-(sin*exp_R).(lower_bound A); ::f.x = exp_R.x * sin.(exp_R.x) theorem :: INTEGR12:14 A c= Z & Z = dom f & f=exp_R(#)(sin*exp_R) implies integral(f,A)=(-cos*exp_R).(upper_bound A)-(-cos*exp_R).(lower_bound A); ::f.x=arctan.(x/r) theorem :: INTEGR12:15 A c= Z & Z c= dom (ln*(f1+f2)) & r <> 0 & (for x st x in Z holds g.x=x/r & g.x > -1 & g.x < 1 & f1.x=1) & f2=( #Z 2)*g & Z = dom f & f=arctan*g implies integral(f,A)=((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2))).(lower_bound A); ::f.x=arccot.(x/r) theorem :: INTEGR12:16 A c= Z & Z c= dom (ln*(f1+f2)) & r <> 0 & (for x st x in Z holds g.x=x/r & g.x > -1 & g.x < 1 & f1.x=1) & f2=( #Z 2)*g & Z = dom f & f=arccot*g implies integral(f,A)=((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2))).(lower_bound A); ::f.x=arctan.(x/r)+x/(r*(1+(x/r)^2)) theorem :: INTEGR12:17 A c= Z & f=arctan*f1+(id Z)/(r(#)(g+f1^2)) & (for x st x in Z holds g.x=1 & f1.x=x/r & f1.x > -1 & f1.x < 1) & Z = dom f & f|A is continuous implies integral(f,A)=((id Z)(#)(arctan*f1)).(upper_bound A) -((id Z)(#)(arctan*f1)).(lower_bound A); ::f.x=arccot.(x/r)-x/(r*(1+(x/r)^2)) theorem :: INTEGR12:18 A c= Z & f=arccot*f1-(id Z)/(r(#)(g+f1^2)) & (for x st x in Z holds g.x=1 & f1.x=x/r & f1.x > -1 & f1.x < 1) & Z = dom f & f|A is continuous implies integral(f,A)=((id Z)(#)((arccot)*f1)).(upper_bound A) -((id Z)(#)((arccot)*f1)).(lower_bound A); ::f.x=n*(arcsin.x) #Z (n-1) / sqrt(1-x^2) theorem :: INTEGR12:19 A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f1.x=1) & Z = dom f & Z c= dom (( #Z n)*arcsin) & 1-1 & f1.x<1) & Z = dom f & f|A is continuous & f=arcsin*f1+(id Z)/(a(#)(( #R (1/2))*(g-f1^2))) implies integral(f,A)=((id Z)(#)((arcsin)*f1)).(upper_bound A) -((id Z)(#)((arcsin)*f1)).(lower_bound A); ::f.x=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2)) theorem :: INTEGR12:26 A c= Z & (for x st x in Z holds g.x=1 & f1.x=x/a & f1.x>-1 & f1.x<1) & Z = dom f & f|A is continuous & f=arccos*f1-(id Z)/(a(#)(( #R (1/2))*(g-f1^2))) implies integral(f,A)=((id Z)(#)(arccos*f1)).(upper_bound A) -((id Z)(#)(arccos*f1)).(lower_bound A); ::f.x = n*(sin.x) #Z (n-1)/(cos.x) #Z (n+1) theorem :: INTEGR12:27 A c= Z & f=(n(#)(( #Z (n-1))*sin))/(( #Z (n+1))*cos) & 1<=n & Z c= dom (( #Z n)*tan) & Z = dom f implies integral(f,A)=(( #Z n)*tan).(upper_bound A)-(( #Z n)*tan).(lower_bound A); ::f.x=n*(cos.x) #Z (n-1)/(sin.x) #Z (n+1) theorem :: INTEGR12:28 A c= Z & f=(n(#)(( #Z (n-1))*cos))/(( #Z (n+1))*sin) & 1<=n & Z c= dom (( #Z n)*cot) & Z = dom f implies integral(f,A)=(-( #Z n)*cot).(upper_bound A)-(-( #Z n)*cot).(lower_bound A); ::f.x=(sin.(a*x))^2/(cos.(a*x))^2 theorem :: INTEGR12:29 A c= Z & Z c= dom (tan*f1) & f=(sin*f1)^2/(cos*f1)^2 & (for x st x in Z holds f1.x=a*x & a<>0) & Z = dom f implies integral(f,A)=((1/a)(#)(tan*f1)-id Z).(upper_bound A) -((1/a)(#)(tan*f1)-id Z).(lower_bound A); ::f.x=(cos.(a*x))^2/(sin.(a*x))^2 theorem :: INTEGR12:30 A c= Z & Z c= dom (cot*f1) & f=(cos*f1)^2/(sin*f1)^2 & (for x st x in Z holds f1.x=a*x & a<>0) & Z = dom f implies integral(f,A)=((-1/a)(#)(cot*f1)-id Z).(upper_bound A) -((-1/a)(#)(cot*f1)-id Z).(lower_bound A); ::f.x=a*sin.x/cos.x+(a*x+b)/(cos.x)^2 theorem :: INTEGR12:31 A c= Z & (for x st x in Z holds f1.x=a*x+b) & Z = dom f & f=a(#)(sin/cos)+f1/cos^2 implies integral(f,A)=(f1(#)tan).(upper_bound A)-(f1(#)tan).(lower_bound A); ::f.x=a*cos.x/sin.x-(a*x+b)/(sin.x)^2 theorem :: INTEGR12:32 A c= Z & (for x st x in Z holds f1.x=a*x+b) & Z = dom f & f=a(#)(cos/sin)-f1/sin^2 implies integral(f,A)=(f1(#)cot).(upper_bound A)-(f1(#)cot).(lower_bound A); ::f.x=(sin.x)^2/(cos.x)^2 theorem :: INTEGR12:33 A c= Z & (for x st x in Z holds f.x=(sin.x)^2/(cos.x)^2) & Z c= dom (tan-id Z) & Z = dom f & f|A is continuous implies integral(f,A)=(tan-id Z).(upper_bound A)-(tan-id Z).(lower_bound A); ::f.x=(cos.x)^2/(sin.x)^2 theorem :: INTEGR12:34 A c= Z & (for x st x in Z holds f.x=(cos.x)^2/(sin.x)^2) & Z c= dom (-cot-id Z) & Z = dom f & f|A is continuous implies integral(f,A)=(-cot-id Z).(upper_bound A)-(-cot-id Z).(lower_bound A); ::f.x=1/(x*(1+(ln.x)^2)) theorem :: INTEGR12:35 A c= Z & (for x st x in Z holds f.x=1/(x*(1+(ln.x)^2)) & ln.x > -1 & ln.x < 1) & Z c= dom (arctan*ln) & Z = dom f & f|A is continuous implies integral(f,A)=(arctan*ln).(upper_bound A) -(arctan*ln).(lower_bound A); ::f.x=-1/(x*(1+(ln.x)^2)) theorem :: INTEGR12:36 A c= Z & (for x st x in Z holds f.x=-1/(x*(1+(ln.x)^2)) & ln.x > -1 & ln.x < 1) & Z c= dom (arccot*ln) & Z = dom f & f|A is continuous implies integral(f,A)=(arccot*ln).(upper_bound A) -(arccot*ln).(lower_bound A); ::f.x=a / sqrt(1-(a*x+b)^2) theorem :: INTEGR12:37 A c= Z & (for x st x in Z holds f.x=a / sqrt(1-(a*x+b)^2) & f1.x=a*x+b & f1.x>-1 & f1.x<1) & Z c= dom ((arcsin)*f1) & Z = dom f & f|A is continuous implies integral(f,A)=((arcsin)*f1).(upper_bound A)-((arcsin)*f1).(lower_bound A); theorem :: INTEGR12:38 A c= Z & (for x st x in Z holds f.x=a / sqrt(1-(a*x+b)^2) & f1.x=a*x+b & f1.x>-1 & f1.x<1) & Z c= dom ((arccos)*f1) & Z = dom f & f|A is continuous implies integral(f,A)=(-(arccos)*f1).(upper_bound A)-(-(arccos)*f1).(lower_bound A); ::f.x=x*(1-x #Z 2) #R (-1/2) theorem :: INTEGR12:39 A c= Z & f1=g-f2 & f2=#Z 2 & (for x st x in Z holds f.x=x*(1-x #Z 2) #R (-1/2) & g.x=1 & f1.x >0) & Z c= dom (( #R (1/2))*f1) & Z = dom f & f|A is continuous implies integral(f,A)=(-( #R (1/2))*f1).(upper_bound A) -(-( #R (1/2))*f1).(lower_bound A); ::f.x=x*(a^2-x #Z 2) #R (-1/2) theorem :: INTEGR12:40 A c= Z & g=f1-f2 & f2=#Z 2 & (for x st x in Z holds f.x=x*((a^2-x #Z 2) #R (-1/2)) & f1.x=a^2 & g.x >0) & Z c= dom (( #R (1/2))*g) & Z = dom f & f|A is continuous implies integral(f,A) =(-( #R (1/2))*g).(upper_bound A)-(-( #R (1/2))*g).(lower_bound A); ::f.x=cos.x/((sin.x) #Z (n+1)) theorem :: INTEGR12:41 A c= Z & n>0 & (for x st x in Z holds f.x=cos.x/((sin.x) #Z (n+1)) & sin.x<>0) & Z c= dom (( #Z n)*(sin^)) & Z =dom f & f|A is continuous implies integral(f,A)=((-1/n)(#)(( #Z n)*(sin^))).(upper_bound A) -((-1/n)(#)(( #Z n)*(sin^))).(lower_bound A); ::f.x=sin.x/((cos.x) #Z (n+1)) theorem :: INTEGR12:42 A c= Z & n>0 & (for x st x in Z holds f.x=sin.x/((cos.x) #Z (n+1)) & cos.x<>0) & Z c= dom (( #Z n)*(cos^)) & Z =dom f & f|A is continuous implies integral(f,A)=((1/n)(#)(( #Z n)*(cos^))).(upper_bound A) -((1/n)(#)(( #Z n)*(cos^))).(lower_bound A); ::f.x=1/((1+x^2)*arccot.x) theorem :: INTEGR12:43 A c= Z & f = ((g1+g2)^)/f2 & f2 = arccot & Z c= ]. -1,1 .[ & g2=#Z 2 & (for x st x in Z holds f.x=1/((1+x^2)*arccot.x) & g1.x=1 & f2.x>0) & Z = dom f implies integral(f,A)=(-ln*arccot).(upper_bound A)-(-ln*arccot).(lower_bound A); ::f.x=1 / (sqrt(1-x^2)*arcsin.x) theorem :: INTEGR12:44 A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds arcsin.x>0 & f1.x=1) & Z c= dom (ln*(arcsin)) & Z = dom f & f=((( #R (1/2))*(f1-#Z 2))(#)arcsin)^ implies integral(f,A)=(ln*(arcsin)).(upper_bound A)-(ln*(arcsin)).(lower_bound A); ::f.x=1 / (sqrt(1-x^2)*arccos.x) theorem :: INTEGR12:45 A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f1.x=1 & arccos.x>0) & Z c= dom (ln*arccos) & Z = dom f & f=((( #R (1/2))*(f1-#Z 2))(#)arccos)^ implies integral(f,A)=(-ln*arccos).(upper_bound A)-(-ln*arccos).(lower_bound A);