let y be Real; :: thesis: for A being closed-interval Subset of REAL
for f being Function of A,REAL st vol A <> 0 & y in rng (lower_sum_set f) holds
ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
let A be closed-interval Subset of REAL; :: thesis: for f being Function of A,REAL st vol A <> 0 & y in rng (lower_sum_set f) holds
ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
let f be Function of A,REAL; :: thesis: ( vol A <> 0 & y in rng (lower_sum_set f) implies ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) )
assume A1: vol A <> 0 ; :: thesis: ( not y in rng (lower_sum_set f) or ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) )
assume y in rng (lower_sum_set f) ; :: thesis: ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
then consider D3 being Element of divs A such that
A2: D3 in dom (lower_sum_set f) and
A3: y = (lower_sum_set f) . D3 by PARTFUN1:26;
reconsider D3 = D3 as Division of A by INTEGRA1:def 3;
rng D3 <> {} ;
then A4: 1 in dom D3 by FINSEQ_3:34;
A5: len D3 in Seg (len D3) by FINSEQ_1:5;
now
per cases ( D3 . 1 <> lower_bound A or D3 . 1 = lower_bound A ) ;
suppose A6: D3 . 1 <> lower_bound A ; :: thesis: ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
D3 . 1 in A by A4, INTEGRA1:8;
then lower_bound A <= D3 . 1 by INTEGRA2:1;
then D3 . 1 > lower_bound A by A6, XXREAL_0:1;
hence ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) by A2, A3; :: thesis: verum
end;
suppose A7: D3 . 1 = lower_bound A ; :: thesis: ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
proof
A8: (lower_volume (f,D3)) . 1 = (lower_bound (rng (f | (divset (D3,1))))) * (vol (divset (D3,1))) by A4, INTEGRA1:def 8;
vol A >= 0 by INTEGRA1:11;
then A9: (upper_bound A) - (lower_bound A) > 0 by A1, INTEGRA1:def 6;
A10: y = lower_sum (f,D3) by A2, A3, 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 ;
A11: D3 . (len D3) = upper_bound A by INTEGRA1:def 2;
len D3 in dom D3 by A5, FINSEQ_1:def 3;
then A12: len D3 > 1 by A4, A7, A11, A9, SEQ_4:154, XREAL_1:49;
then reconsider D = D3 /^ 1 as increasing FinSequence of REAL by INTEGRA1:36;
A13: len D = (len D3) - 1 by A12, RFINSEQ:def 2;
upper_bound A > lower_bound A by A9, XREAL_1:49;
then len D <> 0 by A7, A13, INTEGRA1:def 2;
then reconsider D = D as non empty increasing FinSequence of REAL ;
A14: len D in dom D by FINSEQ_5:6;
(len D) + 1 = len D3 by A13;
then A15: D . (len D) = upper_bound A by A11, A12, A14, RFINSEQ:def 2;
A16: len D3 >= 1 + 1 by A12, NAT_1:13;
then A17: 2 <= len (lower_volume (f,D3)) by INTEGRA1:def 8;
1 + 1 <= len D3 by A12, NAT_1:13;
then 2 in dom D3 by FINSEQ_3:27;
then A18: D3 . 1 < D3 . 2 by A4, SEQM_3:def 1;
A19: rng D3 c= A by INTEGRA1:def 2;
rng D c= rng D3 by FINSEQ_5:36;
then rng D c= A by A19, XBOOLE_1:1;
then reconsider D = D as Division of A by A15, INTEGRA1:def 2;
A20: 1 in Seg 1 by FINSEQ_1:3;
A21: 1 <= len (lower_volume (f,D3)) by A12, INTEGRA1:def 8;
then A22: len ((lower_volume (f,D3)) | 1) = 1 by FINSEQ_1:80;
1 <= len (lower_volume (f,D3)) by A12, INTEGRA1:def 8;
then A23: len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) = ((len (lower_volume (f,D3))) -' 2) + 1 by A17, FINSEQ_6:124
.= ((len D3) -' 2) + 1 by INTEGRA1:def 8
.= ((len D3) - 2) + 1 by A16, XREAL_1:235
.= (len D3) - 1 ;
A24: for i being Nat 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 be Nat; :: thesis: ( 1 <= i & i <= len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) implies (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D)) . i )
assume that
A25: 1 <= i and
A26: i <= len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) ; :: thesis: (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D)) . i
A27: 1 <= i + 1 by NAT_1:12;
i + 1 <= len D3 by A23, A26, XREAL_1:21;
then A28: i + 1 in Seg (len D3) by A27, FINSEQ_1:3;
then A29: i + 1 in dom D3 by FINSEQ_1:def 3;
A30: divset (D3,(i + 1)) = divset (D,i)
proof
A31: i + 1 in dom D3 by A28, FINSEQ_1:def 3;
A32: 1 <> i + 1 by A25, NAT_1:13;
then A33: upper_bound (divset (D3,(i + 1))) = D3 . (i + 1) by A31, INTEGRA1:def 5;
A34: i in dom D by A13, A23, A25, A26, FINSEQ_3:27;
then A35: D . i = D3 . (i + 1) by A12, RFINSEQ:def 2;
A36: lower_bound (divset (D3,(i + 1))) = D3 . ((i + 1) - 1) by A32, A31, INTEGRA1:def 5;
per cases ( i = 1 or i <> 1 ) ;
suppose A40: i <> 1 ; :: thesis: divset (D3,(i + 1)) = divset (D,i)
then i - 1 in dom D by A34, INTEGRA1:9;
then A41: D . (i - 1) = D3 . ((i - 1) + 1) by A12, RFINSEQ:def 2
.= D3 . i ;
A42: upper_bound (divset (D,i)) = D . i by A34, A40, INTEGRA1:def 5;
lower_bound (divset (D,i)) = D . (i - 1) by A34, A40, INTEGRA1:def 5;
then divset (D3,(i + 1)) = [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).] by A33, A36, A35, A42, A41, INTEGRA1:5;
hence divset (D3,(i + 1)) = divset (D,i) by INTEGRA1:5; :: thesis: verum
end;
end;
end;
i <= (len (lower_volume (f,D3))) - 1 by A23, A26, INTEGRA1:def 8;
then A43: i <= ((len (lower_volume (f,D3))) - 2) + 1 ;
i in NAT by ORDINAL1:def 13;
then (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D3)) . ((i + 2) - 1) by A17, A25, A43, FINSEQ_6:128
.= (lower_volume (f,D3)) . (i + 1) ;
then A44: (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_bound (rng (f | (divset (D3,(i + 1)))))) * (vol (divset (D3,(i + 1)))) by A29, INTEGRA1:def 8;
i in Seg (len D) by A13, A23, A25, A26, FINSEQ_1:3;
then i in dom D by FINSEQ_1:def 3;
hence (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) . i = (lower_volume (f,D)) . i by A44, A30, INTEGRA1:def 8; :: thesis: verum
end;
1 in dom (lower_volume (f,D3)) by A21, FINSEQ_3:27;
then ((lower_volume (f,D3)) | 1) . 1 = (lower_volume (f,D3)) . 1 by A20, RFINSEQ:19;
then A45: (lower_volume (f,D3)) | 1 = <*((lower_volume (f,D3)) . 1)*> by A22, FINSEQ_1:57;
A46: 2 -' 1 = 2 - 1 by XREAL_1:235
.= 1 ;
rng D <> {} ;
then 1 in dom D by FINSEQ_3:34;
then A47: D . 1 = D3 . (1 + 1) by A12, RFINSEQ:def 2
.= D3 . 2 ;
D in divs A by INTEGRA1:def 3;
then A48: D in dom (lower_sum_set f) by INTEGRA1:def 12;
len (lower_volume (f,D3)) >= 2 by A16, INTEGRA1:def 8;
then A49: mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3)))) = (lower_volume (f,D3)) /^ 1 by A46, FINSEQ_6:123;
len (mid ((lower_volume (f,D3)),2,(len (lower_volume (f,D3))))) = len (lower_volume (f,D)) by A13, A23, INTEGRA1:def 8;
then A50: (lower_volume (f,D3)) /^ 1 = lower_volume (f,D) by A49, A24, FINSEQ_1:18;
vol (divset (D3,1)) = (upper_bound (divset (D3,1))) - (lower_bound (divset (D3,1))) by INTEGRA1:def 6
.= (upper_bound (divset (D3,1))) - (lower_bound A) by A4, INTEGRA1:def 5
.= (D3 . 1) - (lower_bound A) by A4, INTEGRA1:def 5
.= 0 by A7 ;
then y = 0 + (Sum (lower_volume (f,D))) by A10, A45, A8, A50, RVSUM_1:106
.= lower_sum (f,D) by INTEGRA1:def 10 ;
then y = (lower_sum_set f) . D by A48, INTEGRA1:def 12;
hence ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) by A7, A48, A47, A18; :: thesis: verum
end;
hence ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: verum
end;
end;
end;
hence ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: verum