Copyright (c) 1999 Association of Mizar Users
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;
definitions TARSKI;
theorems AXIOMS, REAL_1, SEQ_4, SUBSET_1, REAL_2, PARTFUN1, PSCOMP_1,
INTEGRA1, RFUNCT_1, FUNCT_1, FINSEQ_1, RVSUM_1, SEQ_1, SEQ_2, FDIFF_1,
ABSVALUE, PRE_CIRC, NAT_1, GOBOARD2, RFINSEQ, TARSKI, GOBOARD1, SQUARE_1,
CARD_1, FINSEQ_5, TOPREAL1, FINSEQ_3, FINSEQ_4, JORDAN7, JORDAN3,
SFMASTR3, RLVECT_1, BINARITH, INTEGRA2, RELAT_1, XREAL_0, SCMFSA_7,
FUNCT_2, XBOOLE_0, XBOOLE_1, RCOMP_1, XCMPLX_1;
schemes FINSEQ_2, NAT_1, BINARITH;
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;
Lm1: now let k; k <= k+1 by NAT_1:29; hence k-1 <= k by REAL_1:86; end;
Lm2: 2-1=1;
Lm3:j-'j+1 = 1
proof
j-'j=j-j by SCMFSA_7:3 .= 0 by XCMPLX_1:14;
hence thesis;
end;
Lm4:for n st 1 <= n & n <= 2 holds n = 1 or n = 2
proof
let n; assume A1:1<=n & n<=2;
per cases by A1,REAL_1:def 5;
suppose n=1;
hence thesis;
suppose n>1;
then n >= 1+1 by NAT_1:38;
hence thesis by A1,AXIOMS:21;
end;
theorem Th1: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
proof
let A be closed-interval Subset of REAL;
let D be Element of divs A;
assume A1:vol(A) <>0;
assume A2:for i st i in dom D holds vol(divset(D,i))<=0;
A3:i in dom D implies vol(divset(D,i))=0
proof
assume i in dom D;
then vol(divset(D,i)) <= 0 by A2;
hence thesis by INTEGRA1:11;
end;
A4:i in dom D implies sup divset(D,i)=inf divset(D,i)
proof
assume i in dom D;
then vol(divset(D,i))=0 by A3;
then sup divset(D,i)-inf divset(D,i)=0 by INTEGRA1:def 6;
hence thesis by XCMPLX_1:15;
end;
A5:len D in dom D by SCMFSA_7:12;
len D = 1
proof
assume A6:len D <> 1;
then A7:inf divset(D,len D)=D.(len D-1) & sup divset(D,len D)=D.(len D)
by A5,INTEGRA1:def 5;
A8: len D-1 in dom D & len D-1 in NAT by A5,A6,INTEGRA1:9;
len D < len D+1 by NAT_1:38;
then len D-1 < len D by REAL_1:84;
then inf divset(D,len D)<sup divset(D,len D) by A5,A7,A8,GOBOARD1:def 1;
hence contradiction by A4,A5;
end;
then inf divset(D,len D)=inf A & sup divset(D,len D)=D.(len D)
by A5,INTEGRA1:def 5;
then inf divset(D,len D)=inf A & sup divset(D,len D)=sup A
by INTEGRA1:def 2;
then sup A = inf A+0 by A4,A5;
then sup A- inf A = 0 by XCMPLX_1:26;
hence contradiction by A1,INTEGRA1:def 6;
end;
theorem Th2: 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)
proof
let A be closed-interval Subset of REAL;
let D be Element of divs A;
assume x in A;
then A1:inf A <= x & x <= sup A by INTEGRA2:1;
rng D <> {};
then A2:1 in dom D by FINSEQ_3:34;
per cases;
suppose x in rng D;
then consider j such that
A3: j in dom D & D.j = x by PARTFUN1:26;
x in divset(D,j)
proof
per cases;
suppose j=1;
then A4: inf divset(D,j)=inf A & sup divset(D,j)=D.j by A3,INTEGRA1:def 5;
consider a,b such that
A5: a <= b & a=inf divset(D,j) & b=sup divset(D,j) by INTEGRA1:4;
thus thesis by A3,A4,A5,INTEGRA2:1;
suppose j<>1;
then A6: sup divset(D,j)=D.j by A3,INTEGRA1:def 5;
consider a,b such that
A7: a <= b & a=inf divset(D,j) & b=sup divset(D,j) by INTEGRA1:4;
thus thesis by A3,A6,A7,INTEGRA2:1;
end;
hence thesis by A3;
suppose A8:not x in rng D;
defpred MIN[Nat] means x < sup divset(D,$1) & $1 in dom D;
defpred MAX[Nat] means x >= inf divset(D,$1) & $1 in dom D;
A9:len D in dom D by SCMFSA_7:12;
sup divset(D,len D)=D.(len D)
proof
per cases;
suppose len D=1;
hence thesis by A9,INTEGRA1:def 5;
suppose len D<>1;
hence thesis by A9,INTEGRA1:def 5;
end;
then A10: sup divset(D,len D) = sup A by INTEGRA1:def 2;
x < sup divset(D,len D)
proof
x <> sup A
proof
assume x = sup A;
then x = D.(len D) by INTEGRA1:def 2;
hence contradiction by A8,A9,FUNCT_1:def 5;
end;
hence thesis by A1,A10,REAL_1:def 5;
end;
then A11: ex k st MIN[k] by A9;
consider k such that
A12:MIN[k] & for n st MIN[n] holds k <= n from Min(A11);
inf divset(D,1)=inf A by A2,INTEGRA1:def 5;
then A13: ex k st MAX[k] by A1,A2;
A14: for k holds MAX[k] implies k <= len D by FINSEQ_3:27;
consider j such that
A15:MAX[j] & for n st MAX[n] holds n <= j from Max(A14,A13);
k=j
proof
assume A16:k<>j;
now per cases by A16,AXIOMS:21;
suppose A17:k < j;
A18: 1 <= k & k <= len D by A12,FINSEQ_3:27;
then A19: j-1 in dom D & j-1 in NAT by A15,A17,INTEGRA1:9;
A20: sup divset(D,k)=D.k
proof
per cases;
suppose k=1;
hence thesis by A12,INTEGRA1:def 5;
suppose k<>1;
hence thesis by A12,INTEGRA1:def 5;
end;
D.(j-1) <= x by A15,A17,A18,INTEGRA1:def 5;
then D.(j-1) < D.k by A12,A20,AXIOMS:22;
then j-1 < k by A12,A19,GOBOARD2:18;
then j < k+1 by REAL_1:84;
hence contradiction by A17,NAT_1:38;
suppose A21:k > j;
x < sup divset(D,j)
proof
assume A22:x >= sup divset(D,j);
A23: sup divset(D,j)=D.j
proof
per cases;
suppose j=1;
hence thesis by A15,INTEGRA1:def 5;
suppose j<>1;
hence thesis by A15,INTEGRA1:def 5;
end;
A24: j+1 in dom D & j+1 > 1
proof
A25: 1 <= j & k <= len D by A12,A15,FINSEQ_3:27;
j < j+1 & j+1 <= k by A21,NAT_1:38;
then 1 <= j+1 & j+1 <= len D by A25,AXIOMS:22;
hence j+1 in dom D by FINSEQ_3:27;
thus thesis by A25,NAT_1:38;
end;
then inf divset(D,j+1) = D.(j+1-1) by INTEGRA1:def 5 .=D.j
by XCMPLX_1:26;
then j+1 <= j by A15,A22,A23,A24;
hence contradiction by NAT_1:38;
end;
hence contradiction by A12,A15,A21;
end;
hence contradiction;
end;
then x in divset(D,k) & k in dom D by A12,A15,INTEGRA2:1;
hence thesis;
end;
theorem Th3: 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
proof
let A be closed-interval Subset of REAL;
let D1,D2 be Element of divs A;
consider D being FinSequence of REAL such that
A1:rng D = rng(D1^D2) & len D = card rng(D1^D2) & D is increasing
by GOBOARD2:21;
reconsider D as increasing FinSequence of REAL by A1;
D1^D2 <> {} by FINSEQ_1:48;
then rng D <> {} by A1,FINSEQ_1:27;
then reconsider D as non empty increasing FinSequence of REAL by FINSEQ_1:27
;
A2:rng(D1^D2) = rng D1 \/ rng D2 by FINSEQ_1:44;
rng D1 c= A & rng D2 c= A by INTEGRA1:def 2;
then A3:rng D c= A by A1,A2,XBOOLE_1:8;
A4:rng D1 c= rng(D1^D2) by A2,XBOOLE_1:7;
A5:rng D2 c= rng(D1^D2) by A2,XBOOLE_1:7;
D.(len D) = sup A
proof
assume A6:D.(len D) <> sup A;
A7: len D in dom D by SCMFSA_7:12;
then D.(len D) in rng D by FUNCT_1:def 5;
then D.(len D) <= sup A by A3,INTEGRA2:1;
then A8: D.(len D) < sup A by A6,REAL_1:def 5;
A9: D1.(len D1) = sup A by INTEGRA1:def 2;
len D1 in dom D1 by SCMFSA_7:12;
then D1.(len D1) in rng D1 by FUNCT_1:def 5;
then consider k such that
A10: k in dom D & D1.(len D1)=D.k by A1,A4,PARTFUN1:26;
k > len D by A7,A8,A9,A10,GOBOARD2:18;
hence contradiction by A10,FINSEQ_3:27;
end;
then D is DivisionPoint of A by A3,INTEGRA1:def 2;
then reconsider D as Element of divs A by INTEGRA1:def 3;
take D;
A11:card rng D1 <= len D by A1,A4,CARD_1:80;
D1 is one-to-one by JORDAN7:17;
then len D1 <= len D by A11,FINSEQ_4:77;
hence D1 <= D by A1,A4,INTEGRA1:def 20;
A12:card rng D2 <= len D by A1,A5,CARD_1:80;
D2 is one-to-one by JORDAN7:17;
then len D2 <= len D by A12,FINSEQ_4:77;
hence D2 <= D by A1,A5,INTEGRA1:def 20;
thus thesis by A1,FINSEQ_1:44;
end;
theorem Th4: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)
proof
let A be closed-interval Subset of REAL;
let D,D1 be Element of divs A;
assume A1:delta(D1)<min rng upper_volume(chi(A,A),D);
let x,y,i;
assume A2:i in dom D1;
assume A3:x in rng D /\ divset(D1,i);
assume A4:y in rng D /\ divset(D1,i);
assume A5:x<>y;
x in rng D by A3,XBOOLE_0:def 3;
then consider n such that A6:n in dom D & x=D.n by PARTFUN1:26;
y in rng D by A4,XBOOLE_0:def 3;
then consider m such that A7:m in dom D & y=D.m by PARTFUN1:26;
A8:abs( D.n-D.m ) >= min rng upper_volume(chi(A,A),D)
proof
per cases by A5,A6,A7,AXIOMS:21;
suppose n<m;
then A9: n+1<=m by NAT_1:38;
n in Seg len D & m in Seg len D by A6,A7,FINSEQ_1:def 3;
then A10: 1<=n & m<=len D by FINSEQ_1:3;
then 1<=n+1 & n+1<=len D by A9,AXIOMS:22,NAT_1:37;
then A11: n+1 in Seg len D by FINSEQ_1:3;
then A12: n+1 in dom D by FINSEQ_1:def 3;
-abs( D.n-D.m ) <= D.n-D.m by ABSVALUE:11;
then A13: abs( D.n-D.m ) >= -(D.n-D.m) by REAL_2:110;
D.m>=D.(n+1) by A7,A9,A12,GOBOARD2:18;
then D.n-D.m <= D.n-D.(n+1) by REAL_2:106;
then -(D.n-D.m) >= -(D.n-D.(n+1)) by REAL_1:50;
then A14: -(D.n-D.m) >= D.(n+1)-D.n by XCMPLX_1:143;
A15: D.(n+1)-D.n=(upper_volume(chi(A,A),D)).(n+1)
proof
n+1 <> 1 by A10,NAT_1:38;
then A16: inf divset(D,n+1)=D.((n+1)-1)
& sup divset(D,n+1)=D.(n+1) by A12,INTEGRA1:def 5;
(n+1)-1=n by XCMPLX_1:26;
then vol(divset(D,n+1))=D.(n+1)-D.n by A16,INTEGRA1:def 6;
hence thesis by A11,INTEGRA1:22;
end;
n+1 in Seg len upper_volume(chi(A,A),D) by A11,INTEGRA1:def 7;
then n+1 in dom upper_volume(chi(A,A),D) by FINSEQ_1:def 3;
then (upper_volume(chi(A,A),D)).(n+1) in rng upper_volume(chi(A,A),D)
by FUNCT_1:def 5;
then D.(n+1)-D.n>=min rng upper_volume(chi(A,A),D) by A15,SFMASTR3:def 1
;
then -(D.n-D.m) >= min rng upper_volume(chi(A,A),D) by A14,AXIOMS:22;
hence thesis by A13,AXIOMS:22;
suppose n>m;
then A17: m+1<=n by NAT_1:38;
n in Seg len D & m in Seg len D by A6,A7,FINSEQ_1:def 3;
then A18: 1<=m & n<=len D by FINSEQ_1:3;
then A19: 1<=m+1 & m+1<=len D by A17,AXIOMS:22,NAT_1:37;
then A20: m+1 in Seg len D by FINSEQ_1:3;
A21: m+1 in dom D by A19,FINSEQ_3:27;
A22: abs( D.n-D.m ) >= D.n-D.m by ABSVALUE:11;
D.(m+1)<=D.n by A6,A17,A21,GOBOARD2:18;
then A23: D.n-D.m >= D.(m+1)-D.m by REAL_1:49;
A24: D.(m+1)-D.m=(upper_volume(chi(A,A),D)).(m+1)
proof
1 < m+1 by A18,NAT_1:38;
then A25: inf divset(D,m+1)=D.((m+1)-1)
& sup divset(D,m+1)=D.(m+1) by A21,INTEGRA1:def 5;
(m+1)-1=m by XCMPLX_1:26;
then vol(divset(D,m+1))=D.(m+1)-D.m by A25,INTEGRA1:def 6;
hence thesis by A20,INTEGRA1:22;
end;
m+1 in Seg len upper_volume(chi(A,A),D) by A20,INTEGRA1:def 7;
then m+1 in dom upper_volume(chi(A,A),D) by FINSEQ_1:def 3;
then (upper_volume(chi(A,A),D)).(m+1) in rng upper_volume(chi(A,A),D)
by FUNCT_1:def 5;
then D.(m+1)-D.m>=min rng upper_volume(chi(A,A),D) by A24,SFMASTR3:def 1
;
then D.n-D.m >= min rng upper_volume(chi(A,A),D) by A23,AXIOMS:22;
hence thesis by A22,AXIOMS:22;
end;
abs (D.n-D.m) <= delta D1
proof
per cases by A5,A6,A7,AXIOMS:21;
suppose n<m;
then D.n<D.m by A6,A7,GOBOARD1:def 1;
then D.n-D.m<0 by REAL_2:105;
then A26: abs( D.n-D.m )=-(D.n-D.m) by ABSVALUE:def 1 .= D.m-D.n by XCMPLX_1:
143;
D.n in divset(D1,i) by A3,A6,XBOOLE_0:def 3;
then A27: D.n >= inf divset(D1,i) by INTEGRA2:1;
D.m in divset(D1,i) by A4,A7,XBOOLE_0:def 3;
then D.m <= sup divset(D1,i) by INTEGRA2:1;
then A28: D.m-inf divset(D1,i)<= sup divset(D1,i)-inf divset(D1,i) by REAL_1:
49;
D.m-D.n <= D.m-inf divset(D1,i) by A27,REAL_2:106;
then D.m-D.n <= sup divset(D1,i)-inf divset(D1,i) by A28,AXIOMS:22;
then A29: D.m-D.n <= vol(divset(D1,i)) by INTEGRA1:def 6;
A30: i in Seg len D1 by A2,FINSEQ_1:def 3;
then A31: D.m-D.n <= upper_volume(chi(A,A),D1).i by A29,INTEGRA1:22;
i in Seg len upper_volume(chi(A,A),D1) by A30,INTEGRA1:def 7;
then i in dom upper_volume(chi(A,A),D1) by FINSEQ_1:def 3;
then upper_volume(chi(A,A),D1).i in rng upper_volume(chi(A,A),D1)
by FUNCT_1:def 5;
then upper_volume(chi(A,A),D1).i <= max rng upper_volume(chi(A,A),D1)
by PRE_CIRC:def 1;
then upper_volume(chi(A,A),D1).i<=delta(D1) by INTEGRA1:def 19;
hence thesis by A26,A31,AXIOMS:22;
suppose n>m;
then D.n>D.m by A6,A7,GOBOARD1:def 1;
then D.n-D.m>0 by SQUARE_1:11;
then A32: abs( D.n-D.m )=D.n-D.m by ABSVALUE:def 1;
D.m in divset(D1,i) by A4,A7,XBOOLE_0:def 3;
then A33: D.m >= inf divset(D1,i) by INTEGRA2:1;
D.n in divset(D1,i) by A3,A6,XBOOLE_0:def 3;
then D.n <= sup divset(D1,i) by INTEGRA2:1;
then A34: D.n-inf divset(D1,i)<= sup divset(D1,i)-inf divset(D1,i) by REAL_1:
49;
D.n-D.m <= D.n-inf divset(D1,i) by A33,REAL_2:106;
then D.n-D.m <= sup divset(D1,i)-inf divset(D1,i) by A34,AXIOMS:22;
then A35: D.n-D.m <= vol(divset(D1,i)) by INTEGRA1:def 6;
A36: i in Seg len D1 by A2,FINSEQ_1:def 3;
then A37: D.n-D.m <= upper_volume(chi(A,A),D1).i by A35,INTEGRA1:22;
i in Seg len upper_volume(chi(A,A),D1) by A36,INTEGRA1:def 7;
then i in dom upper_volume(chi(A,A),D1) by FINSEQ_1:def 3;
then upper_volume(chi(A,A),D1).i in rng upper_volume(chi(A,A),D1)
by FUNCT_1:def 5;
then upper_volume(chi(A,A),D1).i <= max rng upper_volume(chi(A,A),D1)
by PRE_CIRC:def 1;
then upper_volume(chi(A,A),D1).i<=delta(D1) by INTEGRA1:def 19;
hence thesis by A32,A37,AXIOMS:22;
end;
hence contradiction by A1,A8,AXIOMS:22;
end;
theorem Th5:
for p,q st rng p = rng q & p is increasing & q is increasing holds p = q
proof
let p,q;
assume A1:rng p = rng q;
assume A2:p is increasing & q is increasing;
then p is one-to-one & q is one-to-one by JORDAN7:17;
then len p = len q by A1,RLVECT_1:106;
hence thesis by A1,A2,GOBOARD2:22;
end;
theorem Th6:
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
proof
let A be closed-interval Subset of REAL;
let D,D1 be Element of divs A;
assume A1:D <= D1 & i in dom D & j in dom D & i <= j;
then A2:D.i = D1.indx(D1,D,i) & indx(D1,D,i) in dom D1 by INTEGRA1:def 21;
A3:D.j = D1.indx(D1,D,j) & indx(D1,D,j) in dom D1 by A1,INTEGRA1:def 21;
D.i <= D.j by A1,GOBOARD2:18;
hence thesis by A2,A3,GOBOARD1:def 1;
end;
theorem Th7: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)
proof
let A be closed-interval Subset of REAL;
let D,D1 be Element of divs A;
assume A1:D <= D1 & i in dom D & j in dom D & i < j;
then A2:D.i = D1.indx(D1,D,i) & indx(D1,D,i) in dom D1 by INTEGRA1:def 21;
A3:D.j = D1.indx(D1,D,j) & indx(D1,D,j) in dom D1 by A1,INTEGRA1:def 21;
D.i < D.j by A1,GOBOARD1:def 1;
hence thesis by A2,A3,GOBOARD2:18;
end;
theorem Th8: for A be closed-interval Subset of REAL,
D be Element of divs A holds delta(D) >= 0
proof
let A be closed-interval Subset of REAL;
let D be Element of divs A;
consider y such that
A1:y in rng D by SUBSET_1:10;
consider n such that
A2:n in dom D & y=D.n by A1,PARTFUN1:26;
A3:n in Seg len D by A2,FINSEQ_1:def 3;
then vol(divset(D,n))=upper_volume(chi(A,A),D).n by INTEGRA1:22;
then A4:upper_volume(chi(A,A),D).n >= 0 by INTEGRA1:11;
n in Seg len upper_volume(chi(A,A),D) by A3,INTEGRA1:def 7;
then n in dom upper_volume(chi(A,A),D) by FINSEQ_1:def 3;
then upper_volume(chi(A,A),D).n in rng upper_volume(chi(A,A),D)
by FUNCT_1:def 5;
then upper_volume(chi(A,A),D).n <= max rng upper_volume(chi(A,A),D)
by PRE_CIRC:def 1;
hence thesis by A4,INTEGRA1:def 19;
end;
Lm5:a+b-(d+e) = (a-d)+(b-e)
proof
a+b-(d+e)=a+b-d-e by XCMPLX_1:36
.=a-d+b-e by XCMPLX_1:29;
hence thesis by XCMPLX_1:29;
end;
Lm6:for A be closed-interval Subset of REAL, g be Function of A,REAL st
g is_bounded_on A holds sup rng g >= inf rng g
proof
let A be closed-interval Subset of REAL;
let g be Function of A,REAL;
assume A1: g is_bounded_on A;
dom g <> {} by FUNCT_2:def 1;
then A2: rng g <> {} by RELAT_1:65;
g is_bounded_below_on A & g is_bounded_above_on A by A1,RFUNCT_1:def 11;
then rng g is bounded_above & rng g is bounded_below by INTEGRA1:13,15;
then rng g is bounded by SEQ_4:def 3;
hence thesis by A2,SEQ_4:24;
end;
Lm7:for A,B be closed-interval Subset of REAL,
f be Function of A,REAL st f is_bounded_on A & B c= A holds
inf rng(f|B) >= inf rng f & inf rng f <= sup rng(f|B) &
sup rng(f|B) <= sup rng f & inf rng(f|B) <= sup rng f
proof
let A,B be closed-interval Subset of REAL,
f be Function of A,REAL;
assume A1: f is_bounded_on A & B c= A;
then f is_bounded_above_on A & f is_bounded_below_on A
by RFUNCT_1:def 11;
then A2:rng f is bounded_above & rng f is bounded_below by INTEGRA1:13,15;
consider x such that
A3:x in B by SUBSET_1:10;
B c=dom f by A1,FUNCT_2:def 1;
then A4:dom(f|B)=B by RELAT_1:91;
then A5:(f|B).x in rng(f|B) by A3,FUNCT_1:def 5;
A6:rng(f|B) <> {} by A4,RELAT_1:65;
A7:rng(f|B) c= rng f by FUNCT_1:76;
then A8:rng(f|B) is bounded_above & rng(f|B) is bounded_below
by A2,RCOMP_1:3,4;
thus A9:inf rng(f|B) >= inf rng f by A2,A6,A7,PSCOMP_1:12;
A10:inf rng(f|B)<=(f|B).x by A5,A8,SEQ_4:def 5;
sup rng(f|B)>=(f|B).x by A5,A8,SEQ_4:def 4;
then A11: inf rng(f|B) <= sup rng(f|B) by A10,AXIOMS:22;
hence sup rng(f|B) >= inf rng f by A9,AXIOMS:22;
thus sup rng(f|B) <= sup rng f by A2,A6,A7,PSCOMP_1:13;
hence thesis by A11,AXIOMS:22;
end;
Lm8: for A be closed-interval Subset of REAL,
D1 be Element of divs A st j in dom D1 holds
vol(divset(D1,j)) <= delta(D1)
proof
let A be closed-interval Subset of REAL,
D1 be Element of divs A;
assume j in dom D1;
then A1:j in Seg len D1 by FINSEQ_1:def 3;
then j in Seg len upper_volume(chi(A,A),D1) by INTEGRA1:def 7;
then j in dom upper_volume(chi(A,A),D1) by FINSEQ_1:def 3;
then upper_volume(chi(A,A),D1).j in rng upper_volume(chi(A,A),D1)
by FUNCT_1:def 5;
then upper_volume(chi(A,A),D1).j <= max rng upper_volume(chi(A,A),D1)
by PRE_CIRC:def 1;
then vol(divset(D1,j)) <= max rng upper_volume(chi(A,A),D1) by A1,INTEGRA1:22
;
hence thesis by INTEGRA1:def 19;
end;
Lm9:for A be closed-interval Subset of REAL, j1 be Nat,
D1,D2 be Element of divs A st
j1 = len D1 - 1 & x in divset(D1,len D1) & len D1 >= 2 &
D1 <= D2 & rng D2 = rng D1 \/ {x}
holds rng (D2|indx(D2,D1,j1)) = rng (D1|j1)
proof
let A be closed-interval Subset of REAL, j1 be Nat,
D1,D2 be Element of divs A;
assume A1:j1 = len D1 - 1 & x in divset(D1,len D1) & len D1 >= 2;
assume A2:D1<=D2 & rng D2 = rng D1 \/ {x};
A3: len D1 in dom D1 & len D2 in dom D2 by SCMFSA_7:12;
A4: len D1 <> 1 by A1;
then A5:len D1-1 in NAT & len D1-1 in dom D1 by A3,INTEGRA1:9;
inf divset(D1,len D1) <= x & x <= sup divset(D1,len D1)
by A1,INTEGRA2:1;
then A6:D1.j1 <= x & x <= D1.(len D1) by A1,A3,A4,INTEGRA1:def 5;
A7:indx(D2,D1,j1) in dom D2 by A1,A2,A5,INTEGRA1:def 21;
then A8: 1 <= indx(D2,D1,j1) & indx(D2,D1,j1) <= len D2 by FINSEQ_3:27;
A9:j1 in dom D1 by A1,A3,A4,INTEGRA1:9;
then A10: 1 <= j1 & j1 <= len D1 by FINSEQ_3:27;
for x1 st x1 in rng(D2|indx(D2,D1,j1)) holds x1 in rng(D1|j1)
proof
let x1; assume x1 in rng(D2|indx(D2,D1,j1));
then consider k such that
A11: k in dom(D2|indx(D2,D1,j1)) & x1=(D2|indx(D2,D1,j1)).k by PARTFUN1:26;
k in Seg len(D2|indx(D2,D1,j1)) by A11,FINSEQ_1:def 3;
then A12: k in Seg indx(D2,D1,j1) by A8,TOPREAL1:3;
then A13: (D2|indx(D2,D1,j1)).k = D2.k & k in dom D2 by A7,RFINSEQ:19;
then A14: D2.k in rng D2 by FUNCT_1:def 5;
1 <= k & k <= indx(D2,D1,j1) by A12,FINSEQ_1:3;
then D2.k <= D2.indx(D2,D1,j1) by A7,A13,GOBOARD2:18;
then A15: D2.k <= D1.j1 by A1,A2,A5,INTEGRA1:def 21;
A16: len(D1|j1) = j1 by A10,TOPREAL1:3;
A17: D2.k in {x} implies D2.k = D1.j1
proof
assume D2.k in {x};
then D1.j1 <= D2.k by A6,TARSKI:def 1;
hence thesis by A15,AXIOMS:21;
end;
A18: D2.k in {x} implies D2.k in rng(D1|j1)
proof
assume A19:D2.k in {x};
j1 in dom(D1|j1) by A10,A16,FINSEQ_3:27;
then A20: (D1|j1).j1 in rng(D1|j1) by FUNCT_1:def 5;
j1 in Seg j1 by A10,FINSEQ_1:3;
hence thesis by A9,A17,A19,A20,RFINSEQ:19;
end;
D2.k in rng D1 implies D2.k in rng(D1|j1)
proof
assume D2.k in rng D1;
then consider m such that
A21: m in dom D1 & D2.k = D1.m by PARTFUN1:26;
m in Seg len D1 by A21,FINSEQ_1:def 3;
then A22: 1 <= m & m <= j1 by A9,A15,A21,FINSEQ_1:3,GOBOARD1:def 1;
then A23: m in dom (D1|j1) by A16,FINSEQ_3:27;
m in Seg j1 by A22,FINSEQ_1:3;
then D2.k = (D1|j1).m by A9,A21,RFINSEQ:19;
hence thesis by A23,FUNCT_1:def 5;
end;
hence thesis by A2,A7,A11,A12,A14,A18,RFINSEQ:19,XBOOLE_0:def 2;
end;
then A24: rng(D2|indx(D2,D1,j1)) c= rng (D1|j1) by TARSKI:def 3;
for x1 st x1 in rng(D1|j1) holds x1 in rng(D2|indx(D2,D1,j1))
proof
let x1; assume x1 in rng(D1|j1);
then consider k such that
A25: k in dom(D1|j1) & x1=(D1|j1).k by PARTFUN1:26;
k in Seg len(D1|j1) by A25,FINSEQ_1:def 3;
then A26: k in Seg j1 by A10,TOPREAL1:3;
then A27: (D1|j1).k = D1.k & k in dom D1 by A9,RFINSEQ:19;
then D1.k in rng D1 by FUNCT_1:def 5;
then x1 in rng D2 by A2,A25,A27,XBOOLE_0:def 2;
then consider n such that
A28: n in dom D2 & x1=D2.n by PARTFUN1:26;
A29: indx(D2,D1,k) in dom D2 & D2.indx(D2,D1,k)=D2.n
by A2,A25,A27,A28,INTEGRA1:def 21;
k <= j1 by A26,FINSEQ_1:3;
then D1.k <= D1.j1 by A1,A5,A27,GOBOARD2:18;
then D2.indx(D2,D1,k) <= D1.j1 by A2,A27,INTEGRA1:def 21;
then D2.indx(D2,D1,k)<=D2.indx(D2,D1,j1)
by A1,A2,A5,INTEGRA1:def 21;
then A30: n <= indx(D2,D1,j1) by A7,A28,A29,GOBOARD1:def 1;
1 <= n by A28,FINSEQ_3:27;
then A31: n in Seg indx(D2,D1,j1) by A30,FINSEQ_1:3;
then A32: D2.n = (D2|indx(D2,D1,j1)).n by A7,RFINSEQ:19;
n in Seg len(D2|indx(D2,D1,j1)) by A8,A31,TOPREAL1:3;
then n in dom(D2|indx(D2,D1,j1)) by FINSEQ_1:def 3;
hence thesis by A28,A32,FUNCT_1:def 5;
end;
then rng(D1|j1) c= rng(D2|indx(D2,D1,j1)) by TARSKI:def 3;
hence thesis by A24,XBOOLE_0:def 10;
end;
theorem Th9:
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)
proof
let A be closed-interval Subset of REAL;
let g be Function of A,REAL;
let D1,D2 be Element of divs A;
assume A1:x in divset(D1,len D1) & len D1 >= 2;
assume A2:D1<=D2 & rng D2 = rng D1 \/ {x};
assume A3:g is_bounded_on A;
deffunc PLg(Element of divs A,Nat) = (PartSums(lower_volume(g,$1))).$2;
deffunc LVg(Element of divs A) = lower_volume(g,$1);
set j = len D1;
A4:len D1 <> 0 & len D2 <> 0 by FINSEQ_1:25;
then A5:len D1 in Seg len D1 & len D2 in Seg len D2 by FINSEQ_1:5;
A6:len D1 in dom D1 & len D2 in dom D2 by SCMFSA_7:12;
A7:len D1 <> 1 by A1;
A8:sup rng g >= inf rng g by A3,Lm6;
A9:indx(D2,D1,j) in dom D2 & D2.indx(D2,D1,j)=D1.(len D1)
by A2,A6,INTEGRA1:def 21;
then A10:indx(D2,D1,j) in Seg len D2 by FINSEQ_1:def 3;
A11: indx(D2,D1,j) >= len lower_volume(g,D2)
proof
assume indx(D2,D1,j) < len lower_volume(g,D2);
then indx(D2,D1,j) < len D2 by INTEGRA1:def 8;
then A12:D1.(len D1) < D2.(len D2) by A6,A9,GOBOARD1:def 1;
A13:not D2.(len D2) in rng D1
proof
assume A14:D2.(len D2) in rng D1;
rng D1 c= A by INTEGRA1:def 2;
then inf A <= D2.(len D2) & D2.(len D2) <= sup A by A14,INTEGRA2:1;
hence contradiction by A12,INTEGRA1:def 2;
end;
D2.(len D2) in rng D2 by A6,FUNCT_1:def 5;
then D2.(len D2) in rng D1 or D2.(len D2) in {x} by A2,XBOOLE_0:def 2;
then D2.(len D2) = x by A13,TARSKI:def 1;
then D2.(len D2) <= sup divset(D1,len D1) by A1,INTEGRA2:1;
hence contradiction by A6,A7,A12,INTEGRA1:def 5;
end;
then A15:indx(D2,D1,j) in Seg len lower_volume(g,D2)
& indx(D2,D1,j) >= len lower_volume(g,D2) by A10,INTEGRA1:def 8;
A16:j in Seg len lower_volume(g,D1)
& j >= len lower_volume(g,D1) by A5,INTEGRA1:def 8;
A17:len D1-1 in NAT & len D1-1 in dom D1 by A6,A7,INTEGRA1:9;
reconsider j1=len D1-1 as Element of NAT by A6,A7,INTEGRA1:9;
A18:indx(D2,D1,j1) in dom D2 & 1 <= indx(D2,D1,j1) & indx(D2,D1,j1) <= len D2
proof
thus indx(D2,D1,j1) in dom D2 by A2,A17,INTEGRA1:def 21;
hence thesis by FINSEQ_3:27;
end;
then mid(D2,1,indx(D2,D1,j1)) is increasing by INTEGRA1:37;
then A19:D2|indx(D2,D1,j1) is increasing by A18,JORDAN3:25;
A20:j1 in dom D1 & 1 <= j1 & j1 <= len D1
proof
thus j1 in dom D1 by A6,A7,INTEGRA1:9;
hence thesis by FINSEQ_3:27;
end;
then mid(D1,1,j1) is increasing by INTEGRA1:37;
then A21:D1|j1 is increasing by A20,JORDAN3:25;
A22:rng (D2|indx(D2,D1,j1)) = rng (D1|j1) by A1,A2,Lm9;
then A23:D2|indx(D2,D1,j1)=D1|j1 by A19,A21,Th5;
A24:for k st 1 <= k & k <= j1 holds k=indx(D2,D1,k)
proof
let k; assume A25:1 <= k & k <= j1;
assume A26:k<>indx(D2,D1,k);
now per cases by A26,AXIOMS:21;
suppose A27:k > indx(D2,D1,k);
1 <= k & k <= len D1 by A20,A25,AXIOMS:22;
then A28: k in dom D1 by FINSEQ_3:27;
then A29: indx(D2,D1,k) in dom D2 & D1.k=D2.indx(D2,D1,k)
by A2,INTEGRA1:def 21;
then indx(D2,D1,k) in Seg len D2 by FINSEQ_1:def 3;
then A30: 1<=indx(D2,D1,k)&indx(D2,D1,k)<=indx(D2,D1,j1)
by A2,A20,A25,A28,Th6,FINSEQ_1:3;
then indx(D2,D1,k) in Seg indx(D2,D1,j1) by FINSEQ_1:3;
then A31: (D2|indx(D2,D1,j1)).indx(D2,D1,k)=D2.indx(D2,D1,k) by A18,RFINSEQ:
19;
A32: indx(D2,D1,k) < j1 by A25,A27,AXIOMS:22;
then indx(D2,D1,k) <= len D1 by A20,AXIOMS:22;
then indx(D2,D1,k) in dom D1 by A30,FINSEQ_3:27;
then A33: D1.k > D1.indx(D2,D1,k) by A27,A28,GOBOARD1:def 1;
indx(D2,D1,k) in Seg j1 by A30,A32,FINSEQ_1:3;
hence contradiction by A20,A23,A29,A31,A33,RFINSEQ:19;
suppose A34:k < indx(D2,D1,k);
k in Seg j1 by A25,FINSEQ_1:3;
then A35: D1.k = (D1|j1).k by A17,RFINSEQ:19;
1 <= k & k <= len D1 by A20,A25,AXIOMS:22;
then A36: k in dom D1 by FINSEQ_3:27;
then A37: indx(D2,D1,k) in dom D2 & D1.k=D2.indx(D2,D1,k)
by A2,INTEGRA1:def 21;
indx(D2,D1,k) <= indx(D2,D1,j1) & indx(D2,D1,k) in dom D2 &
indx(D2,D1,j1) in dom D2 by A2,A20,A25,A36,Th6;
then A38: k <= indx(D2,D1,j1) by A34,AXIOMS:22;
then k <= len D2 by A18,AXIOMS:22;
then k in dom D2 by A25,FINSEQ_3:27;
then A39: D2.k < D2.indx(D2,D1,k) by A34,A37,GOBOARD1:def 1;
k in Seg indx(D2,D1,j1) by A25,A38,FINSEQ_1:3;
hence contradiction by A18,A23,A35,A37,A39,RFINSEQ:19;
end;
hence contradiction;
end;
A40:len (D2|indx(D2,D1,j1))=len (D1|j1) by A19,A21,A22,Th5;
len (D2|indx(D2,D1,j1))=indx(D2,D1,j1) by A18,TOPREAL1:3;
then A41:indx(D2,D1,j1) =j1 by A20,A40,TOPREAL1:3;
j1 <= len D1 by A17,FINSEQ_3:27;
then j1 <= len lower_volume(g,D1) by INTEGRA1:def 8;
then A42:len(lower_volume(g,D1)|j1)=indx(D2,D1,j1) by A41,TOPREAL1:3;
indx(D2,D1,j1) in dom D2 by A2,A17,INTEGRA1:def 21;
then indx(D2,D1,j1) <= len D2 by FINSEQ_3:27;
then indx(D2,D1,j1) <= len lower_volume(g,D2) by INTEGRA1:def 8;
then A43:len(lower_volume(g,D1)|j1)=len(lower_volume(g,D2)|indx(D2,D1,j1))
by A42,TOPREAL1:3;
for k st 1 <= k & k <= len(lower_volume(g,D1)|j1) holds
(lower_volume(g,D1)|j1).k = (lower_volume(g,D2)|indx(D2,D1,j1)).k
proof
let k; assume A44:1 <= k & k <= len(lower_volume(g,D1)|j1);
A45: len(lower_volume(g,D1)) = len D1 by INTEGRA1:def 8;
then A46:1 <= k & k <= j1 by A20,A44,TOPREAL1:3;
then A47: k in Seg j1 by FINSEQ_1:3;
k <= len D1 by A20,A46,AXIOMS:22;
then A48:k in Seg len D1 by A44,FINSEQ_1:3;
A49:divset(D1,k)=divset(D2,indx(D2,D1,k))
proof
A50: divset(D1,k)=[. inf divset(D1,k), sup divset(D1,k) .] by INTEGRA1:5;
A51: k in dom D1 by A48,FINSEQ_1:def 3;
then A52: indx(D2,D1,k) in dom D2 & D1.k=D2.indx(D2,D1,k) by A2,INTEGRA1:def
21;
inf divset(D1,k)=inf divset(D2,indx(D2,D1,k)) &
sup divset(D1,k)=sup divset(D2,indx(D2,D1,k))
proof
per cases;
suppose A53:k=1;
then A54: inf divset(D1,k)=inf A & sup divset(D1,k)=D1.k by A51,INTEGRA1:def 5
;
indx(D2,D1,k)=1 by A20,A24,A53;
hence thesis by A52,A54,INTEGRA1:def 5;
suppose A55:k<>1;
then A56: inf divset(D1,k)=D1.(k-1) & sup divset(D1,k)=D1.k
by A51,INTEGRA1:def 5;
A57: k-1 in dom D1 & D1.(k-1) in A & k-1 in NAT by A51,A55,INTEGRA1:9;
reconsider k1=k-1 as Nat by A51,A55,INTEGRA1:9;
k <= k+1 by NAT_1:29;
then k1 <= k by REAL_1:86;
then A58: k1 <= j1 by A46,AXIOMS:22;
A59: 1 <= k1 by A57,FINSEQ_3:27;
indx(D2,D1,k)<>1 by A24,A46,A55;
then A60: inf divset(D2,indx(D2,D1,k))=D2.(indx(D2,D1,k)-1) &
sup divset(D2,indx(D2,D1,k))=D2.indx(D2,D1,k) by A52,INTEGRA1:def 5;
D2.(indx(D2,D1,k)-1)=D2.(k-1) by A24,A46
.= D2.indx(D2,D1,k1) by A24,A58,A59;
hence thesis by A2,A51,A56,A57,A60,INTEGRA1:def 21;
end;
hence thesis by A50,INTEGRA1:5;
end;
j1 in Seg len(lower_volume(g,D1)) by A20,A45,FINSEQ_1:def 3;
then j1 in dom(lower_volume(g,D1)) by FINSEQ_1:def 3;
then A61: (lower_volume(g,D1)|j1).k = lower_volume(g,D1).k by A47,RFINSEQ:19
.=(inf(rng(g|divset(D2,indx(D2,D1,k)))))*vol(divset(D2,indx(D2,D1,k)))
by A48,A49,INTEGRA1:def 8;
indx(D2,D1,k) in Seg j1 by A24,A46,A47;
then A62:indx(D2,D1,k) in Seg indx(D2,D1,j1) by A20,A24;
then 1<=indx(D2,D1,k) & indx(D2,D1,k)<=indx(D2,D1,j1) by FINSEQ_1:3;
then 1<=indx(D2,D1,k) & indx(D2,D1,k)<=len D2 by A18,AXIOMS:22;
then A63:indx(D2,D1,k) in Seg len D2 by FINSEQ_1:3;
indx(D2,D1,j1) in Seg len D2 by A18,FINSEQ_1:def 3;
then indx(D2,D1,j1) in Seg len lower_volume(g,D2) by INTEGRA1:def 8;
then A64:indx(D2,D1,j1) in dom lower_volume(g,D2) by FINSEQ_1:def 3;
(lower_volume(g,D2)|indx(D2,D1,j1)).k
=(lower_volume(g,D2)|indx(D2,D1,j1)).indx(D2,D1,k) by A24,A46
.=lower_volume(g,D2).indx(D2,D1,k) by A62,A64,RFINSEQ:19
.=(inf(rng(g|divset(D2,indx(D2,D1,k)))))*vol(divset(D2,indx(D2,D1,k)))
by A63,INTEGRA1:def 8;
hence thesis by A61;
end;
then A65:lower_volume(g,D2)|indx(D2,D1,j1)=lower_volume(g,D1)|j1
by A43,FINSEQ_1:18;
indx(D2,D1,j1) in Seg len D2 by A18,FINSEQ_1:def 3;
then A66:indx(D2,D1,j1) in Seg len lower_volume(g,D2) by INTEGRA1:def 8;
j1 in Seg len D1 by A20,FINSEQ_1:def 3;
then A67:j1 in Seg len lower_volume(g,D1) by INTEGRA1:def 8;
A68:PLg(D2,indx(D2,D1,j1))=Sum(lower_volume(g,D2)|indx(D2,D1,j1))
by A66,INTEGRA1:def 22
.=PLg(D1,j1) by A65,A67,INTEGRA1:def 22;
A69:indx(D2,D1,j1)+1 <= indx(D2,D1,len D1)
proof
len D1 < len D1+1 by NAT_1:38;
then j1 < len D1 by REAL_1:84;
then indx(D2,D1,j1) < indx(D2,D1,len D1) by A2,A6,A20,Th7;
hence thesis by NAT_1:38;
end;
A70:Sum mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,len D1))
-Sum mid(lower_volume(g,D1),len D1,len D1) <=
(sup rng g-inf rng g)*delta(D1)
proof
A71: 1 <= indx(D2,D1,j) & indx(D2,D1,j) <= len lower_volume(g,D2)
proof
indx(D2,D1,j) in dom D2 by A2,A6,INTEGRA1:def 21;
then indx(D2,D1,j) in Seg len D2 by FINSEQ_1:def 3;
then indx(D2,D1,j) in Seg len lower_volume(g,D2) by INTEGRA1:def 8;
hence thesis by FINSEQ_1:3;
end;
then A72: 1 <= indx(D2,D1,j1)+1 & indx(D2,D1,j1)+1 <= len lower_volume(g,D2)
by A18,A69,AXIOMS:22,NAT_1:38;
A73:indx(D2,D1,j)-indx(D2,D1,j1) <= 2
proof
assume A74:indx(D2,D1,j)-indx(D2,D1,j1) > 2;
set ID1=indx(D2,D1,j1)+1;
set ID2=ID1+1;
A75:indx(D2,D1,j1) < ID1 & ID1 < ID2 & ID2 < indx(D2,D1,j)
proof
thus indx(D2,D1,j1) < ID1 by NAT_1:38;
thus ID1 < ID2 by NAT_1:38;
indx(D2,D1,j1)+(1+1)<indx(D2,D1,j) by A74,REAL_1:86;
hence thesis by XCMPLX_1:1;
end;
A76:indx(D2,D1,j) in dom D2 by A2,A6,INTEGRA1:def 21;
then A77:indx(D2,D1,j) <= len D2 by FINSEQ_3:27;
A78:ID1 in dom D2
proof
A79: 1 <= ID1 & ID1 <= indx(D2,D1,j) by A18,A75,AXIOMS:22;
then ID1 <= len D2 by A77,AXIOMS:22;
hence thesis by A79,FINSEQ_3:27;
end;
A80:ID2 in dom D2
proof
A81: indx(D2,D1,j1) <= ID2 & ID2 <= len D2 by A75,A77,AXIOMS:22;
then 1 <= ID2 by A18,AXIOMS:22;
hence thesis by A81,FINSEQ_3:27;
end;
then A82:D2.indx(D2,D1,j1)<D2.ID1 & D2.ID1<D2.ID2 & D2.ID2<D2.indx(D2,D1,j)
by A18,A75,A76,A78,GOBOARD1:def 1;
A83: D2.ID1 in rng D2 & D2.ID2 in rng D2 by A78,A80,FUNCT_1:def 5;
A84: D1.j1 = D2.indx(D2,D1,j1) & D1.j = D2.indx(D2,D1,j)
by A2,A6,A20,INTEGRA1:def 21;
A85:D2.ID1 in {x} & D2.ID2 in {x}
proof
not(D2.ID1 in rng D1) & not(D2.ID2 in rng D1)
proof
assume A86:D2.ID1 in rng D1 or D2.ID2 in rng D1;
now per cases by A86;
suppose D2.ID1 in rng D1;
then consider n such that
A87: n in dom D1 & D1.n=D2.ID1 by PARTFUN1:26;
D2.indx(D2,D1,j1)<D2.ID1 & D2.ID1<D2.indx(D2,D1,j)
by A82,AXIOMS:22;
then j1<n & n<j by A6,A20,A84,A87,GOBOARD2:18;
then j<n+1 & n<j by REAL_1:84;
hence contradiction by NAT_1:38;
suppose D2.ID2 in rng D1;
then consider n such that
A88: n in dom D1 & D1.n=D2.ID2 by PARTFUN1:26;
D2.indx(D2,D1,j1)<D2.ID2 & D2.ID2<D2.indx(D2,D1,j)
by A82,AXIOMS:22;
then j1<n & n<j by A6,A20,A84,A88,GOBOARD2:18;
then j<n+1 & n<j by REAL_1:84;
hence contradiction by NAT_1:38;
end;
hence thesis;
end;
hence thesis by A2,A83,XBOOLE_0:def 2;
end;
then D2.ID1 = x by TARSKI:def 1;
then D2.ID1=D2.ID2 by A85,TARSKI:def 1;
hence contradiction by A75,A78,A80,GOBOARD2:19;
end;
1 <= indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 &
indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 <= 2
proof
A89: indx(D2,D1,j)-'(indx(D2,D1,j1)+1)
=indx(D2,D1,j)-(indx(D2,D1,j1)+1) by A69,SCMFSA_7:3;
then indx(D2,D1,j)-'(indx(D2,D1,j1)+1) >= 0 by A69,SQUARE_1:12;
then indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 >= 0+1 by AXIOMS:24;
hence indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 >= 1;
indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1
=indx(D2,D1,j)-indx(D2,D1,j1)-1+1 by A89,XCMPLX_1:36
.=indx(D2,D1,j)-indx(D2,D1,j1)+1-1 by XCMPLX_1:29
.=indx(D2,D1,j)-indx(D2,D1,j1) by XCMPLX_1:26;
hence thesis by A73;
end;
then A90: 1 <= len mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)) &
len mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))<=2
by A69,A71,A72,JORDAN3:27;
A91: 1 <= j & j <= len lower_volume(g,D1) by A5,FINSEQ_1:3,INTEGRA1:def 8;
j-'j+1 = 1 by Lm3;
then A92: len mid(lower_volume(g,D1),j,j)=1 by A91,JORDAN3:27;
mid(lower_volume(g,D1),j,j).1 = lower_volume(g,D1).j by A91,JORDAN3:27;
then A93:mid(lower_volume(g,D1),j,j)=<*lower_volume(g,D1).j*> by A92,FINSEQ_1:
57;
indx(D2,D1,j1)+1 in Seg len lower_volume(g,D2) by A72,FINSEQ_1:3;
then A94:indx(D2,D1,j1)+1 in Seg len D2 by INTEGRA1:def 8;
A95:j in Seg len D1 by A4,FINSEQ_1:5;
now per cases by A90,Lm4;
suppose
A96: len mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))=1;
A97: indx(D2,D1,j1)+1=indx(D2,D1,j)
proof
len mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
= indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 by A69,A71,A72,JORDAN3:27;
then indx(D2,D1,j)-'(indx(D2,D1,j1)+1)=1-1 by A96,XCMPLX_1:26;
then indx(D2,D1,j)-(indx(D2,D1,j1)+1)=0 by A69,SCMFSA_7:3;
then indx(D2,D1,j)=0+(indx(D2,D1,j1)+1) by XCMPLX_1:27;
hence thesis;
end;
A98: divset(D2,indx(D2,D1,j))=divset(D1,j)
proof
inf divset(D1,j)=D2.indx(D2,D1,j1)
& sup divset(D1,j)=D2.indx(D2,D1,j)
proof
inf divset(D1,j)=D1.j1 & sup divset(D1,j)=D1.j
by A6,A7,INTEGRA1:def 5;
hence thesis by A2,A6,A20,INTEGRA1:def 21;
end;
then A99: divset(D1,j)=[. D2.indx(D2,D1,j1),D2.indx(D2,D1,j).] by INTEGRA1:5;
A100: indx(D2,D1,j)-1=indx(D2,D1,j1) by A97,XCMPLX_1:26;
A101: indx(D2,D1,j) in dom D2 by A2,A6,INTEGRA1:def 21;
indx(D2,D1,j)<>1 by A18,A97,NAT_1:38;
then inf divset(D2,indx(D2,D1,j))=D2.(indx(D2,D1,j)-1)
& sup divset(D2,indx(D2,D1,j))=D2.indx(D2,D1,j)
by A101,INTEGRA1:def 5;
hence thesis by A99,A100,INTEGRA1:5;
end;
mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)).1
=lower_volume(g,D2).(indx(D2,D1,j1)+1) by A71,A72,JORDAN3:27;
then mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=<*lower_volume(g,D2).(indx(D2,D1,j1)+1)*> by A96,FINSEQ_1:57;
then A102: Sum mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=lower_volume(g,D2).(indx(D2,D1,j1)+1) by RVSUM_1:103
.=(inf(rng(g|divset(D2,(indx(D2,D1,j1)+1)))))
*vol(divset(D2,(indx(D2,D1,j1)+1))) by A94,INTEGRA1:def 8
.=lower_volume(g,D1).j by A95,A97,A98,INTEGRA1:def 8
.=Sum mid(lower_volume(g,D1),j,j) by A93,RVSUM_1:103;
A103: delta(D1) >= 0 by Th8;
sup rng g - inf rng g >= 0 by A8,SQUARE_1:12;
then (sup rng g - inf rng g)*delta(D1) >= 0*delta(D1) by A103,AXIOMS:25;
hence Sum mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
-Sum mid(lower_volume(g,D1),j,j) <= (sup rng g-inf rng g)*delta(D1)
by A102,XCMPLX_1:14;
suppose
A104: len mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))=2;
A105: mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)).1
=lower_volume(g,D2).(indx(D2,D1,j1)+1) by A71,A72,JORDAN3:27;
mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)).2
=lower_volume(g,D2).(indx(D2,D1,j1)+2)
proof
A106: 2+(indx(D2,D1,j1)+1)>=0+1 by A72,REAL_1:55;
mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)).2
=LVg(D2).(2+(indx(D2,D1,j1)+1)-'1) by A69,A71,A72,A104,JORDAN3:27
.=LVg(D2).(2+(indx(D2,D1,j1)+1)-1) by A106,SCMFSA_7:3
.=LVg(D2).((indx(D2,D1,j1)+1)+(2-1)) by XCMPLX_1:29
.=LVg(D2).(indx(D2,D1,j1)+(1+1)) by XCMPLX_1:1;
hence thesis;
end;
then mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=<*lower_volume(g,D2).(indx(D2,D1,j1)+1),
lower_volume(g,D2).(indx(D2,D1,j1)+2)*> by A104,A105,FINSEQ_1:61;
then A107: Sum mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=lower_volume(g,D2).(indx(D2,D1,j1)+1)
+lower_volume(g,D2).(indx(D2,D1,j1)+2) by RVSUM_1:107;
A108: vol(divset(D1,j))
=vol(divset(D2,indx(D2,D1,j1)+1))+vol(divset(D2,indx(D2,D1,j1)+2))
proof
A109: inf divset(D1,j)=D2.indx(D2,D1,j1)&sup divset(D1,j)=D2.indx(D2,D1,j)
proof
inf divset(D1,j)=D1.j1 & sup divset(D1,j)=D1.j by A6,A7,INTEGRA1:def 5
;
hence thesis by A2,A6,A20,INTEGRA1:def 21;
end;
A110: indx(D2,D1,j)=indx(D2,D1,j1)+2
proof
indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1=2 by A69,A71,A72,A104,JORDAN3:27;
then indx(D2,D1,j)-(indx(D2,D1,j1)+1)+1=2 by A69,SCMFSA_7:3;
then indx(D2,D1,j)-indx(D2,D1,j1)-1+1=2 by XCMPLX_1:36;
then indx(D2,D1,j)-indx(D2,D1,j1)-(1-1)=2 by XCMPLX_1:37;
hence thesis by XCMPLX_1:27;
end;
A111: inf divset(D2,(indx(D2,D1,j1)+2))=D2.(indx(D2,D1,j1)+1)
& sup divset(D2,(indx(D2,D1,j1)+2))=D2.(indx(D2,D1,j1)+2)
& inf divset(D2,(indx(D2,D1,j1)+1))=D2.indx(D2,D1,j1)
& sup divset(D2,(indx(D2,D1,j1)+1))=D2.(indx(D2,D1,j1)+1)
proof
A112: indx(D2,D1,j1)+2 in dom D2 by A2,A6,A110,INTEGRA1:def 21;
indx(D2,D1,j1)+1 in Seg len lower_volume(g,D2) by A72,FINSEQ_1:3;
then indx(D2,D1,j1)+1 in Seg len D2 by INTEGRA1:def 8;
then A113: indx(D2,D1,j1)+1 in dom D2 by FINSEQ_1:def 3;
A114: indx(D2,D1,j1)+1 <> 1 by A18,NAT_1:38;
indx(D2,D1,j1)+1+1 > 1 by A72,NAT_1:38;
then A115: indx(D2,D1,j1)+(1+1) > 1 by XCMPLX_1:1;
A116: indx(D2,D1,j1)+2-1=indx(D2,D1,j1)+1 by Lm2,XCMPLX_1:29;
A117: indx(D2,D1,j1)+1-1=indx(D2,D1,j1)+(1-1) by XCMPLX_1:29
.=indx(D2,D1,j1)+0;
thus inf divset(D2,(indx(D2,D1,j1)+2))=D2.(indx(D2,D1,j1)+1)
& sup divset(D2,(indx(D2,D1,j1)+2))=D2.(indx(D2,D1,j1)+2)
by A112,A115,A116,INTEGRA1:def 5;
thus thesis by A113,A114,A117,INTEGRA1:def 5;
end;
vol(divset(D1,j))=sup divset(D1,j)-inf divset(D1,j) by INTEGRA1:def 6
.=D2.indx(D2,D1,j)-(D2.(indx(D2,D1,j1)+1)
-D2.(indx(D2,D1,j1)+1))-D2.indx(D2,D1,j1) by A109,XCMPLX_1:17
.=D2.(indx(D2,D1,j1)+2)-D2.(indx(D2,D1,j1)+1)
+D2.(indx(D2,D1,j1)+1)-D2.indx(D2,D1,j1) by A110,XCMPLX_1:37;
then vol(divset(D1,j))=vol(divset(D2,indx(D2,D1,j1)+2))
+D2.(indx(D2,D1,j1)+1)-D2.indx(D2,D1,j1) by A111,INTEGRA1:def 6
.=vol(divset(D2,indx(D2,D1,j1)+2))
+(sup divset(D2,indx(D2,D1,j1)+1)-inf divset(D2,indx(D2,D1,j1)+1))
by A111,XCMPLX_1:29;
hence thesis by INTEGRA1:def 6;
end;
then A118: lower_volume(g,D1).j=(inf(rng(g|divset(D1,j))))*
(vol(divset(D2,indx(D2,D1,j1)+1))+vol(divset(D2,indx(D2,D1,j1)+2)))
by A95,INTEGRA1:def 8;
A119: vol(divset(D2,indx(D2,D1,j1)+1))>=0 by INTEGRA1:11;
A120: vol(divset(D2,indx(D2,D1,j1)+2))>=0 by INTEGRA1:11;
A121: Sum mid(LVg(D2),indx(D2,D1,j1)+1,indx(D2,D1,j))-Sum mid(LVg(D1),j,j)
<=(sup rng g - inf rng g)*(vol(divset(D2,indx(D2,D1,j1)+2))
+vol(divset(D2,indx(D2,D1,j1)+1)))
proof
A122: indx(D2,D1,j) in dom D2 by A2,A6,INTEGRA1:def 21;
A123: indx(D2,D1,j)=indx(D2,D1,j1)+2
proof
indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1=2 by A69,A71,A72,A104,JORDAN3:27;
then indx(D2,D1,j)-(indx(D2,D1,j1)+1)+1=2 by A69,SCMFSA_7:3;
then indx(D2,D1,j)-indx(D2,D1,j1)-1+1=2 by XCMPLX_1:36;
then indx(D2,D1,j)-indx(D2,D1,j1)-(1-1)=2 by XCMPLX_1:37;
hence thesis by XCMPLX_1:27;
end;
then A124: indx(D2,D1,j1)+2 in Seg len D2 by A122,FINSEQ_1:def 3;
set ID1=indx(D2,D1,j1)+1, ID2=indx(D2,D1,j1)+2;
A125: Sum mid(LVg(D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=(inf rng(g|divset(D2,indx(D2,D1,j1)+2)))
*vol(divset(D2,indx(D2,D1,j1)+2))
+LVg(D2).(indx(D2,D1,j1)+1) by A107,A124,INTEGRA1:def 8
.=(inf rng(g|divset(D2,indx(D2,D1,j1)+2)))
*vol(divset(D2,indx(D2,D1,j1)+2))
+(inf rng(g|divset(D2,indx(D2,D1,j1)+1)))
*vol(divset(D2,indx(D2,D1,j1)+1)) by A94,INTEGRA1:def 8;
divset(D2,ID2)c=A by A122,A123,INTEGRA1:10;
then inf rng(g|divset(D2,ID2)) <= sup rng g by A3,Lm7;
then A126: (inf rng(g|divset(D2,ID2)))*vol(divset(D2,ID2))
<=(sup rng g)*vol(divset(D2,ID2)) by A120,AXIOMS:25;
ID1 in dom D2 by A94,FINSEQ_1:def 3;
then divset(D2,ID1) c= A by INTEGRA1:10;
then inf rng(g|divset(D2,ID1)) <= sup rng g by A3,Lm7;
then A127: (inf rng(g|divset(D2,ID1)))*vol(divset(D2,ID1))
<=(sup rng g)*vol(divset(D2,ID1)) by A119,AXIOMS:25;
divset(D1,j)c=A by A6,INTEGRA1:10;
then inf rng(g|divset(D1,j)) >= inf rng g by A3,Lm7;
then A128: (inf rng(g|divset(D1,j)))*vol(divset(D2,ID2))
>=(inf rng g)*vol(divset(D2,ID2))
& (inf rng(g|divset(D1,j)))*vol(divset(D2,ID1))
>=(inf rng g)*vol(divset(D2,ID1)) by A119,A120,AXIOMS:25;
Sum mid(LVg(D2),ID1,indx(D2,D1,j))
-(inf rng(g|divset(D2,ID1)))*vol(divset(D2,ID1))
<=(sup rng g)*vol(divset(D2,ID2)) by A125,A126,XCMPLX_1:26;
then Sum mid(LVg(D2),ID1,indx(D2,D1,j))
<=(sup rng g)*vol(divset(D2,ID2))
+(inf rng(g|divset(D2,ID1)))*vol(divset(D2,ID1)) by REAL_1:86;
then Sum mid(LVg(D2),ID1,indx(D2,D1,j))-(sup rng g)*vol(divset(D2,ID2))
<=(inf rng(g|divset(D2,ID1)))*vol(divset(D2,ID1)) by REAL_1:86;
then Sum mid(LVg(D2),ID1,indx(D2,D1,j))-(sup rng g)*vol(divset(D2,ID2))
<=(sup rng g)*vol(divset(D2,ID1)) by A127,AXIOMS:22;
then A129: Sum mid(LVg(D2),ID1,indx(D2,D1,j))<=(sup rng g)*vol(divset(D2,ID2))
+
(sup rng g)*vol(divset(D2,ID1)) by REAL_1:86;
set IR = (inf rng g)*vol(divset(D2,ID2));
Sum mid(LVg(D1),j,j)=(inf rng(g|divset(D1,j)))
*(vol(divset(D2,indx(D2,D1,j1)+1))
+vol(divset(D2,indx(D2,D1,j1)+2))) by A93,A118,RVSUM_1:103
.=(inf rng(g|divset(D1,j)))*vol(divset(D2,indx(D2,D1,j1)+2))
+(inf rng(g|divset(D1,j)))*vol(divset(D2,indx(D2,D1,j1)+1))
by XCMPLX_1:8;
then Sum mid(LVg(D1),j,j)-(inf rng(g|divset(D1,j)))*vol(divset(D2,ID1))
>=IR by A128,XCMPLX_1:26;
then Sum mid(LVg(D1),j,j)>=(inf rng(g|divset(D1,j)))*vol(divset(D2,ID1))
+IR by REAL_1:84;
then Sum mid(LVg(D1),j,j)-(inf rng g)*vol(divset(D2,ID2))
>=(inf rng(g|divset(D1,j)))*vol(divset(D2,ID1)) by REAL_1:84;
then Sum mid(LVg(D1),j,j)-(inf rng g)*vol(divset(D2,ID2))
>=(inf rng g)*vol(divset(D2,ID1)) by A128,AXIOMS:22;
then Sum mid(LVg(D1),j,j) >=IR+(inf rng g)*vol(divset(D2,ID1))
by REAL_1:84;
then Sum mid(LVg(D2),ID1,indx(D2,D1,j))-Sum mid(LVg(D1),j,j)
<=(sup rng g)*vol(divset(D2,ID2))+(sup rng g)*vol(divset(D2,ID1))
-(IR+(inf rng g)*vol(divset(D2,ID1)))
by A129,REAL_1:92;
then Sum mid(LVg(D2),ID1,indx(D2,D1,j))-Sum mid(LVg(D1),j,j)
<=((sup rng g)*vol(divset(D2,ID2))-(inf rng g)*vol(divset(D2,ID2)))
+((sup rng g)*vol(divset(D2,ID1))-(inf rng g)*vol(divset(D2,ID1)))
by Lm5;
then Sum mid(LVg(D2),ID1,indx(D2,D1,j))-Sum mid(LVg(D1),j,j)
<=(sup rng g - inf rng g)*vol(divset(D2,ID2))
+((sup rng g)*vol(divset(D2,ID1))-(inf rng g)*vol(divset(D2,ID1)))
by XCMPLX_1:40;
then Sum mid(LVg(D2),ID1,indx(D2,D1,j))-Sum mid(LVg(D1),j,j)
<=(sup rng g - inf rng g)*vol(divset(D2,ID2))
+(sup rng g - inf rng g)*vol(divset(D2,ID1)) by XCMPLX_1:40;
hence thesis by XCMPLX_1:8;
end;
A130: vol(divset(D1,j)) <= delta(D1) by A6,Lm8;
sup rng g - inf rng g >= 0 by A8,SQUARE_1:12;
then (sup rng g - inf rng g)*(vol(divset(D1,j)))
<=(sup rng g - inf rng g)*delta(D1) by A130,AXIOMS:25;
hence thesis by A108,A121,AXIOMS:22;
end;
hence thesis;
end;
A131:PLg(D2,indx(D2,D1,j1))
+Sum mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=PLg(D2,indx(D2,D1,j))
proof
indx(D2,D1,j) in dom D2 by A2,A6,INTEGRA1:def 21;
then A132: indx(D2,D1,j) in Seg len D2 by FINSEQ_1:def 3;
then A133:1 <= indx(D2,D1,j) & indx(D2,D1,j) <= len D2 by FINSEQ_1:3;
then A134: indx(D2,D1,j) <= len LVg(D2) by INTEGRA1:def 8;
A135: indx(D2,D1,j) in Seg len LVg(D2) by A132,INTEGRA1:def 8;
A136: indx(D2,D1,j1) < indx(D2,D1,j) by A69,NAT_1:38;
indx(D2,D1,j1) in Seg len D2 by A18,FINSEQ_1:def 3;
then indx(D2,D1,j1) in Seg len LVg(D2) by INTEGRA1:def 8;
then PLg(D2,indx(D2,D1,j1))
=Sum(LVg(D2)|indx(D2,D1,j1)) by INTEGRA1:def 22;
then PLg(D2,indx(D2,D1,j1))
+Sum mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=Sum(LVg(D2)|indx(D2,D1,j1)
^mid(LVg(D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))) by RVSUM_1:105
.=Sum(mid(LVg(D2),1,indx(D2,D1,j1))
^mid(LVg(D2),indx(D2,D1,j1)+1,indx(D2,D1,j))) by A18,JORDAN3:25
.=Sum(mid(LVg(D2),1,indx(D2,D1,j))) by A18,A134,A136,INTEGRA2:4
.=Sum(LVg(D2)|indx(D2,D1,j)) by A133,JORDAN3:25;
hence thesis by A135,INTEGRA1:def 22;
end;
PLg(D1,j1)+Sum mid(lower_volume(g,D1),j,j)=PLg(D1,j)
proof
A137: 1 <= j & j <= len LVg(D1) by A5,FINSEQ_1:3,INTEGRA1:def 8;
A138: j in Seg len LVg(D1) by A5,INTEGRA1:def 8;
A139: j1+1=j by XCMPLX_1:27;
j < j+1 by NAT_1:38;
then A140: j1 < j by REAL_1:84;
j1 in Seg len D1 by A20,FINSEQ_1:def 3;
then j1 in Seg len LVg(D1) by INTEGRA1:def 8;
then PLg(D1,j1)=Sum(LVg(D1)|j1) by INTEGRA1:def 22;
then PLg(D1,j1)+Sum mid(LVg(D1),j,j)
=Sum((LVg(D1)|j1)^mid(LVg(D1),j,j)) by RVSUM_1:105
.=Sum(mid(LVg(D1),1,j1)^mid(LVg(D1),j1+1,j)) by A20,A139,JORDAN3:25
.=Sum(mid(LVg(D1),1,j)) by A20,A137,A140,INTEGRA2:4
.=Sum(LVg(D1)|j) by A137,JORDAN3:25;
hence thesis by A138,INTEGRA1:def 22;
end;
then A141:PLg(D2,indx(D2,D1,j))-PLg(D1,j)
=(PLg(D2,indx(D2,D1,j1))-PLg(D1,j1))
+(Sum mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,len D1))
-Sum mid(lower_volume(g,D1),j,j)) by A131,Lm5
.=0+(Sum mid(lower_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,len D1))
-Sum mid(lower_volume(g,D1),j,j)) by A68,XCMPLX_1:14;
A142:PLg(D2,indx(D2,D1,j))=Sum(lower_volume(g,D2)|indx(D2,D1,j))
by A15,INTEGRA1:def 22
.=Sum lower_volume(g,D2) by A11,TOPREAL1:2;
PLg(D1,j)=Sum(lower_volume(g,D1)|j) by A16,INTEGRA1:def 22
.=Sum lower_volume(g,D1) by A16,TOPREAL1:2;
hence thesis by A70,A141,A142;
end;
theorem Th10:
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)
proof
let A be closed-interval Subset of REAL;
let g be Function of A,REAL;
let D1,D2 be Element of divs A;
assume A1:x in divset(D1,len D1) & len D1 >= 2;
assume A2:D1<=D2 & rng D2 = rng D1 \/ {x};
assume A3:g is_bounded_on A;
deffunc PUg(Element of divs A,Nat) = (PartSums(upper_volume(g,$1))).$2;
deffunc UVg(Element of divs A) = upper_volume(g,$1);
set j = len D1;
len D1 <> 0 & len D2 <> 0 by FINSEQ_1:25;
then A4:len D1 in Seg len D1 & len D2 in Seg len D2 by FINSEQ_1:5;
then A5:len D1 in dom D1 & len D2 in dom D2 by FINSEQ_1:def 3;
A6:len D1 <> 1 by A1;
A7:sup rng g >= inf rng g by A3,Lm6;
A8:indx(D2,D1,j) in dom D2 & D2.indx(D2,D1,j)=D1.(len D1)
by A2,A5,INTEGRA1:def 21;
then A9:indx(D2,D1,j) in Seg len D2 by FINSEQ_1:def 3;
A10: indx(D2,D1,j) >= len upper_volume(g,D2)
proof
assume indx(D2,D1,j) < len upper_volume(g,D2);
then indx(D2,D1,j) < len D2 by INTEGRA1:def 7;
then A11:D1.(len D1) < D2.(len D2) by A5,A8,GOBOARD1:def 1;
A12:not(D2.(len D2) in rng D1)
proof
assume A13:D2.(len D2) in rng D1;
rng D1 c= A by INTEGRA1:def 2;
then inf A <= D2.(len D2) & D2.(len D2) <= sup A by A13,INTEGRA2:1;
hence contradiction by A11,INTEGRA1:def 2;
end;
D2.(len D2) in rng D2 by A5,FUNCT_1:def 5;
then D2.(len D2) in rng D1 or D2.(len D2) in {x} by A2,XBOOLE_0:def 2;
then D2.(len D2) = x by A12,TARSKI:def 1;
then D2.(len D2) <= sup divset(D1,len D1) by A1,INTEGRA2:1;
hence contradiction by A5,A6,A11,INTEGRA1:def 5;
end;
then A14:indx(D2,D1,j) in Seg len upper_volume(g,D2)
& indx(D2,D1,j) >= len upper_volume(g,D2) by A9,INTEGRA1:def 7;
A15:j in Seg len upper_volume(g,D1)
& j >= len upper_volume(g,D1) by A4,INTEGRA1:def 7;
A16:len D1-1 in NAT & len D1-1 in dom D1 by A5,A6,INTEGRA1:9;
reconsider j1=len D1-1 as Element of NAT by A5,A6,INTEGRA1:9;
A17:indx(D2,D1,j1) in dom D2 & 1 <= indx(D2,D1,j1) & indx(D2,D1,j1) <= len D2
proof
thus indx(D2,D1,j1) in dom D2 by A2,A16,INTEGRA1:def 21;
hence thesis by FINSEQ_3:27;
end;
then mid(D2,1,indx(D2,D1,j1)) is increasing by INTEGRA1:37;
then A18:D2|indx(D2,D1,j1) is increasing by A17,JORDAN3:25;
A19:j1 in dom D1 & 1 <= j1 & j1 <= len D1 by A16,FINSEQ_3:27;
then mid(D1,1,j1) is increasing by INTEGRA1:37;
then A20: D1|j1 is increasing by A19,JORDAN3:25;
A21: rng (D2|indx(D2,D1,j1)) = rng (D1|j1) by A1,A2,Lm9;
then A22:D2|indx(D2,D1,j1)=D1|j1 by A18,A20,Th5;
A23:for k st 1 <= k & k <= j1 holds k=indx(D2,D1,k)
proof
let k; assume A24:1 <= k & k <= j1;
assume A25:k<>indx(D2,D1,k);
now per cases by A25,AXIOMS:21;
suppose A26:k > indx(D2,D1,k);
1 <= k & k <= len D1 by A19,A24,AXIOMS:22;
then A27: k in dom D1 by FINSEQ_3:27;
then A28: indx(D2,D1,k) in dom D2 & D1.k=D2.indx(D2,D1,k)
by A2,INTEGRA1:def 21;
then indx(D2,D1,k) in Seg len D2 by FINSEQ_1:def 3;
then A29: 1<=indx(D2,D1,k)&indx(D2,D1,k)<=indx(D2,D1,j1)
by A2,A16,A24,A27,Th6,FINSEQ_1:3;
then indx(D2,D1,k) in Seg indx(D2,D1,j1) by FINSEQ_1:3;
then A30: (D2|indx(D2,D1,j1)).indx(D2,D1,k)=D2.indx(D2,D1,k) by A17,RFINSEQ:
19;
A31: indx(D2,D1,k) < j1 by A24,A26,AXIOMS:22;
then indx(D2,D1,k) <= len D1 by A19,AXIOMS:22;
then indx(D2,D1,k) in Seg len D1 by A29,FINSEQ_1:3;
then indx(D2,D1,k) in dom D1 by FINSEQ_1:def 3;
then A32: D1.k > D1.indx(D2,D1,k) by A26,A27,GOBOARD1:def 1;
indx(D2,D1,k) in Seg j1 by A29,A31,FINSEQ_1:3;
hence contradiction by A16,A22,A28,A30,A32,RFINSEQ:19;
suppose A33:k < indx(D2,D1,k);
k in Seg j1 by A24,FINSEQ_1:3;
then A34: D1.k = (D1|j1).k by A16,RFINSEQ:19;
1 <= k & k <= len D1 by A19,A24,AXIOMS:22;
then A35: k in dom D1 by FINSEQ_3:27;
then A36: indx(D2,D1,k) in dom D2 & D1.k=D2.indx(D2,D1,k)
by A2,INTEGRA1:def 21;
indx(D2,D1,k) <= indx(D2,D1,j1) & indx(D2,D1,k) in dom D2 &
indx(D2,D1,j1) in dom D2 by A2,A16,A24,A35,Th6;
then A37: k <= indx(D2,D1,j1) by A33,AXIOMS:22;
then k <= len D2 by A17,AXIOMS:22;
then k in dom D2 by A24,FINSEQ_3:27;
then A38: D2.k < D2.indx(D2,D1,k) by A33,A36,GOBOARD1:def 1;
k in Seg indx(D2,D1,j1) by A24,A37,FINSEQ_1:3;
hence contradiction by A17,A22,A34,A36,A38,RFINSEQ:19;
end;
hence contradiction;
end;
A39: len (D2|indx(D2,D1,j1))=len (D1|j1) by A18,A20,A21,Th5;
len (D2|indx(D2,D1,j1))=indx(D2,D1,j1) by A17,TOPREAL1:3;
then A40: indx(D2,D1,j1) =j1 by A19,A39,TOPREAL1:3;
j1 in Seg len D1 by A16,FINSEQ_1:def 3;
then j1 <= len D1 by FINSEQ_1:3;
then j1 <= len upper_volume(g,D1) by INTEGRA1:def 7;
then A41:len(upper_volume(g,D1)|j1)=indx(D2,D1,j1) by A40,TOPREAL1:3;
indx(D2,D1,j1) in dom D2 by A2,A16,INTEGRA1:def 21;
then indx(D2,D1,j1) <= len D2 by FINSEQ_3:27;
then indx(D2,D1,j1) <= len upper_volume(g,D2) by INTEGRA1:def 7;
then A42:len(upper_volume(g,D1)|j1)=len(upper_volume(g,D2)|indx(D2,D1,j1))
by A41,TOPREAL1:3;
for k st 1 <= k & k <= len(upper_volume(g,D1)|j1) holds
(upper_volume(g,D1)|j1).k = (upper_volume(g,D2)|indx(D2,D1,j1)).k
proof
let k; assume A43:1 <= k & k <= len(upper_volume(g,D1)|j1);
A44: len(upper_volume(g,D1)) = len D1 by INTEGRA1:def 7;
then A45:1 <= k & k <= j1 by A19,A43,TOPREAL1:3;
then A46: k in Seg j1 by FINSEQ_1:3;
1 <= k & k <= len D1 by A19,A45,AXIOMS:22;
then A47:k in Seg len D1 by FINSEQ_1:3;
A48:divset(D1,k)=divset(D2,indx(D2,D1,k))
proof
A49: divset(D1,k)=[. inf divset(D1,k), sup divset(D1,k) .] by INTEGRA1:5;
A50: k in dom D1 by A47,FINSEQ_1:def 3;
then A51: indx(D2,D1,k) in dom D2 & D1.k=D2.indx(D2,D1,k) by A2,INTEGRA1:def
21;
inf divset(D1,k)=inf divset(D2,indx(D2,D1,k)) &
sup divset(D1,k)=sup divset(D2,indx(D2,D1,k))
proof
per cases;
suppose A52:k=1;
then A53: inf divset(D1,k)=inf A&sup divset(D1,k)=D1.k by A50,INTEGRA1:def 5;
indx(D2,D1,k)=1 by A19,A23,A52;
hence thesis by A51,A53,INTEGRA1:def 5;
suppose A54:k<>1;
then A55: inf divset(D1,k)=D1.(k-1) & sup divset(D1,k)=D1.k
by A50,INTEGRA1:def 5;
A56: k-1 in dom D1 & D1.(k-1) in A & k-1 in NAT by A50,A54,INTEGRA1:9;
reconsider k1=k-1 as Nat by A50,A54,INTEGRA1:9;
k <= k+1 by NAT_1:29;
then k1 <= k by REAL_1:86;
then A57: k1 <= j1 by A45,AXIOMS:22;
1 <= k1 by A56,FINSEQ_3:27;
then A58: k1=indx(D2,D1,k1) by A23,A57;
indx(D2,D1,k)<>1 by A23,A45,A54;
then A59: inf divset(D2,indx(D2,D1,k))=D2.(indx(D2,D1,k)-1) &
sup divset(D2,indx(D2,D1,k))=D2.indx(D2,D1,k) by A51,INTEGRA1:def 5;
D2.(indx(D2,D1,k)-1)= D2.indx(D2,D1,k1) by A23,A45,A58;
hence thesis by A2,A50,A55,A56,A59,INTEGRA1:def 21;
end;
hence thesis by A49,INTEGRA1:5;
end;
j1 in Seg len(upper_volume(g,D1))
by A16,A44,FINSEQ_1:def 3;
then j1 in dom(upper_volume(g,D1)) by FINSEQ_1:def 3;
then A60: (upper_volume(g,D1)|j1).k = upper_volume(g,D1).k by A46,RFINSEQ:19
.=(sup(rng(g|divset(D2,indx(D2,D1,k)))))*vol(divset(D2,indx(D2,D1,k)))
by A47,A48,INTEGRA1:def 7;
indx(D2,D1,k) in Seg j1 by A23,A45,A46;
then A61:indx(D2,D1,k) in Seg indx(D2,D1,j1) by A19,A23;
then 1<=indx(D2,D1,k) & indx(D2,D1,k)<=indx(D2,D1,j1) by FINSEQ_1:3;
then 1<=indx(D2,D1,k) & indx(D2,D1,k)<=len D2 by A17,AXIOMS:22;
then A62:indx(D2,D1,k) in Seg len D2 by FINSEQ_1:3;
indx(D2,D1,j1) in Seg len D2 by A17,FINSEQ_1:def 3;
then indx(D2,D1,j1) in Seg len upper_volume(g,D2) by INTEGRA1:def 7;
then A63:indx(D2,D1,j1) in dom upper_volume(g,D2) by FINSEQ_1:def 3;
(upper_volume(g,D2)|indx(D2,D1,j1)).k
=(upper_volume(g,D2)|indx(D2,D1,j1)).indx(D2,D1,k) by A23,A45
.=upper_volume(g,D2).indx(D2,D1,k) by A61,A63,RFINSEQ:19
.=(sup(rng(g|divset(D2,indx(D2,D1,k)))))*vol(divset(D2,indx(D2,D1,k)))
by A62,INTEGRA1:def 7;
hence thesis by A60;
end;
then A64:upper_volume(g,D2)|indx(D2,D1,j1)=upper_volume(g,D1)|j1
by A42,FINSEQ_1:18;
indx(D2,D1,j1) in Seg len D2 by A17,FINSEQ_1:def 3;
then A65:indx(D2,D1,j1) in Seg len upper_volume(g,D2) by INTEGRA1:def 7;
j1 in Seg len D1 by A16,FINSEQ_1:def 3;
then A66:j1 in Seg len upper_volume(g,D1) by INTEGRA1:def 7;
A67:PUg(D2,indx(D2,D1,j1))=Sum(upper_volume(g,D2)|indx(D2,D1,j1))
by A65,INTEGRA1:def 22
.=PUg(D1,j1) by A64,A66,INTEGRA1:def 22;
A68:indx(D2,D1,j1)+1 <= indx(D2,D1,len D1)
proof
len D1 < len D1+1 by NAT_1:38;
then j1 < len D1 by REAL_1:84;
then indx(D2,D1,j1) < indx(D2,D1,len D1) by A2,A5,A16,Th7;
hence thesis by NAT_1:38;
end;
A69:Sum mid(upper_volume(g,D1),len D1,len D1)
-Sum mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,len D1))
<= (sup rng g-inf rng g)*delta(D1)
proof
A70: 1 <= indx(D2,D1,j) & indx(D2,D1,j) <= len upper_volume(g,D2)
proof
indx(D2,D1,j) in dom D2 by A2,A5,INTEGRA1:def 21;
then indx(D2,D1,j) in Seg len D2 by FINSEQ_1:def 3;
then indx(D2,D1,j) in Seg len upper_volume(g,D2) by INTEGRA1:def 7;
hence thesis by FINSEQ_1:3;
end;
then A71: 1 <= indx(D2,D1,j1)+1 & indx(D2,D1,j1)+1 <= len upper_volume(g,D2)
by A17,A68,AXIOMS:22,NAT_1:38;
A72:indx(D2,D1,j)-indx(D2,D1,j1) <= 2
proof
assume A73:indx(D2,D1,j)-indx(D2,D1,j1) > 2;
reconsider ID1=indx(D2,D1,j1)+1 as Nat;
reconsider ID2=ID1+1 as Nat;
A74:indx(D2,D1,j1) < ID1 & ID1 < ID2 & ID2 < indx(D2,D1,j)
proof
thus indx(D2,D1,j1) < ID1 by NAT_1:38;
thus ID1 < ID2 by NAT_1:38;
indx(D2,D1,j1)+(1+1)<indx(D2,D1,j) by A73,REAL_1:86;
hence thesis by XCMPLX_1:1;
end;
A75:indx(D2,D1,j) in dom D2 by A2,A5,INTEGRA1:def 21;
then A76:indx(D2,D1,j) <= len D2 by FINSEQ_3:27;
A77:ID1 in dom D2
proof
A78: 1 <= ID1 & ID1 <= indx(D2,D1,j) by A17,A74,AXIOMS:22;
then ID1 <= len D2 by A76,AXIOMS:22;
hence thesis by A78,FINSEQ_3:27;
end;
A79:ID2 in dom D2
proof
A80: indx(D2,D1,j1) <= ID2 & ID2 <= len D2 by A74,A76,AXIOMS:22;
then 1 <= ID2 by A17,AXIOMS:22;
hence thesis by A80,FINSEQ_3:27;
end;
then A81:D2.indx(D2,D1,j1)<D2.ID1 & D2.ID1<D2.ID2 & D2.ID2<D2.indx(D2,D1,j)
by A17,A74,A75,A77,GOBOARD1:def 1;
A82:D2.ID1 in {x} & D2.ID2 in {x}
proof
A83: D2.ID1 in rng D2 & D2.ID2 in rng D2 by A77,A79,FUNCT_1:def 5;
A84: D1.j1 = D2.indx(D2,D1,j1) & D1.j = D2.indx(D2,D1,j)
by A2,A5,A16,INTEGRA1:def 21;
not(D2.ID1 in rng D1) & not(D2.ID2 in rng D1)
proof
assume A85:D2.ID1 in rng D1 or D2.ID2 in rng D1;
now per cases by A85;
suppose D2.ID1 in rng D1;
then consider n such that
A86: n in dom D1 & D1.n=D2.ID1 by PARTFUN1:26;
D2.indx(D2,D1,j1)<D2.ID1 & D2.ID1<D2.indx(D2,D1,j)
by A81,AXIOMS:22;
then j1<n & n<j by A5,A16,A84,A86,GOBOARD2:18;
then j<n+1 & n<j by REAL_1:84;
hence contradiction by NAT_1:38;
suppose D2.ID2 in rng D1;
then consider n such that
A87: n in dom D1 & D1.n=D2.ID2 by PARTFUN1:26;
D2.indx(D2,D1,j1)<D2.ID2 & D2.ID2<D2.indx(D2,D1,j)
by A81,AXIOMS:22;
then j1<n & n<j by A5,A16,A84,A87,GOBOARD2:18;
then j<n+1 & n<j by REAL_1:84;
hence contradiction by NAT_1:38;
end;
hence thesis;
end;
hence thesis by A2,A83,XBOOLE_0:def 2;
end;
then D2.ID1 = x by TARSKI:def 1;
then D2.ID1=D2.ID2 by A82,TARSKI:def 1;
hence contradiction by A74,A77,A79,GOBOARD2:19;
end;
1 <= indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 &
indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 <= 2
proof
A88: indx(D2,D1,j)-'(indx(D2,D1,j1)+1)
=indx(D2,D1,j)-(indx(D2,D1,j1)+1) by A68,SCMFSA_7:3;
then indx(D2,D1,j)-'(indx(D2,D1,j1)+1) >= 0 by A68,SQUARE_1:12;
then indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 >= 0+1 by AXIOMS:24;
hence indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 >= 1;
indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1
=indx(D2,D1,j)-indx(D2,D1,j1)-1+1 by A88,XCMPLX_1:36
.=indx(D2,D1,j)-indx(D2,D1,j1)+1-1 by XCMPLX_1:29
.=indx(D2,D1,j)-indx(D2,D1,j1) by XCMPLX_1:26;
hence thesis by A72;
end;
then A89: 1 <= len mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)) &
len mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))<=2
by A68,A70,A71,JORDAN3:27;
A90: 1 <= j & j <= len upper_volume(g,D1) by A4,FINSEQ_1:3,INTEGRA1:def 7;
j-'j+1 = 1 by Lm3;
then A91: len mid(upper_volume(g,D1),j,j)=1 by A90,JORDAN3:27;
mid(upper_volume(g,D1),j,j).1 = upper_volume(g,D1).j by A90,JORDAN3:27;
then mid(upper_volume(g,D1),j,j)=<*upper_volume(g,D1).j*> by A91,FINSEQ_1:
57;
then A92:Sum mid(upper_volume(g,D1),j,j)=upper_volume(g,D1).j by RVSUM_1:103;
A93:indx(D2,D1,j1)+1 in Seg len D2
proof
indx(D2,D1,j1)+1 in Seg len upper_volume(g,D2) by A71,FINSEQ_1:3;
hence thesis by INTEGRA1:def 7;
end;
now per cases by A89,Lm4;
suppose
A94: len mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))=1;
A95: indx(D2,D1,j1)+1=indx(D2,D1,j)
proof
len mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
= indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1 by A68,A70,A71,JORDAN3:27;
then indx(D2,D1,j)-'(indx(D2,D1,j1)+1)=1-1 by A94,XCMPLX_1:26;
then indx(D2,D1,j)-(indx(D2,D1,j1)+1)=0 by A68,SCMFSA_7:3;
then indx(D2,D1,j)=0+(indx(D2,D1,j1)+1) by XCMPLX_1:27;
hence thesis;
end;
A96: divset(D2,indx(D2,D1,j))=divset(D1,j)
proof
inf divset(D1,j)=D1.j1 & sup divset(D1,j)=D1.j
by A5,A6,INTEGRA1:def 5;
then inf divset(D1,j)=D2.indx(D2,D1,j1)
& sup divset(D1,j)=D2.indx(D2,D1,j)
by A2,A5,A16,INTEGRA1:def 21;
then A97: divset(D1,j)=[. D2.indx(D2,D1,j1),D2.indx(D2,D1,j).] by INTEGRA1:5;
A98: indx(D2,D1,j)-1=indx(D2,D1,j1) by A95,XCMPLX_1:26;
A99: indx(D2,D1,j) in dom D2 by A2,A5,INTEGRA1:def 21;
indx(D2,D1,j)<>1 by A17,A95,NAT_1:38;
then inf divset(D2,indx(D2,D1,j))=D2.(indx(D2,D1,j)-1)
& sup divset(D2,indx(D2,D1,j))=D2.indx(D2,D1,j)
by A99,INTEGRA1:def 5;
hence thesis by A97,A98,INTEGRA1:5;
end;
mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)).1
=upper_volume(g,D2).(indx(D2,D1,j1)+1) by A70,A71,JORDAN3:27;
then mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=<*upper_volume(g,D2).(indx(D2,D1,j1)+1)*> by A94,FINSEQ_1:57;
then A100: Sum mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=upper_volume(g,D2).(indx(D2,D1,j1)+1) by RVSUM_1:103
.=(sup(rng(g|divset(D2,(indx(D2,D1,j1)+1)))))
*vol(divset(D2,(indx(D2,D1,j1)+1))) by A93,INTEGRA1:def 7
.=Sum
mid(upper_volume(g,D1),j,j) by A4,A92,A95,A96,INTEGRA1:def 7;
A101: delta(D1) >= 0 by Th8;
sup rng g - inf rng g >= 0 by A7,SQUARE_1:12;
then (sup rng g - inf rng g)*delta(D1) >= 0*delta(D1) by A101,AXIOMS:25;
hence Sum mid(upper_volume(g,D1),j,j)-
Sum mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
<= (sup rng g-inf rng g)*delta(D1) by A100,XCMPLX_1:14;
suppose
A102: len mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))=2;
A103: mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)).1
=upper_volume(g,D2).(indx(D2,D1,j1)+1) by A70,A71,JORDAN3:27;
mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)).2
=upper_volume(g,D2).(indx(D2,D1,j1)+2)
proof
A104: 2+(indx(D2,D1,j1)+1)>=0+1 by A71,REAL_1:55;
mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j)).2
=UVg(D2).(2+(indx(D2,D1,j1)+1)-'1) by A68,A70,A71,A102,JORDAN3:27
.=UVg(D2).(2+(indx(D2,D1,j1)+1)-1) by A104,SCMFSA_7:3
.=UVg(D2).((indx(D2,D1,j1)+1)+(2-1)) by XCMPLX_1:29
.=UVg(D2).(indx(D2,D1,j1)+(1+1)) by XCMPLX_1:1;
hence thesis;
end;
then mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=<*upper_volume(g,D2).(indx(D2,D1,j1)+1),
upper_volume(g,D2).(indx(D2,D1,j1)+2)*> by A102,A103,FINSEQ_1:61;
then A105: Sum mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=upper_volume(g,D2).(indx(D2,D1,j1)+1)
+upper_volume(g,D2).(indx(D2,D1,j1)+2) by RVSUM_1:107;
A106: vol(divset(D1,j))
=vol(divset(D2,indx(D2,D1,j1)+1))+vol(divset(D2,indx(D2,D1,j1)+2))
proof
A107: inf divset(D1,j)=D2.indx(D2,D1,j1)&sup divset(D1,j)=D2.indx(D2,D1,j)
proof
inf divset(D1,j)=D1.j1 & sup divset(D1,j)=D1.j by A5,A6,INTEGRA1:def 5
;
hence thesis by A2,A5,A16,INTEGRA1:def 21;
end;
A108: indx(D2,D1,j)=indx(D2,D1,j1)+2
proof
indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1=2 by A68,A70,A71,A102,JORDAN3:27;
then indx(D2,D1,j)-(indx(D2,D1,j1)+1)+1=2 by A68,SCMFSA_7:3;
then indx(D2,D1,j)-indx(D2,D1,j1)-1+1=2 by XCMPLX_1:36;
then indx(D2,D1,j)-indx(D2,D1,j1)-(1-1)=2 by XCMPLX_1:37;
hence thesis by XCMPLX_1:27;
end;
A109: inf divset(D2,(indx(D2,D1,j1)+2))=D2.(indx(D2,D1,j1)+1)
& sup divset(D2,(indx(D2,D1,j1)+2))=D2.(indx(D2,D1,j1)+2)
& inf divset(D2,(indx(D2,D1,j1)+1))=D2.indx(D2,D1,j1)
& sup divset(D2,(indx(D2,D1,j1)+1))=D2.(indx(D2,D1,j1)+1)
proof
A110: indx(D2,D1,j1)+2 in dom D2 by A2,A5,A108,INTEGRA1:def 21;
indx(D2,D1,j1)+1 in Seg len upper_volume(g,D2) by A71,FINSEQ_1:3;
then indx(D2,D1,j1)+1 in Seg len D2 by INTEGRA1:def 7;
then A111: indx(D2,D1,j1)+1 in dom D2 by FINSEQ_1:def 3;
A112: indx(D2,D1,j1)+1 <> 1 by A17,NAT_1:38;
indx(D2,D1,j1)+1+1 > 1 by A71,NAT_1:38;
then A113: indx(D2,D1,j1)+(1+1) > 1 by XCMPLX_1:1;
A114: indx(D2,D1,j1)+2-1=indx(D2,D1,j1)+1 by Lm2,XCMPLX_1:29;
A115: indx(D2,D1,j1)+1-1=indx(D2,D1,j1)+(1-1) by XCMPLX_1:29
.=indx(D2,D1,j1)+0;
thus inf divset(D2,(indx(D2,D1,j1)+2))=D2.(indx(D2,D1,j1)+1)
& sup divset(D2,(indx(D2,D1,j1)+2))=D2.(indx(D2,D1,j1)+2)
by A110,A113,A114,INTEGRA1:def 5;
thus thesis by A111,A112,A115,INTEGRA1:def 5;
end;
vol(divset(D1,j))
=sup divset(D1,j)-inf divset(D1,j) by INTEGRA1:def 6
.=D2.indx(D2,D1,j)-(D2.(indx(D2,D1,j1)+1)
-D2.(indx(D2,D1,j1)+1))-D2.indx(D2,D1,j1) by A107,XCMPLX_1:17
.=D2.(indx(D2,D1,j1)+2)-D2.(indx(D2,D1,j1)+1)
+D2.(indx(D2,D1,j1)+1)-D2.indx(D2,D1,j1) by A108,XCMPLX_1:37;
then vol(divset(D1,j))
=vol(divset(D2,indx(D2,D1,j1)+2))
+D2.(indx(D2,D1,j1)+1)-D2.indx(D2,D1,j1) by A109,INTEGRA1:def 6
.=vol(divset(D2,indx(D2,D1,j1)+2))
+(sup divset(D2,indx(D2,D1,j1)+1)-inf divset(D2,indx(D2,D1,j1)+1))
by A109,XCMPLX_1:29;
hence thesis by INTEGRA1:def 6;
end;
then A116: upper_volume(g,D1).j=(sup(rng(g|divset(D1,j))))*
(vol(divset(D2,indx(D2,D1,j1)+1))+vol(divset(D2,indx(D2,D1,j1)+2)))
by A4,INTEGRA1:def 7;
A117: vol(divset(D2,indx(D2,D1,j1)+1))>=0 by INTEGRA1:11;
A118: vol(divset(D2,indx(D2,D1,j1)+2))>=0 by INTEGRA1:11;
A119: Sum mid(UVg(D1),j,j)-Sum mid(UVg(D2),indx(D2,D1,j1)+1,indx(D2,D1,j))
<=(sup rng g - inf rng g)*(vol(divset(D2,indx(D2,D1,j1)+2))
+vol(divset(D2,indx(D2,D1,j1)+1)))
proof
A120: indx(D2,D1,j) in dom D2 by A2,A5,INTEGRA1:def 21;
then A121: indx(D2,D1,j) in Seg len D2 by FINSEQ_1:def 3;
A122: indx(D2,D1,j)=indx(D2,D1,j1)+2
proof
indx(D2,D1,j)-'(indx(D2,D1,j1)+1)+1=2 by A68,A70,A71,A102,JORDAN3:27;
then indx(D2,D1,j)-(indx(D2,D1,j1)+1)+1=2 by A68,SCMFSA_7:3;
then indx(D2,D1,j)-indx(D2,D1,j1)-1+1=2 by XCMPLX_1:36;
then indx(D2,D1,j)-indx(D2,D1,j1)-(1-1)=2 by XCMPLX_1:37;
hence thesis by XCMPLX_1:27;
end;
set ID1=indx(D2,D1,j1)+1, ID2=indx(D2,D1,j1)+2;
A123: Sum mid(UVg(D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=(sup rng(g|divset(D2,indx(D2,D1,j1)+2)))
*vol(divset(D2,indx(D2,D1,j1)+2))
+UVg(D2).(indx(D2,D1,j1)+1) by A105,A121,A122,INTEGRA1:def 7
.=(sup rng(g|divset(D2,indx(D2,D1,j1)+2)))
*vol(divset(D2,indx(D2,D1,j1)+2))
+(sup rng(g|divset(D2,indx(D2,D1,j1)+1)))
*vol(divset(D2,indx(D2,D1,j1)+1)) by A93,INTEGRA1:def 7;
divset(D2,ID2)c=A by A120,A122,INTEGRA1:10;
then sup rng(g|divset(D2,ID2)) >= inf rng g by A3,Lm7;
then A124: (sup rng(g|divset(D2,ID2)))*vol(divset(D2,ID2))
>=(inf rng g)*vol(divset(D2,ID2)) by A118,AXIOMS:25;
ID1 in dom D2 by A93,FINSEQ_1:def 3;
then divset(D2,ID1)c=A by INTEGRA1:10;
then sup rng(g|divset(D2,ID1)) >= inf rng g by A3,Lm7;
then A125: (sup rng(g|divset(D2,ID1)))*vol(divset(D2,ID1))
>=(inf rng g)*vol(divset(D2,ID1)) by A117,AXIOMS:25;
divset(D1,j)c=A by A5,INTEGRA1:10;
then sup rng(g|divset(D1,j)) <= sup rng g by A3,Lm7;
then A126: (sup rng(g|divset(D1,j)))*vol(divset(D2,ID2))
<=(sup rng g)*vol(divset(D2,ID2))
& (sup rng(g|divset(D1,j)))*vol(divset(D2,ID1))
<=(sup rng g)*vol(divset(D2,ID1)) by A117,A118,AXIOMS:25;
Sum mid(UVg(D2),ID1,indx(D2,D1,j))
-(sup rng(g|divset(D2,ID1)))*vol(divset(D2,ID1))
>=(inf rng g)*vol(divset(D2,ID2)) by A123,A124,XCMPLX_1:26;
then Sum mid(UVg(D2),ID1,indx(D2,D1,j))
>=(inf rng g)*vol(divset(D2,ID2))
+(sup rng(g|divset(D2,ID1)))*vol(divset(D2,ID1)) by REAL_1:84;
then Sum mid(UVg(D2),ID1,indx(D2,D1,j))-(inf rng g)*vol(divset(D2,ID2))
>=(sup rng(g|divset(D2,ID1)))*vol(divset(D2,ID1)) by REAL_1:84;
then Sum mid(UVg(D2),ID1,indx(D2,D1,j))-(inf rng g)*vol(divset(D2,ID2))
>=(inf rng g)*vol(divset(D2,ID1)) by A125,AXIOMS:22;
then A127: Sum mid(UVg(D2),ID1,indx(D2,D1,j))>=(inf rng g)*vol(divset(D2,ID2))
+
(inf rng g)*vol(divset(D2,ID1)) by REAL_1:84;
Sum mid(UVg(D1),j,j)
=(sup rng(g|divset(D1,j)))*vol(divset(D2,indx(D2,D1,j1)+2))
+(sup rng(g|divset(D1,j)))*vol(divset(D2,indx(D2,D1,j1)+1))
by A92,A116,XCMPLX_1:8;
then Sum mid(UVg(D1),j,j)-(sup rng(g|divset(D1,j)))*vol(divset(D2,ID1))
=(sup rng(g|divset(D1,j)))*vol(divset(D2,ID2)) by XCMPLX_1:26;
then Sum mid(UVg(D1),j,j)<=(sup rng(g|divset(D1,j)))*vol(divset(D2,ID1))
+(sup rng g)*vol(divset(D2,ID2)) by A126,REAL_1:86;
then Sum mid(UVg(D1),j,j)-(sup rng g)*vol(divset(D2,ID2))
<=(sup rng(g|divset(D1,j)))*vol(divset(D2,ID1)) by REAL_1:86;
then Sum mid(UVg(D1),j,j)-(sup rng g)*vol(divset(D2,ID2))
<=(sup rng g)*vol(divset(D2,ID1)) by A126,AXIOMS:22;
then Sum mid(UVg(D1),j,j)
<=(sup rng g)*vol(divset(D2,ID2))+(sup rng g)*vol(divset(D2,ID1))
by REAL_1:86;
then Sum mid(UVg(D1),j,j)-Sum mid(UVg(D2),ID1,indx(D2,D1,j))
<=(sup rng g)*vol(divset(D2,ID2))+(sup rng g)*vol(divset(D2,ID1))
-((inf rng g)*vol(divset(D2,ID2))+(inf rng g)*vol(divset(D2,ID1)))
by A127,REAL_1:92;
then Sum mid(UVg(D1),j,j)-Sum mid(UVg(D2),ID1,indx(D2,D1,j))
<=((sup rng g)*vol(divset(D2,ID2))-(inf rng g)*vol(divset(D2,ID2)))
+((sup rng g)*vol(divset(D2,ID1))-(inf rng g)*vol(divset(D2,ID1)))
by Lm5;
then Sum mid(UVg(D1),j,j)-Sum mid(UVg(D2),ID1,indx(D2,D1,j))
<=(sup rng g - inf rng g)*vol(divset(D2,ID2))
+((sup rng g)*vol(divset(D2,ID1))-(inf rng g)*vol(divset(D2,ID1)))
by XCMPLX_1:40;
then Sum mid(UVg(D1),j,j)-Sum mid(UVg(D2),ID1,indx(D2,D1,j))
<=(sup rng g - inf rng g)*vol(divset(D2,ID2))
+(sup rng g - inf rng g)*vol(divset(D2,ID1)) by XCMPLX_1:40;
hence thesis by XCMPLX_1:8;
end;
A128: vol(divset(D1,j)) <= delta(D1) by A5,Lm8;
sup rng g - inf rng g >= 0 by A7,SQUARE_1:12;
then (sup rng g - inf rng g)*(vol(divset(D1,j)))
<=(sup rng g - inf rng g)*delta(D1) by A128,AXIOMS:25;
hence thesis by A106,A119,AXIOMS:22;
end;
hence thesis;
end;
A129:PUg(D2,indx(D2,D1,j1))
+Sum mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=PUg(D2,indx(D2,D1,j))
proof
indx(D2,D1,j) in dom D2 by A2,A5,INTEGRA1:def 21;
then A130: indx(D2,D1,j) in Seg len D2 by FINSEQ_1:def 3;
then A131: 1 <= indx(D2,D1,j) & indx(D2,D1,j) <= len D2 by FINSEQ_1:3;
then A132: 1 <= indx(D2,D1,j) & indx(D2,D1,j) <= len UVg(D2) by INTEGRA1:def 7;
A133: indx(D2,D1,j) in Seg len UVg(D2) by A130,INTEGRA1:def 7;
A134: indx(D2,D1,j1) < indx(D2,D1,j) by A68,NAT_1:38;
indx(D2,D1,j1) in Seg len D2 by A17,FINSEQ_1:def 3;
then indx(D2,D1,j1) in Seg len UVg(D2) by INTEGRA1:def 7;
then PUg(D2,indx(D2,D1,j1))
=Sum(UVg(D2)|indx(D2,D1,j1)) by INTEGRA1:def 22;
then PUg(D2,indx(D2,D1,j1))
+Sum mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))
=Sum(UVg(D2)|indx(D2,D1,j1)
^mid(UVg(D2),(indx(D2,D1,j1)+1),indx(D2,D1,j))) by RVSUM_1:105
.=Sum(mid(UVg(D2),1,indx(D2,D1,j1))
^mid(UVg(D2),indx(D2,D1,j1)+1,indx(D2,D1,j))) by A17,JORDAN3:25
.=Sum(mid(UVg(D2),1,indx(D2,D1,j))) by A17,A132,A134,INTEGRA2:4
.=Sum(UVg(D2)|indx(D2,D1,j)) by A131,JORDAN3:25;
hence thesis by A133,INTEGRA1:def 22;
end;
PUg(D1,j1)+Sum mid(upper_volume(g,D1),j,j)=PUg(D1,j)
proof
A135: 1 <= j & j <= len UVg(D1) by A4,FINSEQ_1:3,INTEGRA1:def 7;
A136: j in Seg len UVg(D1) by A4,INTEGRA1:def 7;
A137: j1+1=j by XCMPLX_1:27;
j < j+1 by NAT_1:38;
then A138: j1 < j by REAL_1:84;
j1 in Seg len D1 by A16,FINSEQ_1:def 3;
then j1 in Seg len UVg(D1) by INTEGRA1:def 7;
then PUg(D1,j1)=Sum(UVg(D1)|j1) by INTEGRA1:def 22;
then PUg(D1,j1)+Sum mid(UVg(D1),j,j)
=Sum((UVg(D1)|j1)^mid(UVg(D1),j,j)) by RVSUM_1:105
.=Sum(mid(UVg(D1),1,j1)^mid(UVg(D1),j1+1,j)) by A19,A137,JORDAN3:25
.=Sum(mid(UVg(D1),1,j)) by A19,A135,A138,INTEGRA2:4
.=Sum(UVg(D1)|j) by A135,JORDAN3:25;
hence thesis by A136,INTEGRA1:def 22;
end;
then A139:PUg(D1,j)-PUg(D2,indx(D2,D1,j))
=(PUg(D1,j1)-PUg(D2,indx(D2,D1,j1)))
+(Sum mid(upper_volume(g,D1),j,j)
-Sum mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,len D1)))
by A129,Lm5
.=0+(Sum mid(upper_volume(g,D1),j,j)-
Sum mid(upper_volume(g,D2),(indx(D2,D1,j1)+1),indx(D2,D1,len D1)))
by A67,XCMPLX_1:14;
A140:PUg(D2,indx(D2,D1,j))=Sum(upper_volume(g,D2)|indx(D2,D1,j))
by A14,INTEGRA1:def 22
.=Sum upper_volume(g,D2) by A10,TOPREAL1:2;
PUg(D1,j)=Sum(upper_volume(g,D1)|j) by A15,INTEGRA1:def 22
.=Sum upper_volume(g,D1) by A15,TOPREAL1:2;
hence thesis by A69,A139,A140;
end;
Lm10:
for A be closed-interval Subset of REAL, f be PartFunc of A,REAL
st vol(A)<>0 & y in rng lower_sum_set(f) holds ex D being Element of divs A st
D in dom lower_sum_set(f) & y=(lower_sum_set(f)).D & D.1 > inf A
proof
let A be closed-interval Subset of REAL;
let f be PartFunc of A,REAL;
assume A1:vol(A)<>0;
assume y in rng lower_sum_set(f);
then consider D3 being Element of divs A such that
A2:D3 in dom lower_sum_set(f) & y=(lower_sum_set(f)).D3 by PARTFUN1:26;
len D3 <> 0 by FINSEQ_1:25;
then A3:len D3 in Seg len D3 by FINSEQ_1:5;
then 1 <= len D3 by FINSEQ_1:3;
then A4:1 in Seg len D3 by FINSEQ_1:3;
rng D3 <> {};
then A5:1 in dom D3 by FINSEQ_3:34;
now per cases;
suppose A6:D3.1 <> inf A;
D3.1 in A by A5,INTEGRA1:8;
then inf A <= D3.1 by INTEGRA2:1;
then D3.1 > inf A by A6,REAL_1:def 5;
hence ex D being Element of divs A st D in dom lower_sum_set(f) &
y=(lower_sum_set(f)).D & D.1 > inf A by A2;
suppose A7:D3.1 = inf A;
ex D being Element of divs A st D in dom lower_sum_set(f) &
y=(lower_sum_set(f)).D & D.1 > inf A
proof
A8: D3.(len D3) = sup A by INTEGRA1:def 2;
A9: len D3 in dom D3 by A3,FINSEQ_1:def 3;
vol(A) >= 0 by INTEGRA1:11;
then sup A - inf A > 0 by A1,INTEGRA1:def 6;
then sup A > inf A by REAL_2:106;
then A10: len D3 > 1 by A5,A7,A8,A9,GOBOARD2:18;
then reconsider D=D3/^1 as increasing FinSequence of REAL by INTEGRA1:
36;
A11: len D = len D3 - 1 & for m be Nat st m in dom D holds D.m = D3.(m+1)
by A10,RFINSEQ:def 2;
then len D <> 0 by A10,SQUARE_1:11;
then reconsider D as non empty increasing FinSequence of REAL by
FINSEQ_1:25;
rng D c= rng D3 & rng D3 c= A by FINSEQ_5:36,INTEGRA1:def 2;
then A12: rng D c= A by XBOOLE_1:1;
A13: len D+1=len D3 by A11,XCMPLX_1:27;
len D in dom D by SCMFSA_7:12;
then D.(len D)=sup A by A8,A10,A13,RFINSEQ:def 2;
then D is DivisionPoint of A by A12,INTEGRA1:def 2;
then reconsider D as Element of divs A by INTEGRA1:def 4;
D in divs A;
then A14: D in dom lower_sum_set(f) by INTEGRA1:def 12;
A15: y=(lower_sum_set(f)).D
proof
A16: y=lower_sum(f,D3) by A2,INTEGRA1:def 12
.=Sum(lower_volume(f,D3)) by INTEGRA1:def 10
.=Sum((lower_volume(f,D3)|1)^(lower_volume(f,D3)/^1)) by RFINSEQ:21;
A17: lower_volume(f,D3)|1 = <*lower_volume(f,D3).1*>
proof
A18: 1 <= len lower_volume(f,D3) by A10,INTEGRA1:def 8;
then A19: len (lower_volume(f,D3)|1)=1 by TOPREAL1:3;
A20: 1 in dom lower_volume(f,D3) by A18,FINSEQ_3:27;
1 in Seg 1 by FINSEQ_1:3;
then (lower_volume(f,D3)|1).1 = lower_volume(f,D3).1 by A20,RFINSEQ:
19;
hence thesis by A19,FINSEQ_1:57;
end;
A21: vol(divset(D3,1))=sup divset(D3,1)-inf divset(D3,1) by INTEGRA1:def 6
.=sup divset(D3,1) - inf A by A5,INTEGRA1:def 5
.=D3.1 - inf A by A5,INTEGRA1:def 5
.=0 by A7,XCMPLX_1:14;
A22: lower_volume(f,D3).1=(inf rng(f|divset(D3,1)))*vol(divset(D3,1))
by A4,INTEGRA1:def 8;
lower_volume(f,D3)/^1 = lower_volume(f,D)
proof
A23: 2-'1=2-1 by SCMFSA_7:3 .= 1;
A24: len D3 >= 1+1 by A10,NAT_1:38;
then len lower_volume(f,D3) >= 2 by INTEGRA1:def 8;
then A25: mid(lower_volume(f,D3),2,len lower_volume(f,D3))
=lower_volume(f,D3)/^1 by A23,JORDAN3:26;
A26: 2 <= len lower_volume(f,D3) & 1 <= len lower_volume(f,D3)
by A10,A24,INTEGRA1:def 8;
A27: len(mid(lower_volume(f,D3),2,len lower_volume(f,D3)))
=len lower_volume(f,D)
proof
len(mid(lower_volume(f,D3),2,len lower_volume(f,D3)))
=len lower_volume(f,D3)-'2+1 by A26,JORDAN3:27
.=len D3-'2+1 by INTEGRA1:def 8
.=len D3-2+1 by A24,SCMFSA_7:3
.=len D3-(2-1) by XCMPLX_1:37
.=len D3-1;
hence thesis by A11,INTEGRA1:def 8;
end;
for i st 1<=i&i<=len mid(lower_volume(f,D3),2,len lower_volume(f,D3
)
)
holds mid(lower_volume(f,D3),2,len lower_volume(f,D3)).i
=lower_volume(f,D).i
proof
let i; assume
A28: 1<=i&i<=len mid(lower_volume(f,D3),2,len lower_volume(f,D3));
then A29: 1 <= i & i <= len D by A27,INTEGRA1:def 8;
then 1<=i & i<=len lower_volume(f,D3) - 1 by A11,INTEGRA1:def 8;
then 1 <= i & i <= len lower_volume(f,D3)-2+1 by Lm2,XCMPLX_1:37;
then A30: mid(lower_volume(f,D3),2,len lower_volume(f,D3)).i
=lower_volume(f,D3).(i+2-1) by A26,JORDAN3:31
.=lower_volume(f,D3).(i+(2-1)) by XCMPLX_1:29
.=lower_volume(f,D3).(i+1);
1 <= i+1 & i+1 <= len D3 by A11,A29,NAT_1:37,REAL_1:84;
then A31: i+1 in Seg len D3 by FINSEQ_1:3;
then A32: mid(lower_volume(f,D3),2,len lower_volume(f,D3)).i
=(inf rng(f|divset(D3,i+1)))*vol(divset(D3,i+1))
by A30,INTEGRA1:def 8;
A33: divset(D3,i+1)=divset(D,i)
proof
A34: 1<>i+1 by A28,NAT_1:38;
i+1 in dom D3 by A31,FINSEQ_1:def 3;
then A35: sup divset(D3,i+1)=D3.(i+1) & inf divset(D3,i+1)=D3.(i+1-
1)
by A34,INTEGRA1:def 5;
then A36: sup divset(D3,i+1)=D3.(i+1) & inf divset(D3,i+1)=D3.i by
XCMPLX_1:26;
A37: i in dom D by A29,FINSEQ_3:27;
then A38: D.i=D3.(i+1) by A10,RFINSEQ:def 2;
per cases;
suppose A39:i=1;
then A40: inf divset(D,i)=inf A & sup divset(D,i)=D.i
by A37,INTEGRA1:def 5;
divset(D3,i+1)=[.inf A, D.i.] by A7,A35,A38,A39,INTEGRA1:5;
hence thesis by A40,INTEGRA1:5;
suppose A41:i<>1;
then A42: inf divset(D,i)=D.(i-1) & sup divset(D,i)=D.i
by A37,INTEGRA1:def 5;
i-1 in dom D & i-1 in NAT by A37,A41,INTEGRA1:9;
then D.(i-1)=D3.(i-1+1) by A10,RFINSEQ:def 2
.= D3.(i-(1-1)) by XCMPLX_1:37
.=D3.i;
then divset(D3,i+1)=[.inf divset(D,i),sup divset(D,i).]
by A36,A38,A42,INTEGRA1:5;
hence thesis by INTEGRA1:5;
end;
i in Seg len D by A29,FINSEQ_1:3;
hence thesis by A32,A33,INTEGRA1:def 8;
end;
hence thesis by A25,A27,FINSEQ_1:18;
end;
then y=0+Sum(lower_volume(f,D)) by A16,A17,A21,A22,RVSUM_1:106
.=lower_sum(f,D) by INTEGRA1:def 10;
hence thesis by A14,INTEGRA1:def 12;
end;
rng D <> {};
then 1 in dom D by FINSEQ_3:34;
then A43: D.1=D3.(1+1) by A10,RFINSEQ:def 2 .=D3.2;
1+1 <= len D3 by A10,NAT_1:38;
then 2 in dom D3 by FINSEQ_3:27;
then D3.1 < D3.2 by A5,GOBOARD1:def 1;
hence thesis by A7,A14,A15,A43;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th11:
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
proof
let A be closed-interval Subset of REAL;
let D be Element of divs A;
let r be Real;
let i,j be Nat;
assume A1:i in dom D;
assume A2:j in dom D;
assume A3:i <= j;
assume A4:r < mid(D,i,j).1;
consider C being closed-interval Subset of REAL such that
A5:inf C=mid(D,i,j).1 & sup C=mid(D,i,j).(len mid(D,i,j))
& len mid(D,i,j)=j-i+1 & mid(D,i,j) is DivisionPoint of C
by A1,A2,A3,INTEGRA1:38;
consider a,b such that
A6:a <= b & a = inf C & b = sup C by INTEGRA1:4;
r <= sup C by A4,A5,A6,AXIOMS:22;
then reconsider B=[.r,sup C.] as closed-interval Subset of REAL by INTEGRA1:
def 1;
reconsider MD=mid(D,i,j) as non empty increasing FinSequence of REAL by A5;
B=[.inf B,sup B.] by INTEGRA1:5;
then A7:inf B = r & sup B = sup C by INTEGRA1:6;
A8:rng mid(D,i,j) c= C&mid(D,i,j).(len mid(D,i,j))=sup C by A5,INTEGRA1:def 2;
x in C implies x in B
proof
assume x in C;
then inf C <= x & x <= sup C by INTEGRA2:1;
then r <= x & x <= sup C by A4,A5,AXIOMS:22;
hence thesis by A7,INTEGRA2:1;
end;
then C c= B by SUBSET_1:7;
then rng mid(D,i,j) c= B by A8,XBOOLE_1:1;
then MD is DivisionPoint of B by A5,A7,INTEGRA1:def 2;
hence thesis by A5,A7;
end;
Lm11:for A be closed-interval Subset of REAL,
D1 be Element of divs A st vol(A)<>0 & len D1 = 1 holds
<*inf A*>^D1 is non empty increasing FinSequence of REAL
proof
let A be closed-interval Subset of REAL,
D1 be Element of divs A;
assume A1:vol(A)<>0;
assume len D1 = 1;
then A2: D1.1=sup A by INTEGRA1:def 2;
vol(A) >= 0 by INTEGRA1:11;
then D1.1 - inf A > 0 by A1,A2,INTEGRA1:def 6;
then A3:inf A < D1.1 by REAL_2:106;
set MD1 = <*inf A*>^D1;
A4:len MD1 = len <*inf A*> + len D1 by FINSEQ_1:35;
len <*inf A*> = 1 by FINSEQ_1:56;
then A5: len MD1 <> 0 by A4,NAT_1:21;
n in dom MD1 & m in dom MD1 & n<m implies MD1.n < MD1.m
proof
assume A6:n in dom MD1 & m in dom MD1 & n<m;
A7: not m in dom <*inf A*>
proof
assume m in dom <*inf A*>;
then m in Seg len <*inf A*> by FINSEQ_1:def 3;
then m in {1} by FINSEQ_1:4,56;
then A8: n < 1 by A6,TARSKI:def 1;
n in Seg len MD1 by A6,FINSEQ_1:def 3;
hence contradiction by A8,FINSEQ_1:3;
end;
MD1.m in rng MD1 by A6,FUNCT_1:def 5;
then A9: MD1.m in rng <*inf A*> \/ rng D1 by FINSEQ_1:44;
not(MD1.m in rng <*inf A*>)
proof
assume MD1.m in rng <*inf A*>;
then MD1.m in {inf A} by FINSEQ_1:55;
then A10: MD1.m = inf A by TARSKI:def 1;
consider n such that
A11: n in dom D1 & m=len <*inf A*>+n by A6,A7,FINSEQ_1:38;
n in Seg len D1 by A11,FINSEQ_1:def 3;
then A12: 1 <= n & n <= len D1 by FINSEQ_1:3;
rng D1 <> {};
then A13: 1 in dom D1 by FINSEQ_3:34;
D1.n=MD1.m by A11,FINSEQ_1:def 7;
hence contradiction by A3,A10,A11,A12,A13,GOBOARD2:18;
end;
then A14: MD1.m in rng D1 by A9,XBOOLE_0:def 2;
now per cases by A6,FINSEQ_1:38;
suppose A15:n in dom <*inf A*>;
then n in Seg len <*inf A*> by FINSEQ_1:def 3;
then n in {1} by FINSEQ_1:4,56;
then A16: n = 1 by TARSKI:def 1;
consider k such that
A17: k in dom D1 & MD1.m = D1.k by A14,PARTFUN1:26;
A18: 1 <= k & k <= len D1 by A17,FINSEQ_3:27;
rng D1 <> {};
then 1 in dom D1 by FINSEQ_3:34;
then A19: D1.1 <= MD1.m by A17,A18,GOBOARD2:18;
MD1.n = <*inf A*>.n by A15,FINSEQ_1:def 7 .= inf A by A16,FINSEQ_1:def
8
;
hence MD1.n < MD1.m by A3,A19,AXIOMS:22;
suppose ex i st i in dom D1 & n = len <*inf A*> + i;
then consider i such that
A20: i in dom D1 & n=len <*inf A*> + i;
consider j such that
A21: j in dom D1 & m=len <*inf A*> + j by A6,A7,FINSEQ_1:38;
A22: i < j by A6,A20,A21,AXIOMS:24;
A23: D1.i=MD1.n by A20,FINSEQ_1:def 7;
D1.j=MD1.m by A21,FINSEQ_1:def 7;
hence thesis by A20,A21,A22,A23,GOBOARD1:def 1;
end;
hence thesis;
end;
hence thesis by A5,FINSEQ_1:25,GOBOARD1:def 1;
end;
Lm12:for A be closed-interval Subset of REAL,
D2 be Element of divs A st inf A < D2.1 holds
<*inf A*>^D2 is non empty increasing FinSequence of REAL
proof
let A be closed-interval Subset of REAL,
D2 be Element of divs A;
assume A1: inf A < D2.1;
set MD2=<*inf A*>^D2;
A2: len MD2 = 1+len D2 by FINSEQ_5:8;
n in dom MD2 & m in dom MD2 & n<m implies MD2.n < MD2.m
proof
assume A3:n in dom MD2 & m in dom MD2 & n<m;
A4: not m in dom <*inf A*>
proof
assume m in dom <*inf A*>;
then m in Seg len <*inf A*> by FINSEQ_1:def 3;
then m in {1} by FINSEQ_1:4,56;
then A5: n < 1 by A3,TARSKI:def 1;
n in Seg len MD2 by A3,FINSEQ_1:def 3;
hence contradiction by A5,FINSEQ_1:3;
end;
MD2.m in rng MD2 by A3,FUNCT_1:def 5;
then MD2.m in rng <*inf A*> \/ rng D2 by FINSEQ_1:44;
then A6: MD2.m in rng <*inf A*> or MD2.m in rng D2 by XBOOLE_0:def 2;
A7: not MD2.m in rng <*inf A*>
proof
assume MD2.m in rng <*inf A*>;
then MD2.m in {inf A} by FINSEQ_1:55;
then A8: MD2.m = inf A by TARSKI:def 1;
consider n such that
A9: n in dom D2 & m=len <*inf A*>+n by A3,A4,FINSEQ_1:38;
n in Seg len D2 by A9,FINSEQ_1:def 3;
then A10: 1 <= n & n <= len D2 by FINSEQ_1:3;
rng D2 <> {};
then A11: 1 in dom D2 by FINSEQ_3:34;
D2.n=MD2.m by A9,FINSEQ_1:def 7;
hence contradiction by A1,A8,A9,A10,A11,GOBOARD2:18;
end;
now per cases by A3,FINSEQ_1:38;
suppose A12:n in dom <*inf A*>;
then n in Seg len <*inf A*> by FINSEQ_1:def 3;
then n in {1} by FINSEQ_1:4,56;
then A13: n = 1 by TARSKI:def 1;
consider k such that
A14: k in dom D2 & MD2.m = D2.k by A6,A7,PARTFUN1:26;
k in Seg len D2 by A14,FINSEQ_1:def 3;
then A15: 1 <= k & k <= len D2 by FINSEQ_1:3;
rng D2 <> {};
then 1 in dom D2 by FINSEQ_3:34;
then A16: D2.1 <= MD2.m by A14,A15,GOBOARD2:18;
MD2.n = <*inf A*>.n by A12,FINSEQ_1:def 7 .= inf A by A13,FINSEQ_1:def
8
;
hence MD2.n < MD2.m by A1,A16,AXIOMS:22;
suppose ex i st i in dom D2 & n = len <*inf A*> + i;
then consider i such that
A17: i in dom D2 & n=len <*inf A*> + i;
consider j such that
A18: j in dom D2 & m=len <*inf A*> + j by A3,A4,FINSEQ_1:38;
A19: i < j by A3,A17,A18,AXIOMS:24;
A20: D2.i=MD2.n by A17,FINSEQ_1:def 7;
D2.j=MD2.m by A18,FINSEQ_1:def 7;
hence thesis by A17,A18,A19,A20,GOBOARD1:def 1;
end;
hence thesis;
end;
hence thesis by A2,FINSEQ_1:25,GOBOARD1:def 1;
end;
Lm13:for A be closed-interval Subset of REAL,
f being PartFunc of A,REAL,
D1, MD1 being Element of divs A
st MD1 = <*inf A*>^D1 holds
(for i st i in Seg len D1 holds divset(MD1,i+1)=divset(D1,i)) &
upper_volume(f,D1)=upper_volume(f,MD1)/^1 &
lower_volume(f,D1)=lower_volume(f,MD1)/^1
proof
let A be closed-interval Subset of REAL,
f being PartFunc of A,REAL,
D1, MD1 being Element of divs A;
assume A1:MD1 = <*inf A*>^D1;
then A2: len MD1=len <*inf A*> + len D1 by FINSEQ_1:35
.= 1+len D1 by FINSEQ_1:56;
thus A3:for i st i in Seg len D1 holds divset(MD1,i+1)=divset(D1,i)
proof
let i;
assume A4:i in Seg len D1;
then A5: 1 <= i & i <= len D1 by FINSEQ_1:3;
A6: i in dom D1 by A4,FINSEQ_1:def 3;
A7: 1 <= i+1 by NAT_1:29;
i+1 <= len D1+1 by A5,AXIOMS:24;
then i+1 <= len D1 + len<*inf A*> by FINSEQ_1:56;
then i+1 <= len MD1 by A1,FINSEQ_1:35;
then A8: i+1 in dom MD1 by A7,FINSEQ_3:27;
A9: divset(D1,i)=[.inf divset(D1,i), sup divset(D1,i).] by INTEGRA1:5;
inf divset(D1,i)=inf divset(MD1,i+1)
& sup divset(D1,i)=sup divset(MD1,i+1)
proof
per cases;
suppose A10:i=1;
i+1 > 1 by A5,NAT_1:38;
then A11: inf divset(MD1,i+1)=MD1.(i+1-1) & sup divset(MD1,i+1)=MD1.(i+1)
by A8,INTEGRA1:def 5;
then A12: inf divset(MD1,i+1) = inf A by A1,A10,FINSEQ_1:58;
MD1.(i+1) = MD1.(i+len <*inf A*>) by FINSEQ_1:57
.= D1.i by A1,A6,FINSEQ_1:def 7;
hence thesis by A6,A10,A11,A12,INTEGRA1:def 5;
suppose A13:i<>1;
A14: i+1 > 1 by A5,NAT_1:38;
i-1 in dom D1 & i-1 in NAT by A6,A13,INTEGRA1:9;
then D1.(i-1) = MD1.(i-1+len <*inf A*>) by A1,FINSEQ_1:def 7
.=MD1.(i-1+1) by FINSEQ_1:56 .=MD1.(i-(1-1)) by XCMPLX_1:37
.=MD1.(i+1-1) by XCMPLX_1:26;
then A15: inf divset(D1,i)=MD1.(i+1-1) by A6,A13,INTEGRA1:def 5
.=inf divset(MD1,i+1) by A8,A14,INTEGRA1:def 5;
MD1.(i+1) = MD1.(i+len <*inf A*>) by FINSEQ_1:57
.= D1.i by A1,A6,FINSEQ_1:def 7;
then sup divset(MD1,i+1)=D1.i by A8,A14,INTEGRA1:def 5
.= sup divset(D1,i) by A6,A13,INTEGRA1:def 5;
hence thesis by A15;
end;
hence thesis by A9,INTEGRA1:5;
end;
thus upper_volume(f,D1)=upper_volume(f,MD1)/^1
proof
set D2 = D1, MD2 = MD1;
A16: len upper_volume(f,D2)=len (upper_volume(f,MD2)/^1)
proof
rng upper_volume(f,MD2) <> {};
then 1 in dom upper_volume(f,MD2) by FINSEQ_3:34;
then 1 <= len upper_volume(f,MD2) by FINSEQ_3:27;
then len (upper_volume(f,MD2)/^1)=len upper_volume(f,MD2)-1 by RFINSEQ:
def 2
.=len MD2 -1 by INTEGRA1:def 7
.=len D2 by A2,XCMPLX_1:26;
hence thesis by INTEGRA1:def 7;
end;
1 <= k & k <= len upper_volume(f,D2) implies
upper_volume(f,D2).k = (upper_volume(f,MD2)/^1).k
proof
assume A17:1 <= k & k <= len upper_volume(f,D2);
then k in Seg len upper_volume(f,D2) by FINSEQ_1:3;
then A18: k in Seg len D2 by INTEGRA1:def 7;
then A19: upper_volume(f,D2).k=(sup rng(f|divset(D2,k)))*vol(divset(D2,k))
by INTEGRA1:def 7 .=(sup rng(f|divset(MD2,k+1)))*vol(divset(D2,k))
by A3,A18 .=(sup rng(f|divset(MD2,k+1)))*vol(divset(MD2,k+1)) by A3,A18;
A20: 1 <= k+1 by NAT_1:29;
k+1 <= len upper_volume(f,D2)+1 by A17,AXIOMS:24;
then k+1 <= len D2+1 by INTEGRA1:def 7;
then A21: k+1 in Seg len MD2 by A2,A20,FINSEQ_1:3;
A22: k in dom (upper_volume(f,MD2)/^1) by A16,A17,FINSEQ_3:27;
A23: len (upper_volume(f,MD2)/^1) <= len upper_volume(f,MD2) by FINSEQ_5:28;
1 <= len upper_volume(f,D2) by A17,AXIOMS:22;
then 1 <= len upper_volume(f,MD2) by A16,A23,AXIOMS:22;
then (upper_volume(f,MD2)/^1).k=upper_volume(f,MD2).(k+1) by A22,RFINSEQ:
def 2
.=(sup rng(f|divset(MD2,k+1)))*vol(divset(MD2,k+1))
by A21,INTEGRA1:def 7;
hence thesis by A19;
end;
hence thesis by A16,FINSEQ_1:18;
end;
A24: len lower_volume(f,D1)=len (lower_volume(f,MD1)/^1)
proof
rng lower_volume(f,MD1) <> {};
then 1 in dom lower_volume(f,MD1) by FINSEQ_3:34;
then 1 <= len lower_volume(f,MD1) by FINSEQ_3:27;
then len (lower_volume(f,MD1)/^1)=len lower_volume(f,MD1)-1 by RFINSEQ:
def 2
.=len MD1 -1 by INTEGRA1:def 8
.=len D1 by A2,XCMPLX_1:26;
hence thesis by INTEGRA1:def 8;
end;
1 <= k & k <= len lower_volume(f,D1) implies
lower_volume(f,D1).k = (lower_volume(f,MD1)/^1).k
proof
assume A25:1 <= k & k <= len lower_volume(f,D1);
then k in Seg len lower_volume(f,D1) by FINSEQ_1:3;
then A26: k in Seg len D1 by INTEGRA1:def 8;
then A27: lower_volume(f,D1).k=(inf rng(f|divset(D1,k)))*vol(divset(D1,k))
by INTEGRA1:def 8 .=(inf rng(f|divset(MD1,k+1)))*vol(divset(D1,k))
by A3,A26
.=(inf rng(f|divset(MD1,k+1)))*vol(divset(MD1,k+1)) by A3,A26;
A28: 1 <= k+1 by NAT_1:29;
A29: len MD1=len <*inf A*>+len D1 by A1,FINSEQ_1:35
.=len D1 + 1 by FINSEQ_1:56;
k+1 <= len lower_volume(f,D1)+1 by A25,AXIOMS:24;
then k+1 <= len D1+1 by INTEGRA1:def 8;
then A30: k+1 in Seg len MD1 by A28,A29,FINSEQ_1:3;
A31: k in dom (lower_volume(f,MD1)/^1) by A24,A25,FINSEQ_3:27;
A32: len (lower_volume(f,MD1)/^1) <= len lower_volume(f,MD1) by FINSEQ_5:28;
1 <= len (lower_volume(f,MD1)/^1) by A24,A25,AXIOMS:22;
then 1 <= len lower_volume(f,MD1) by A32,AXIOMS:22;
then (lower_volume(f,MD1)/^1).k=lower_volume(f,MD1).(k+1) by A31,RFINSEQ:
def 2
.=(inf rng(f|divset(MD1,k+1)))*vol(divset(MD1,k+1))
by A30,INTEGRA1:def 8;
hence thesis by A27;
end;
hence thesis by A24,FINSEQ_1:18;
end;
Lm14:for A be closed-interval Subset of REAL, D2, MD2 being Element of divs A
st MD2 = <*inf A*>^D2 holds vol(divset(MD2,1))=0
proof
let A be closed-interval Subset of REAL, D2,MD2 be Element of divs A;
assume A1:MD2 = <*inf A*>^D2;
rng MD2 <> {};
then 1 in dom MD2 by FINSEQ_3:34;
then inf divset(MD2,1) = inf A & sup divset(MD2,1) = MD2.1 by INTEGRA1:def
5;
then vol(divset(MD2,1)) = MD2.1 - inf A by INTEGRA1:def 6.=inf A-inf A
by A1,FINSEQ_1:58;
hence thesis by XCMPLX_1:14;
end;
Lm15:
for A be closed-interval Subset of REAL, f be Function of A,REAL,
D1,MD1 be Element of divs A st MD1 = <*inf A*>^D1 holds
delta(MD1)=delta(D1)
proof
let A be closed-interval Subset of REAL, f be Function of A,REAL,
D1,MD1 be Element of divs A;
assume A1:MD1 = <*inf A*>^D1;
then A2: vol(divset(MD1,1))=0 by Lm14;
A3: delta(D1)=max rng upper_volume(chi(A,A),D1) by INTEGRA1:def 19;
then delta(D1) in rng upper_volume(chi(A,A),D1)
& for x st x in rng upper_volume(chi(A,A),D1) holds x <= delta(D1)
by PRE_CIRC:def 1;
then consider i such that
A4: i in dom upper_volume(chi(A,A),D1) & upper_volume(chi(A,A),D1).i=delta(D1)
by PARTFUN1:26;
A5: delta(MD1)=max rng upper_volume(chi(A,A),MD1) by INTEGRA1:def 19;
then delta(MD1) in rng upper_volume(chi(A,A),MD1)
&for x st x in rng upper_volume(chi(A,A),MD1) holds x <= delta(MD1)
by PRE_CIRC:def 1;
then consider j such that
A6: j in dom upper_volume(chi(A,A),MD1)&upper_volume(chi(A,A),MD1).j=delta(MD1
)
by PARTFUN1:26;
i in Seg len upper_volume(chi(A,A),D1) by A4,FINSEQ_1:def 3;
then A7: i in Seg len D1 by INTEGRA1:def 7;
then A8: delta(D1)=(sup rng (chi(A,A)|divset(D1,i)))*vol(divset(D1,i))
by A4,INTEGRA1:def 7
.=(sup rng(chi(A,A)|divset(MD1,i+1)))*vol(divset(D1,i)) by A1,A7,Lm13
.=(sup rng (chi(A,A)|divset(MD1,i+1)))*vol(divset(MD1,i+1)) by A1,A7,Lm13;
i in dom D1 by A7,FINSEQ_1:def 3;
then len <*inf A*>+i in dom MD1 by A1,FINSEQ_1:41;
then i+1 in dom MD1 by FINSEQ_1:56;
then A9: i+1 in Seg len MD1 by FINSEQ_1:def 3;
then A10: delta(D1)=upper_volume(chi(A,A),MD1).(i+1) by A8,INTEGRA1:def 7;
i+1 in Seg len upper_volume(chi(A,A),MD1) by A9,INTEGRA1:def 7;
then i+1 in dom upper_volume(chi(A,A),MD1) by FINSEQ_1:def 3;
then delta(D1) in rng upper_volume(chi(A,A),MD1) by A10,FUNCT_1:def 5;
then A11: delta(D1) <= delta(MD1) by A5,PRE_CIRC:def 1;
j in Seg len upper_volume(chi(A,A),MD1) by A6,FINSEQ_1:def 3;
then A12: j in Seg len MD1 by INTEGRA1:def 7;
then A13: delta(MD1)=(sup rng(chi(A,A)|divset(MD1,j)))*vol(divset(MD1,j))
by A6,INTEGRA1:def 7;
delta(MD1) <= delta(D1)
proof
per cases;
suppose j=1;
hence thesis by A2,A13,Th8;
suppose j<>1;
then not(j in Seg 1) by FINSEQ_1:4,TARSKI:def 1;
then not(j in Seg len <*inf A*>) by FINSEQ_1:56;
then A14: not(j in dom <*inf A*>) by FINSEQ_1:def 3;
j in dom MD1 by A12,FINSEQ_1:def 3;
then consider k such that
A15: k in dom D1 & j=len <*inf A*>+k by A1,A14,FINSEQ_1:38;
A16: k in Seg len D1 by A15,FINSEQ_1:def 3;
then divset(D1,k)=divset(MD1,k+1) by A1,Lm13
.=divset(MD1,j) by A15,FINSEQ_1:56;
then delta(MD1) = (sup rng(chi(A,A)|divset(D1,k)))*vol(divset(D1,k))
by A6,A12,INTEGRA1:def 7;
then A17: delta(MD1)=upper_volume(chi(A,A),D1).k by A16,INTEGRA1:def 7;
k in Seg len upper_volume(chi(A,A),D1) by A16,INTEGRA1:def 7;
then k in dom upper_volume(chi(A,A),D1) by FINSEQ_1:def 3;
then delta(MD1) in rng upper_volume(chi(A,A),D1) by A17,FUNCT_1:def 5;
hence thesis by A3,PRE_CIRC:def 1;
end;
hence thesis by A11,AXIOMS:21;
end;
theorem Th12:
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)
proof
let A be closed-interval Subset of REAL;
let f be Function of A,REAL;
let D1,D2 be Element of divs A;
assume that A1:x in divset(D1,len D1) and A2:vol(A)<>0 and A3:D1 <= D2
and A4:rng D2 = rng D1 \/ {x} and A5:f is_bounded_on A
and A6:x > inf A;
len D1 <> 0 by FINSEQ_1:25;
then len D1 in Seg len D1 by FINSEQ_1:5;
then A7:1 <= len D1 by FINSEQ_1:3;
then len D1 = 1 or len D1 > 1 by REAL_1:def 5;
then A8:len D1 = 1 or len D1 >= 1+1 by NAT_1:38;
now per cases by A8;
suppose A9:len D1 = 1;
then A10: D1.1=sup A by INTEGRA1:def 2;
vol(A) >= 0 by INTEGRA1:11;
then D1.1 - inf A > 0 by A2,A10,INTEGRA1:def 6;
then A11:inf A < D1.1 by REAL_2:106;
reconsider MD1 = <*inf A*>^D1
as non empty increasing FinSequence of REAL by A2,A9,Lm11;
MD1 is DivisionPoint of A
proof
y in rng MD1 implies y in A
proof
assume y in rng MD1;
then A12: y in rng <*inf A*> \/ rng D1 by FINSEQ_1:44;
per cases by A12,XBOOLE_0:def 2;
suppose y in rng <*inf A*>;
then y in {inf A} by FINSEQ_1:55;
then A13: y = inf A by TARSKI:def 1;
consider a,b such that
A14: a <= b & a = inf A & b = sup A by INTEGRA1:4;
thus thesis by A13,A14,INTEGRA2:1;
suppose A15:y in rng D1;
rng D1 c= A by INTEGRA1:def 2;
hence thesis by A15;
end;
then A16: rng MD1 c= A by SUBSET_1:7;
MD1.(len MD1) = sup A
proof
A17: len MD1 = len <*inf A*> + len D1 by FINSEQ_1:35;
len <*inf A*> + 1 <= len <*inf A*> + len D1 by A7,AXIOMS:24;
then MD1.(len MD1)=D1.(len <*inf A*>+len D1-len <*inf A*>) by A17,
FINSEQ_1:36
.=D1.(len D1) by XCMPLX_1:26;
hence thesis by INTEGRA1:def 2;
end;
hence thesis by A16,INTEGRA1:def 2;
end;
then reconsider MD1 as Element of divs A by INTEGRA1:def 4;
rng D2 <> {};
then A18: 1 in dom D2 by FINSEQ_3:34;
then A19: 1 <= len D2 by FINSEQ_3:27;
A20: D2.1 in rng D2 by A18,FUNCT_1:def 5;
A21:inf A < D2.1
proof
per cases by A4,A20,XBOOLE_0:def 2;
suppose D2.1 in rng D1;
then consider k such that
A22: k in dom D1 & D1.k = D2.1 by PARTFUN1:26;
A23: 1 <= k & k <= len D1 by A22,FINSEQ_3:27;
rng D1 <> {};
then 1 in dom D1 by FINSEQ_3:34;
then D1.1 <= D2.1 by A22,A23,GOBOARD2:18;
hence thesis by A11,AXIOMS:22;
suppose D2.1 in {x};
hence thesis by A6,TARSKI:def 1;
end;
set MD2=<*inf A*>^D2;
reconsider MD2 as non empty increasing FinSequence of REAL by A21,Lm12;
MD2 is DivisionPoint of A
proof
y in rng MD2 implies y in A
proof
assume y in rng MD2;
then A24: y in rng <*inf A*> \/ rng D2 by FINSEQ_1:44;
per cases by A24,XBOOLE_0:def 2;
suppose y in rng <*inf A*>;
then y in {inf A} by FINSEQ_1:55;
then A25: y = inf A by TARSKI:def 1;
consider a,b such that
A26: a <= b & a = inf A & b = sup A by INTEGRA1:4;
thus thesis by A25,A26,INTEGRA2:1;
suppose A27:y in rng D2;
rng D2 c= A by INTEGRA1:def 2;
hence thesis by A27;
end;
then A28: rng MD2 c= A by SUBSET_1:7;
MD2.(len MD2) = sup A
proof
A29: len MD2 = len <*inf A*> + len D2 by FINSEQ_1:35;
len <*inf A*> + 1 <= len <*inf A*> + len D2 by A19,AXIOMS:24;
then MD2.(len MD2)=D2.(len <*inf A*>+len D2-len <*inf A*>) by A29,
FINSEQ_1:36
.=D2.(len D2) by XCMPLX_1:26;
hence thesis by INTEGRA1:def 2;
end;
hence thesis by A28,INTEGRA1:def 2;
end;
then reconsider MD2 as Element of divs A by INTEGRA1:def 4;
A30: len MD1=len <*inf A*> + len D1 by FINSEQ_1:35 .= 1+len D1 by FINSEQ_1:56;
A31: 1+len D1 >= 1+1 by A7,AXIOMS:24;
A32: x in divset(MD1,len MD1)
proof
A33: inf divset(D1,len D1) <= x & x <= sup divset(D1,len D1) by A1,INTEGRA2:1;
A34: len D1 in dom D1 by SCMFSA_7:12;
A35: len MD1 in dom MD1 by SCMFSA_7:12;
A36: len MD1 <> 1 by A30,A31;
len MD1 - 1 =len D1 by A30,XCMPLX_1:26;
then inf divset(MD1,len MD1) = MD1.(len D1) by A35,A36,INTEGRA1:def 5
.=inf A by A9,FINSEQ_1:58;
then A37: inf divset(D1,len D1) = inf divset(MD1,len MD1) by A9,A34,INTEGRA1:
def 5;
MD1.(len MD1) = MD1.(len <*inf A*> + len D1) by FINSEQ_1:35
.=D1.(len D1) by A34,FINSEQ_1:def 7;
then sup divset(MD1,len MD1)=D1.(len D1) by A35,A36,INTEGRA1:def 5
.= sup divset(D1,len D1)
by A9,A34,INTEGRA1:def 5;
hence thesis by A33,A37,INTEGRA2:1;
end;
A38:MD1<=MD2
proof
A39: len D1 <= len D2 & rng D1 c= rng D2 by A3,INTEGRA1:def 20;
then len D1+len <*inf A*> <= len D2+len <*inf A*> by AXIOMS:24;
then len MD1 <= len D2+len <*inf A*> by FINSEQ_1:35;
then A40: len MD1 <= len MD2 by FINSEQ_1:35;
rng D1 \/ rng<*inf A*> c= rng D2 \/ rng <*inf A*> by A39,XBOOLE_1:9;
then rng MD1 c= rng D2 \/ rng <*inf A*> by FINSEQ_1:44;
then rng MD1 c= rng MD2 by FINSEQ_1:44;
hence thesis by A40,INTEGRA1:def 20;
end;
rng MD2 = rng D2 \/ rng <*inf A*> by FINSEQ_1:44
.=rng D1 \/ rng <*inf A*> \/ {x} by A4,XBOOLE_1:4;
then rng MD2 = rng MD1 \/ {x} by FINSEQ_1:44;
then A41:Sum lower_volume(f,MD2)-Sum
lower_volume(f,MD1)<=(sup rng f-inf rng f)*delta(MD1)
by A5,A30,A31,A32,A38,Th9;
A42:vol(divset(MD1,1))=0 by Lm14;
lower_volume(f,D1)=lower_volume(f,MD1)/^1 by Lm13;
then lower_volume(f,MD1)=<*(lower_volume(f,MD1))/.1*>^lower_volume(f,D1)
by FINSEQ_5:32;
then A43:Sum lower_volume(f,MD1)=((lower_volume(f,MD1))/.1)+Sum lower_volume(f,
D1)
by RVSUM_1:106;
rng MD1 <> {};
then 1 in dom MD1 by FINSEQ_3:34;
then A44:1 in Seg len MD1 by FINSEQ_1:def 3;
then A45:lower_volume(f,MD1).1 = (inf rng(f|divset(MD1,1)))*vol(divset(MD1,1))
by INTEGRA1:def 8;
1 in Seg len lower_volume(f,MD1) by A44,INTEGRA1:def 8;
then 1 in dom lower_volume(f,MD1) by FINSEQ_1:def 3;
then A46: lower_volume(f,MD1)/.1 = 0 by A42,A45,FINSEQ_4:def 4;
A47:vol(divset(MD2,1))=0 by Lm14;
lower_volume(f,D2)=lower_volume(f,MD2)/^1 by Lm13;
then lower_volume(f,MD2)=<*(lower_volume(f,MD2))/.1*>^lower_volume(f,D2)
by FINSEQ_5:32;
then A48:Sum lower_volume(f,MD2)=(lower_volume(f,MD2))/.1+Sum lower_volume(f,D2
)
by RVSUM_1:106;
rng MD2 <> {};
then 1 in dom MD2 by FINSEQ_3:34;
then A49:1 in Seg len MD2 by FINSEQ_1:def 3;
then A50: lower_volume(f,MD2).1 = (inf rng(f|divset(MD2,1)))*vol(divset(MD2
,1))
by INTEGRA1:def 8;
1 in Seg len lower_volume(f,MD2) by A49,INTEGRA1:def 8;
then 1 in dom lower_volume(f,MD2) by FINSEQ_1:def 3;
then lower_volume(f,MD2)/.1 = 0 by A47,A50,FINSEQ_4:def 4;
hence Sum lower_volume(f,D2)-Sum lower_volume(f,D1)<=
(sup rng f-inf rng f)*delta(D1) by A41,A43,A46,A48,Lm15;
suppose len D1 >= 2;
hence thesis by A1,A3,A4,A5,Th9;
end;
hence thesis;
end;
theorem Th13:
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)
proof
let A be closed-interval Subset of REAL;
let f be Function of A,REAL;
let D1,D2 be Element of divs A;
assume that A1:x in divset(D1,len D1) and A2:vol(A)<>0 and A3:D1 <= D2
and A4:rng D2 = rng D1 \/ {x} and A5:f is_bounded_on A
and A6:x > inf A;
len D1 <> 0 by FINSEQ_1:25;
then len D1 in Seg len D1 by FINSEQ_1:5;
then A7:1 <= len D1 by FINSEQ_1:3;
then len D1 = 1 or len D1 > 1 by REAL_1:def 5;
then A8:len D1 = 1 or len D1 >= 1+1 by NAT_1:38;
now per cases by A8;
suppose A9:len D1 = 1;
then A10: D1.1=sup A by INTEGRA1:def 2;
vol(A) >= 0 by INTEGRA1:11;
then D1.1 - inf A > 0 by A2,A10,INTEGRA1:def 6;
then A11:inf A < D1.1 by REAL_2:106;
reconsider MD1 = <*inf A*>^D1 as non empty increasing FinSequence of REAL
by A2,A9,Lm11;
MD1 is DivisionPoint of A
proof
y in rng MD1 implies y in A
proof
assume y in rng MD1;
then A12: y in rng <*inf A*> \/ rng D1 by FINSEQ_1:44;
per cases by A12,XBOOLE_0:def 2;
suppose y in rng <*inf A*>;
then y in {inf A} by FINSEQ_1:55;
then A13: y = inf A by TARSKI:def 1;
consider a,b such that
A14: a <= b & a = inf A & b = sup A by INTEGRA1:4;
thus thesis by A13,A14,INTEGRA2:1;
suppose A15:y in rng D1;
rng D1 c= A by INTEGRA1:def 2;
hence thesis by A15;
end;
then A16: rng MD1 c= A by SUBSET_1:7;
MD1.(len MD1) = sup A
proof
A17: len MD1 = len <*inf A*> + len D1 by FINSEQ_1:35;
len <*inf A*> + 1 <= len <*inf A*> + len D1 by A7,AXIOMS:24;
then MD1.(len MD1)=D1.(len <*inf A*>+len D1-len <*inf A*>) by A17,
FINSEQ_1:36
.=D1.(len D1) by XCMPLX_1:26;
hence thesis by INTEGRA1:def 2;
end;
hence thesis by A16,INTEGRA1:def 2;
end;
then reconsider MD1 as Element of divs A by INTEGRA1:def 4;
rng D2 <> {};
then A18: 1 in dom D2 by FINSEQ_3:34;
then A19: 1 <= len D2 by FINSEQ_3:27;
A20:D2.1 in rng D2 by A18,FUNCT_1:def 5;
A21:inf A < D2.1
proof
per cases by A4,A20,XBOOLE_0:def 2;
suppose D2.1 in rng D1;
then consider k such that
A22: k in dom D1 & D1.k = D2.1 by PARTFUN1:26;
A23: 1 <= k & k <= len D1 by A22,FINSEQ_3:27;
rng D1 <> {};
then 1 in dom D1 by FINSEQ_3:34;
then D1.1 <= D2.1 by A22,A23,GOBOARD2:18;
hence thesis by A11,AXIOMS:22;
suppose D2.1 in {x};
hence thesis by A6,TARSKI:def 1;
end;
set MD2=<*inf A*>^D2;
reconsider MD2 as non empty increasing FinSequence of REAL by A21,Lm12;
MD2 is DivisionPoint of A
proof
y in rng MD2 implies y in A
proof
assume y in rng MD2;
then A24: y in rng <*inf A*> \/ rng D2 by FINSEQ_1:44;
per cases by A24,XBOOLE_0:def 2;
suppose y in rng <*inf A*>;
then y in {inf A} by FINSEQ_1:55;
then A25: y = inf A by TARSKI:def 1;
consider a,b such that
A26: a <= b & a = inf A & b = sup A by INTEGRA1:4;
thus thesis by A25,A26,INTEGRA2:1;
suppose A27:y in rng D2;
rng D2 c= A by INTEGRA1:def 2;
hence thesis by A27;
end;
then A28: rng MD2 c= A by SUBSET_1:7;
MD2.(len MD2) = sup A
proof
A29: len MD2 = len <*inf A*> + len D2 by FINSEQ_1:35;
len <*inf A*> + 1 <= len <*inf A*> + len D2 by A19,AXIOMS:24;
then MD2.(len MD2)=D2.(len <*inf A*>+len D2-len <*inf A*>) by A29,
FINSEQ_1:36
.=D2.(len D2) by XCMPLX_1:26;
hence thesis by INTEGRA1:def 2;
end;
hence thesis by A28,INTEGRA1:def 2;
end;
then reconsider MD2 as Element of divs A by INTEGRA1:def 4;
A30: len MD1=len <*inf A*> + len D1 by FINSEQ_1:35 .= 1+len D1 by FINSEQ_1:56;
A31:1+len D1 >= 1+1 by A7,AXIOMS:24;
A32: x in divset(MD1,len MD1)
proof
A33: inf divset(D1,len D1) <= x & x <= sup divset(D1,len D1) by A1,INTEGRA2:1;
A34: len D1 in dom D1 by SCMFSA_7:12;
A35: len MD1 in dom MD1 by SCMFSA_7:12;
A36: len MD1 <> 1 by A30,A31;
len MD1 - 1 = len D1 by A30,XCMPLX_1:26;
then inf divset(MD1,len MD1) = MD1.(len D1) by A35,A36,INTEGRA1:def 5
.=inf A by A9,FINSEQ_1:58;
then A37: inf divset(D1,len D1) = inf divset(MD1,len MD1) by A9,A34,INTEGRA1:
def 5;
MD1.(len MD1) = MD1.(len <*inf A*> + len D1) by FINSEQ_1:35
.=D1.(len D1) by A34,FINSEQ_1:def 7;
then sup divset(MD1,len MD1)=D1.(len D1) by A35,A36,INTEGRA1:def 5
.= sup divset(D1,len D1) by A9,A34,INTEGRA1:def 5;
hence thesis by A33,A37,INTEGRA2:1;
end;
A38:MD1<=MD2
proof
A39: len D1 <= len D2 & rng D1 c= rng D2 by A3,INTEGRA1:def 20;
then len D1+len <*inf A*> <= len D2+len <*inf A*> by AXIOMS:24;
then len MD1 <= len D2+len <*inf A*> by FINSEQ_1:35;
then A40: len MD1 <= len MD2 by FINSEQ_1:35;
rng D1 \/ rng<*inf A*> c= rng D2 \/ rng <*inf A*> by A39,XBOOLE_1:9;
then rng MD1 c= rng D2 \/ rng <*inf A*> by FINSEQ_1:44;
then rng MD1 c= rng MD2 by FINSEQ_1:44;
hence thesis by A40,INTEGRA1:def 20;
end;
rng MD2 = rng MD1 \/ {x}
proof
rng MD2 = rng D2 \/ rng <*inf A*> by FINSEQ_1:44
.=rng D1 \/ rng <*inf A*> \/ {x} by A4,XBOOLE_1:4;
hence thesis by FINSEQ_1:44;
end;
then A41:Sum upper_volume(f,MD1)-Sum upper_volume(f,MD2)
<=(sup rng f-inf rng f)*delta(MD1) by A5,A30,A31,A32,A38,Th10;
A42:vol(divset(MD1,1))=0 by Lm14;
upper_volume(f,D1)=upper_volume(f,MD1)/^1 by Lm13;
then upper_volume(f,MD1)=<*upper_volume(f,MD1)/.1*>^upper_volume(f,D1)
by FINSEQ_5:32;
then A43:Sum upper_volume(f,MD1)=(upper_volume(f,MD1)/.1)+Sum upper_volume(f,D1
)
by RVSUM_1:106;
rng MD1 <> {};
then 1 in dom MD1 by FINSEQ_3:34;
then A44:1 in Seg len MD1 by FINSEQ_1:def 3;
then A45:upper_volume(f,MD1).1 = (sup rng(f|divset(MD1,1)))*vol(divset(MD1,1))
by INTEGRA1:def 7;
1 in Seg len upper_volume(f,MD1) by A44,INTEGRA1:def 7;
then 1 in dom upper_volume(f,MD1) by FINSEQ_1:def 3;
then A46: upper_volume(f,MD1)/.1 = 0 by A42,A45,FINSEQ_4:def 4;
A47:vol(divset(MD2,1))=0 by Lm14;
upper_volume(f,D2)=upper_volume(f,MD2)/^1 by Lm13;
then upper_volume(f,MD2)=<*upper_volume(f,MD2)/.1*>^upper_volume(f,D2)
by FINSEQ_5:32;
then A48:Sum upper_volume(f,MD2)=(upper_volume(f,MD2)/.1)+Sum upper_volume(f,D2
)
by RVSUM_1:106;
rng MD2 <> {};
then 1 in dom MD2 by FINSEQ_3:34;
then A49:1 in Seg len MD2 by FINSEQ_1:def 3;
then A50:upper_volume(f,MD2).1 = (sup rng(f|divset(MD2,1)))*vol(divset(MD2,1))
by INTEGRA1:def 7;
1 in Seg len upper_volume(f,MD2) by A49,INTEGRA1:def 7;
then 1 in dom upper_volume(f,MD2) by FINSEQ_1:def 3;
then upper_volume(f,MD2)/.1 = 0 by A47,A50,FINSEQ_4:def 4;
hence Sum upper_volume(f,D1)-Sum upper_volume(f,D2)<=
(sup rng f-inf rng f)*delta(D1) by A41,A43,A46,A48,Lm15;
suppose len D1 >= 2;
hence thesis by A1,A3,A4,A5,Th10;
end;
hence thesis;
end;
theorem Th14:
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))
proof
let A be closed-interval Subset of REAL;
let D1,D2 be Element of divs A;
let r be Real;
let i,j;
assume A1:i in dom D1;
assume A2:j in dom D1;
assume A3:i <= j;
assume A4:D1 <= D2;
assume A5:r < mid(D2,indx(D2,D1,i),indx(D2,D1,j)).1;
set MD1=mid(D1,i,j);
set MD2=mid(D2,indx(D2,D1,i),indx(D2,D1,j));
A6: indx(D2,D1,i) in dom D2 & D2.indx(D2,D1,i)=D1.i by A1,A4,INTEGRA1:def 21;
A7: indx(D2,D1,j) in dom D2 & D2.indx(D2,D1,j)=D1.j by A2,A4,INTEGRA1:def 21;
D1.i <= D1.j by A1,A2,A3,GOBOARD2:18;
then A8:indx(D2,D1,i) <= indx(D2,D1,j) by A6,A7,GOBOARD1:def 1;
then consider B being closed-interval Subset of REAL such that
A9: r = inf B & sup B=MD2.(len MD2) & len MD2=indx(D2,D1,j)-indx(D2,D1,i)+1
&MD2 is DivisionPoint of B by A5,A6,A7,Th11;
reconsider MD2 as Element of divs B by A9,INTEGRA1:def 3;
indx(D2,D1,j)-indx(D2,D1,i) >= 0 by A8,SQUARE_1:12;
then A10:indx(D2,D1,j)-indx(D2,D1,i)+1 >= 0+1 by AXIOMS:24;
A11:1 <= indx(D2,D1,i) & indx(D2,D1,j) <= len D2 by A6,A7,FINSEQ_3:27;
then A12:MD2.1=D2.(1+indx(D2,D1,i)-1) by A8,A10,JORDAN3:31
.=D2.indx(D2,D1,i) by XCMPLX_1:26 .=D1.i by A1,A4,INTEGRA1:def 21;
j-i >= 0 by A3,SQUARE_1:12;
then A13:j-i+1 >= 0+1 by AXIOMS:24;
A14:1 <= i & j <= len D1 by A1,A2,FINSEQ_3:27;
then A15:MD1.1 = D1.(1+i-1) by A3,A13,JORDAN3:31 .= D1.i by XCMPLX_1:26;
then consider C being closed-interval Subset of REAL such that
A16:r = inf C & sup C=MD1.(len MD1) & len MD1=j-i+1
&MD1 is DivisionPoint of C by A1,A2,A3,A5,A12,Th11;
A17:MD1.(len MD1)=D1.(j-i+1-1+i) by A3,A13,A14,A16,JORDAN3:31
.=D1.(j-i+i) by XCMPLX_1:26 .=D1.(j-(i-i)) by XCMPLX_1:37
.=D1.j by XCMPLX_1:17;
A18: MD2.(len MD2)=D2.(indx(D2,D1,j)-indx(D2,D1,i)+1-1+indx(D2,D1,i))
by A8,A9,A10,A11,JORDAN3:31
.=D2.(indx(D2,D1,j)-indx(D2,D1,i)+indx(D2,D1,i)) by XCMPLX_1:26
.=D2.(indx(D2,D1,j)-(indx(D2,D1,i)-indx(D2,D1,i))) by XCMPLX_1:37
.=D2.indx(D2,D1,j) by XCMPLX_1:17 .= D1.j by A2,A4,INTEGRA1:def 21;
A19:B=[.inf B,sup B.] by INTEGRA1:5
.=C by A9,A16,A17,A18,INTEGRA1:5;
then reconsider MD1 as Element of divs B by A16,INTEGRA1:def 3;
A20:rng MD1 c= rng MD2
proof
A21: rng MD1 c= rng D1 by JORDAN3:28;
rng D1 c= rng D2 by A4,INTEGRA1:def 20;
then A22: rng MD1 c= rng D2 by A21,XBOOLE_1:1;
let x1;assume A23:x1 in rng MD1;
then consider k2 being Nat such that
A24: k2 in dom D2 & D2.k2=x1 by A22,PARTFUN1:26;
consider k1 being Nat such that
A25: k1 in dom MD1 & MD1.k1=x1 by A23,PARTFUN1:26;
A26: 1 <= k1 & k1 <= len MD1 by A25,FINSEQ_3:27;
then 1 <= len MD1 by AXIOMS:22;
then A27: 1 in dom MD1 by FINSEQ_3:27;
len MD1 in dom MD1 by SCMFSA_7:12;
then MD1.1<=MD1.k1 & MD1.k1<=MD1.(len MD1) by A25,A26,A27,GOBOARD2:18;
then A28: indx(D2,D1,i) <= k2 & k2 <= indx(D2,D1,j)
by A6,A7,A15,A17,A24,A25,GOBOARD1:def 1;
then indx(D2,D1,i)+1<=k2+1 & k2+1<=indx(D2,D1,j)+1 by AXIOMS:24;
then A29: 1<=k2+1-indx(D2,D1,i) & k2+1-indx(D2,D1,i)<=indx(D2,D1,j)+1-indx(D2,
D1,i)
by REAL_1:49,84;
indx(D2,D1,i) <= k2+1 by A28,NAT_1:37;
then consider k3 being Nat such that
A30: k2+1 = indx(D2,D1,i)+k3 by NAT_1:28;
A31: 1 <= k3 & k3 <= indx(D2,D1,j)+1-indx(D2,D1,i) by A29,A30,XCMPLX_1:26;
then MD2.k3 = D2.(k3+indx(D2,D1,i)-1) by A8,A11,JORDAN3:31;
then A32: MD2.k3=D2.k2 by A30,XCMPLX_1:26;
1 <= k3 & k3 <= indx(D2,D1,j)-indx(D2,D1,i)+1 by A31,XCMPLX_1:29;
then k3 in dom MD2 by A9,FINSEQ_3:27;
hence thesis by A24,A32,FUNCT_1:def 5;
end;
len MD1 <= len MD2
proof
MD1 is one-to-one & MD2 is one-to-one by JORDAN7:17;
then card(rng MD1) = len MD1 & card(rng MD2) = len MD2 by FINSEQ_4:77;
hence thesis by A20,CARD_1:80;
end;
then MD1 <= MD2 by A20,INTEGRA1:def 20;
hence thesis by A9,A16,A19;
end;
theorem Th15:
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)
proof
let A be closed-interval Subset of REAL;
let D be Element of divs A;
assume x in rng D;
then consider i such that
A1:i in dom D & x=D.i by PARTFUN1:26;
A2:1 <= i & i <= len D by A1,FINSEQ_3:27;
then 1 <= len D by AXIOMS:22;
then 1 in dom D & len D in dom D by FINSEQ_3:27;
hence thesis by A1,A2,GOBOARD2:18;
end;
theorem Th16:
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)
proof
let p be FinSequence of REAL;
let i,j,k;
assume that A1:p is increasing and A2:i in dom p and A3:j in dom p
and A4:k in dom p and A5:p.i <= p.k and A6:p.k <= p.j;
A7:1 <= i & i <= len p by A2,FINSEQ_3:27;
A8:1 <= j & j <= len p by A3,FINSEQ_3:27;
A9:i <= k by A1,A2,A4,A5,GOBOARD1:def 1;
A10:k <= j by A1,A3,A4,A6,GOBOARD1:def 1;
then A11:i <= j by A9,AXIOMS:22;
then len mid(p,i,j) = j-'i+1 by A7,A8,JORDAN3:27;
then A12:len mid(p,i,j) = j-i+1 by A11,SCMFSA_7:3;
i <= k+1 by A9,NAT_1:37;
then consider n such that
A13:k+1=i+n by NAT_1:28;
A14:n=k+1-i by A13,XCMPLX_1:26 .=k-i+1 by XCMPLX_1:29;
k-i >= 0 by A9,SQUARE_1:12;
then A15:k-i+1 >= 0+1 by AXIOMS:24;
k-i <= j-i by A10,REAL_1:49;
then A16:k-i+1 <= j-i+1 by AXIOMS:24;
then A17:n in dom mid(p,i,j) by A12,A14,A15,FINSEQ_3:27;
mid(p,i,j).n = p.(n+i-1) by A7,A8,A11,A14,A15,A16,JORDAN3:31
.=p.k by A13,XCMPLX_1:26;
hence thesis by A17,FUNCT_1:def 5;
end;
theorem Th17:
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
proof
let A be closed-interval Subset of REAL;
let f be Function of A,REAL;
let D be Element of divs A;
assume A1:f is_bounded_on A;
assume i in dom D;
then divset(D,i) c= A by INTEGRA1:10;
hence thesis by A1,Lm7;
end;
theorem Th18:
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
proof
let A be closed-interval Subset of REAL;
let f be Function of A,REAL;
let D be Element of divs A;
assume A1:f is_bounded_on A;
assume i in dom D;
then divset(D,i) c= A by INTEGRA1:10;
hence thesis by A1,Lm7;
end;
begin :: Darboux's Theorem
theorem
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)
proof
let A be closed-interval Subset of REAL;
let f be Function of A,REAL;
let T be DivSequence of A;
assume A1:f is_bounded_on A;
assume A2:delta(T) is convergent_to_0;
assume A3:vol(A)<>0;
A4:delta(T) is_not_0 & delta(T) is convergent & lim delta(T) = 0
by A2,FDIFF_1:def 1;
A5:for e st e>0 ex n st for m st n<=m holds
0 < (delta(T)).m & (delta(T)).m < e
proof
let e; assume e>0;
then consider n such that
A6: for m st n<=m holds abs((delta(T)).m-0)<e by A4,SEQ_2:def 7;
for m st n<=m holds 0 < (delta(T)).m & (delta(T)).m < e
proof
let m; assume n<=m;
then A7: abs((delta(T)).m-0)<e by A6;
(delta(T)).m-0<=abs((delta(T)).m-0) by ABSVALUE:11;
then A8: (delta(T)).m+abs((delta(T)).m-0)<e+abs((delta(T)).m-0) by A7,REAL_1
:67;
A9: (delta(T)).m<>0 by A4,SEQ_1:7;
A10: (delta(T)).m = delta(T.m) by INTEGRA2:def 3;
delta(T.m) = max rng upper_volume(chi(A,A),T.m) by INTEGRA1:def 19;
then delta(T.m) in rng upper_volume(chi(A,A),T.m) by PRE_CIRC:def 1;
then consider i such that
A11: i in dom upper_volume(chi(A,A),T.m) &
delta(T.m)=upper_volume(chi(A,A),T.m).i by PARTFUN1:26;
A12: i in Seg len upper_volume(chi(A,A),T.m) by A11,FINSEQ_1:def 3;
consider D being Element of divs A such that
A13: D = T.m;
i in Seg len D by A12,A13,INTEGRA1:def 7;
then delta(T.m)=vol(divset(T.m,i)) by A11,A13,INTEGRA1:22;
hence thesis by A8,A9,A10,AXIOMS:24,INTEGRA1:11;
end;
hence thesis;
end;
A14:for D,D1 be Element of divs A holds ex D2 be Element of divs A st
D<=D2 & D1<=D2 & rng D2=rng D1 \/
rng D & 0<=lower_sum(f,D2)-lower_sum(f,D) &
0<=lower_sum(f,D2)-lower_sum(f,D1)
proof
let D,D1 be Element of divs A;
consider D2 be Element of divs A such that
A15: D<=D2 & D1<=D2 & rng D2=rng D1 \/ rng D by Th3;
A16: f is_bounded_below_on A by A1,RFUNCT_1:def 11;
then lower_sum(f,D2)>=lower_sum(f,D) by A15,INTEGRA1:48;
then A17: lower_sum(f,D2)-lower_sum(f,D)>=0 by SQUARE_1:12;
lower_sum(f,D2)>=lower_sum(f,D1) by A15,A16,INTEGRA1:48;
then lower_sum(f,D2)-lower_sum(f,D1)>=0 by SQUARE_1:12;
hence thesis by A15,A17;
end;
A18:sup rng f >= inf rng f by A1,Lm6;
A19:for D,D1 be Element of divs A st delta(D1)<min rng upper_volume(chi(A,A),D)
holds ex D2 be Element of divs A st D<=D2 & D1<=D2 & rng D2=rng D1 \/ rng D
& lower_sum(f,D2)-lower_sum(f,D1) <=
(len D)*(sup(rng f)-inf(rng f))*delta(D1)
proof
let D,D1 be Element of divs A;
assume A20:delta(D1)<min rng upper_volume(chi(A,A),D);
ex D2 be Element of divs A st D<=D2 & D1<=D2 & rng D2=rng D1 \/ rng D
& lower_sum(f,D2)-lower_sum(f,D1)<=(len D)*(sup(rng f)-inf(rng f))*delta(D1)
proof
consider D2 be Element of divs A such that
A21: D<=D2 & D1<=D2 & rng D2=rng D1 \/
rng D & 0<=lower_sum(f,D2)-lower_sum(f,D)
& 0<=lower_sum(f,D2)-lower_sum(f,D1) by A14;
lower_sum(f,D2)-lower_sum(f,D1) <=
(len D)*(sup(rng f)-inf(rng f))*delta(D1)
proof
deffunc PLf(Element of divs A,Nat) = (PartSums(lower_volume(f,$1))).$2;
deffunc LVf(Element of divs A) = lower_volume(f,$1);
A22: for i st i in dom D holds ex j st j in dom D1 & D.i in divset(D1,j)
& PLf(D2,indx(D2,D1,j))-PLf(D1,j)<=i*(sup(rng f)-inf(rng f))*delta(D1)
proof
let i; assume A23:i in dom D;
A24: for i,j st i in dom D & j in dom D1 & D.i in divset(D1,j) holds j >= 2
proof
let i,j;
assume A25:i in dom D;
assume A26:j in dom D1 & D.i in divset(D1,j);
assume j<2;
then j<1+1;
then A27: j <= 1 by NAT_1:38;
A28: inf divset(D1,j)<=D.i & D.i<=sup divset(D1,j) by A26,INTEGRA2:1;
j in Seg len D1 by A26,FINSEQ_1:def 3;
then j >= 1 by FINSEQ_1:3;
then j = 1 by A27,AXIOMS:21;
then A29: inf divset(D1,j)=inf A & sup divset(D1,j)=D1.j by A26,INTEGRA1:def
5;
delta(D1) >= min rng upper_volume(chi(A,A),D)
proof
per cases;
suppose A30:i=1;
len D &