environ vocabulary FINSEQ_1, ARYTM_1, INTEGRA1, MEASURE5, RELAT_1, ORDINAL2, BOOLE, FUNCT_1, CARD_1, FUNCT_3, SQUARE_1, ABSVALUE, RFUNCT_1, RLVECT_1, SEQ_2, LATTICES, JORDAN3, RCOMP_1, PARTFUN1, RFINSEQ, INTEGRA2, FDIFF_1, SEQ_1, ARYTM_3, PROB_1, FINSEQ_4, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, SEQ_4, PARTFUN1, PSCOMP_1, FINSEQ_1, RFUNCT_1, RVSUM_1, INTEGRA1, SEQ_1, SEQ_2, JORDAN3, PRE_CIRC, SFMASTR3, RCOMP_1, FDIFF_1, ABSVALUE, GOBOARD1, CARD_1, SQUARE_1, FINSEQ_4, TOPREAL1, RFINSEQ, BINARITH, INTEGRA2; constructors REAL_1, REALSET1, PARTFUN1, RFUNCT_1, PRE_CIRC, SFMASTR3, FDIFF_1, SQUARE_1, FINSEQ_4, RFINSEQ, TOPREAL1, BINARITH, JORDAN3, INTEGRA2, ABSVALUE, PSCOMP_1, FINSOP_1; clusters XREAL_0, RELSET_1, FINSEQ_1, NAT_2, GOBOARD1, INTEGRA1, INTEGRA2, NAT_1, MEMBERED, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Lemmas of Division reserve a,b,d,e,x,y for Real, i,j,k,n,m for Nat, x1 for set, p,q for FinSequence of REAL; theorem :: INTEGRA3:1 for A be closed-interval Subset of REAL, D be Element of divs A st vol(A) <> 0 holds ex i st i in dom D & vol(divset(D,i)) > 0; theorem :: INTEGRA3:2 for A be closed-interval Subset of REAL, D be Element of divs A st x in A holds ex j st j in dom D & x in divset(D,j); theorem :: INTEGRA3:3 for A be closed-interval Subset of REAL, D1,D2 be Element of divs A holds ex D be Element of divs A st D1 <= D & D2 <= D & rng D = rng D1 \/ rng D2; theorem :: INTEGRA3:4 for A be closed-interval Subset of REAL, D,D1 be Element of divs A st delta(D1)<min rng upper_volume(chi(A,A),D) holds (for x,y,i st i in dom D1 & x in rng D /\ divset(D1,i) & y in rng D /\ divset(D1,i) holds x=y); theorem :: INTEGRA3:5 for p,q st rng p = rng q & p is increasing & q is increasing holds p = q; theorem :: INTEGRA3:6 for A be closed-interval Subset of REAL, D,D1 be Element of divs A st D <= D1 & i in dom D & j in dom D & i <= j holds indx(D1,D,i) <= indx(D1,D,j) & indx(D1,D,i) in dom D1; theorem :: INTEGRA3:7 for A be closed-interval Subset of REAL, D,D1 be Element of divs A st D <= D1 & i in dom D & j in dom D & i < j holds indx(D1,D,i) < indx(D1,D,j); theorem :: INTEGRA3:8 for A be closed-interval Subset of REAL, D be Element of divs A holds delta(D) >= 0; theorem :: INTEGRA3:9 for A be closed-interval Subset of REAL, g be Function of A,REAL, D1,D2 be Element of divs A st x in divset(D1,len D1) & len D1 >= 2 & D1<=D2 & rng D2 = rng D1 \/ {x} & g is_bounded_on A holds Sum lower_volume(g,D2)-Sum lower_volume(g,D1)<=(sup rng g-inf rng g)*delta(D1); theorem :: INTEGRA3:10 for A be closed-interval Subset of REAL, g be Function of A,REAL, D1,D2 be Element of divs A st x in divset(D1,len D1) & len D1 >= 2 & D1<=D2 & rng D2 = rng D1 \/ {x} & g is_bounded_on A holds Sum upper_volume(g,D1)-Sum upper_volume(g,D2)<=(sup rng g-inf rng g)*delta(D1); theorem :: INTEGRA3:11 for A be closed-interval Subset of REAL, D be Element of divs A, r be Real, i,j be Nat st i in dom D & j in dom D & i<=j & r < mid(D,i,j).1 holds ex B be closed-interval Subset of REAL st r=inf B & sup B=mid(D,i,j).(len mid(D,i,j)) & len mid(D,i,j)=j-i+1 & mid(D,i,j) is DivisionPoint of B; theorem :: INTEGRA3:12 for A be closed-interval Subset of REAL, f be Function of A,REAL, D1,D2 be Element of divs A st x in divset(D1,len D1) & vol(A)<>0 & D1<=D2 & rng D2 = rng D1 \/ {x} & f is_bounded_on A & x > inf A holds Sum lower_volume(f,D2)-Sum lower_volume(f,D1)<=(sup rng f-inf rng f)*delta(D1); theorem :: INTEGRA3:13 for A be closed-interval Subset of REAL, f be Function of A,REAL, D1,D2 be Element of divs A st x in divset(D1,len D1) & vol(A)<>0 & D1<=D2 & rng D2 = rng D1 \/ {x} & f is_bounded_on A & x > inf A holds Sum upper_volume(f,D1)-Sum upper_volume(f,D2)<=(sup rng f-inf rng f)*delta(D1); theorem :: INTEGRA3:14 for A be closed-interval Subset of REAL, D1,D2 be Element of divs A, r be Real, i,j be Nat st i in dom D1 & j in dom D1 & i<=j & D1 <= D2 & r < mid(D2,indx(D2,D1,i),indx(D2,D1,j)).1 holds ex B be closed-interval Subset of REAL, MD1,MD2 be Element of divs B st r=inf B & sup B=MD2.(len MD2) & sup B=MD1.(len MD1) & MD1 <= MD2 & MD1=mid(D1,i,j) & MD2=mid(D2,indx(D2,D1,i),indx(D2,D1,j)); theorem :: INTEGRA3:15 for A be closed-interval Subset of REAL, D be Element of divs A st x in rng D holds D.1 <= x & x <= D.(len D); theorem :: INTEGRA3:16 for p be FinSequence of REAL, i,j,k st p is increasing & i in dom p & j in dom p & k in dom p & p.i <= p.k & p.k <= p.j holds p.k in rng mid(p,i,j); theorem :: INTEGRA3:17 for A be closed-interval Subset of REAL, f be Function of A,REAL, D be Element of divs A st f is_bounded_on A & i in dom D holds inf rng(f|divset(D,i)) <= sup rng f; theorem :: INTEGRA3:18 for A be closed-interval Subset of REAL, f be Function of A,REAL, D be Element of divs A st f is_bounded_on A & i in dom D holds sup rng(f|divset(D,i)) >= inf rng f; begin :: Darboux's Theorem theorem :: INTEGRA3:19 for A be closed-interval Subset of REAL, f be Function of A,REAL, T be DivSequence of A st f is_bounded_on A & delta(T) is convergent_to_0 & vol(A)<>0 holds lower_sum(f,T) is convergent & lim lower_sum(f,T) = lower_integral(f); theorem :: INTEGRA3:20 for A be closed-interval Subset of REAL, f be Function of A,REAL, T be DivSequence of A st f is_bounded_on A & delta(T) is convergent_to_0 & vol(A)<>0 holds upper_sum(f,T) is convergent & lim upper_sum(f,T) = upper_integral(f);