let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f is bounded holds

( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

let f be Function of A,REAL; :: thesis: ( f is bounded implies ( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) )

assume A1: f is bounded ; :: thesis: ( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) ; :: thesis: verum

( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

let f be Function of A,REAL; :: thesis: ( f is bounded implies ( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) )

assume A1: f is bounded ; :: thesis: ( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

hereby :: thesis: ( ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )

A3:
f | A is bounded
by A1;for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )

assume A2:
f is integrable
; :: thesis: ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )

reconsider I = integral f as Real ;

take I = I; :: thesis: for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )

thus for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, A2, Th9; :: thesis: verum

end;for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )

reconsider I = integral f as Real ;

take I = I; :: thesis: for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )

thus for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, A2, Th9; :: thesis: verum

now :: thesis: ( ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )

hence
( ex I being Real st for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )

given I being Real such that A4:
for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; :: thesis: f is integrable

A5: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds

lim (upper_sum (f,T)) = I

I = lim (lower_sum (f,T))

end;for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; :: thesis: f is integrable

A5: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds

lim (upper_sum (f,T)) = I

proof

A18:
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies lim (upper_sum (f,T)) = I )

set S = the middle_volume_Sequence of f,T;

then A9: upper_sum (f,T) is convergent by A3, INTEGRA4:9;

then A17: (upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T)) is convergent by A9;

lim ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f, the middle_volume_Sequence of f,T))) by A9, A16, SEQ_2:12

.= (lim (upper_sum (f,T))) - I by A4, A8 ;

then 0 <= (lim (upper_sum (f,T))) - I by A6, A17, SEQ_2:17;

then (lim (upper_sum (f,T))) - I = 0 by A10, XREAL_1:5;

hence lim (upper_sum (f,T)) = I ; :: thesis: verum

end;set S = the middle_volume_Sequence of f,T;

A6: now :: thesis: for i being Nat holds 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i

assume A8:
( delta T is convergent & lim (delta T) = 0 )
; :: thesis: lim (upper_sum (f,T)) = Ilet i be Nat; :: thesis: 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i

A7: i in NAT by ORDINAL1:def 12;

(middle_sum (f, the middle_volume_Sequence of f,T)) . i <= (upper_sum (f,T)) . i by A3, Th6, A7;

then ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) <= ((upper_sum (f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) by XREAL_1:9;

hence 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i by VALUED_1:15, A7; :: thesis: verum

end;A7: i in NAT by ORDINAL1:def 12;

(middle_sum (f, the middle_volume_Sequence of f,T)) . i <= (upper_sum (f,T)) . i by A3, Th6, A7;

then ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) <= ((upper_sum (f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) by XREAL_1:9;

hence 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i by VALUED_1:15, A7; :: thesis: verum

then A9: upper_sum (f,T) is convergent by A3, INTEGRA4:9;

A10: now :: thesis: for e1 being Real st 0 < e1 holds

(lim (upper_sum (f,T))) - I <= e1

A16:
middle_sum (f, the middle_volume_Sequence of f,T) is convergent
by A4, A8;(lim (upper_sum (f,T))) - I <= e1

let e1 be Real; :: thesis: ( 0 < e1 implies (lim (upper_sum (f,T))) - I <= e1 )

reconsider e = e1 as Element of REAL by XREAL_0:def 1;

assume 0 < e1 ; :: thesis: (lim (upper_sum (f,T))) - I <= e1

then consider S being middle_volume_Sequence of f,T such that

A11: for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A3, Th8;

then A15: (upper_sum (f,T)) - (middle_sum (f,S)) is convergent by A9;

lim ((upper_sum (f,T)) - (middle_sum (f,S))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f,S))) by A9, A14, SEQ_2:12

.= (lim (upper_sum (f,T))) - I by A4, A8 ;

hence (lim (upper_sum (f,T))) - I <= e1 by A12, A15, PREPOWER:2; :: thesis: verum

end;reconsider e = e1 as Element of REAL by XREAL_0:def 1;

assume 0 < e1 ; :: thesis: (lim (upper_sum (f,T))) - I <= e1

then consider S being middle_volume_Sequence of f,T such that

A11: for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A3, Th8;

A12: now :: thesis: for i being Nat holds ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e

A14:
middle_sum (f,S) is convergent
by A4, A8;let i be Nat; :: thesis: ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e

A13: i in NAT by ORDINAL1:def 12;

((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A11, A13;

then (((upper_sum (f,T)) . i) - e) + e <= ((middle_sum (f,S)) . i) + e by XREAL_1:6;

then ((upper_sum (f,T)) . i) - ((middle_sum (f,S)) . i) <= (((middle_sum (f,S)) . i) + e) - ((middle_sum (f,S)) . i) by XREAL_1:9;

hence ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e by VALUED_1:15, A13; :: thesis: verum

end;A13: i in NAT by ORDINAL1:def 12;

((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A11, A13;

then (((upper_sum (f,T)) . i) - e) + e <= ((middle_sum (f,S)) . i) + e by XREAL_1:6;

then ((upper_sum (f,T)) . i) - ((middle_sum (f,S)) . i) <= (((middle_sum (f,S)) . i) + e) - ((middle_sum (f,S)) . i) by XREAL_1:9;

hence ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e by VALUED_1:15, A13; :: thesis: verum

then A15: (upper_sum (f,T)) - (middle_sum (f,S)) is convergent by A9;

lim ((upper_sum (f,T)) - (middle_sum (f,S))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f,S))) by A9, A14, SEQ_2:12

.= (lim (upper_sum (f,T))) - I by A4, A8 ;

hence (lim (upper_sum (f,T))) - I <= e1 by A12, A15, PREPOWER:2; :: thesis: verum

then A17: (upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T)) is convergent by A9;

lim ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f, the middle_volume_Sequence of f,T))) by A9, A16, SEQ_2:12

.= (lim (upper_sum (f,T))) - I by A4, A8 ;

then 0 <= (lim (upper_sum (f,T))) - I by A6, A17, SEQ_2:17;

then (lim (upper_sum (f,T))) - I = 0 by A10, XREAL_1:5;

hence lim (upper_sum (f,T)) = I ; :: thesis: verum

I = lim (lower_sum (f,T))

proof

let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies I = lim (lower_sum (f,T)) )

set S = the middle_volume_Sequence of f,T;

then A22: lower_sum (f,T) is convergent by A3, INTEGRA4:8;

then A30: (middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T)) is convergent by A22;

lim ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) = (lim (middle_sum (f, the middle_volume_Sequence of f,T))) - (lim (lower_sum (f,T))) by A22, A29, SEQ_2:12

.= I - (lim (lower_sum (f,T))) by A4, A21 ;

then 0 <= I - (lim (lower_sum (f,T))) by A19, A30, SEQ_2:17;

then I - (lim (lower_sum (f,T))) = 0 by A23, XREAL_1:5;

hence I = lim (lower_sum (f,T)) ; :: thesis: verum

end;set S = the middle_volume_Sequence of f,T;

A19: now :: thesis: for i being Nat holds 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i

assume A21:
( delta T is convergent & lim (delta T) = 0 )
; :: thesis: I = lim (lower_sum (f,T))let i be Nat; :: thesis: 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i

A20: i in NAT by ORDINAL1:def 12;

(lower_sum (f,T)) . i <= (middle_sum (f, the middle_volume_Sequence of f,T)) . i by A3, Th5, A20;

then ((lower_sum (f,T)) . i) - ((lower_sum (f,T)) . i) <= ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((lower_sum (f,T)) . i) by XREAL_1:9;

hence 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i by VALUED_1:15, A20; :: thesis: verum

end;A20: i in NAT by ORDINAL1:def 12;

(lower_sum (f,T)) . i <= (middle_sum (f, the middle_volume_Sequence of f,T)) . i by A3, Th5, A20;

then ((lower_sum (f,T)) . i) - ((lower_sum (f,T)) . i) <= ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((lower_sum (f,T)) . i) by XREAL_1:9;

hence 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i by VALUED_1:15, A20; :: thesis: verum

then A22: lower_sum (f,T) is convergent by A3, INTEGRA4:8;

A23: now :: thesis: for e1 being Real st 0 < e1 holds

I - (lim (lower_sum (f,T))) <= e1

A29:
middle_sum (f, the middle_volume_Sequence of f,T) is convergent
by A4, A21;I - (lim (lower_sum (f,T))) <= e1

let e1 be Real; :: thesis: ( 0 < e1 implies I - (lim (lower_sum (f,T))) <= e1 )

reconsider e = e1 as Element of REAL by XREAL_0:def 1;

assume 0 < e1 ; :: thesis: I - (lim (lower_sum (f,T))) <= e1

then consider S being middle_volume_Sequence of f,T such that

A24: for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A3, Th7;

then A28: (middle_sum (f,S)) - (lower_sum (f,T)) is convergent by A22;

lim ((middle_sum (f,S)) - (lower_sum (f,T))) = (lim (middle_sum (f,S))) - (lim (lower_sum (f,T))) by A22, A27, SEQ_2:12

.= I - (lim (lower_sum (f,T))) by A4, A21 ;

hence I - (lim (lower_sum (f,T))) <= e1 by A25, A28, PREPOWER:2; :: thesis: verum

end;reconsider e = e1 as Element of REAL by XREAL_0:def 1;

assume 0 < e1 ; :: thesis: I - (lim (lower_sum (f,T))) <= e1

then consider S being middle_volume_Sequence of f,T such that

A24: for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A3, Th7;

A25: now :: thesis: for i being Nat holds ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e

A27:
middle_sum (f,S) is convergent
by A4, A21;let i be Nat; :: thesis: ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e

A26: i in NAT by ORDINAL1:def 12;

(middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A24, A26;

then ((middle_sum (f,S)) . i) - ((lower_sum (f,T)) . i) <= (((lower_sum (f,T)) . i) + e) - ((lower_sum (f,T)) . i) by XREAL_1:9;

hence ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e by VALUED_1:15, A26; :: thesis: verum

end;A26: i in NAT by ORDINAL1:def 12;

(middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A24, A26;

then ((middle_sum (f,S)) . i) - ((lower_sum (f,T)) . i) <= (((lower_sum (f,T)) . i) + e) - ((lower_sum (f,T)) . i) by XREAL_1:9;

hence ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e by VALUED_1:15, A26; :: thesis: verum

then A28: (middle_sum (f,S)) - (lower_sum (f,T)) is convergent by A22;

lim ((middle_sum (f,S)) - (lower_sum (f,T))) = (lim (middle_sum (f,S))) - (lim (lower_sum (f,T))) by A22, A27, SEQ_2:12

.= I - (lim (lower_sum (f,T))) by A4, A21 ;

hence I - (lim (lower_sum (f,T))) <= e1 by A25, A28, PREPOWER:2; :: thesis: verum

then A30: (middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T)) is convergent by A22;

lim ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) = (lim (middle_sum (f, the middle_volume_Sequence of f,T))) - (lim (lower_sum (f,T))) by A22, A29, SEQ_2:12

.= I - (lim (lower_sum (f,T))) by A4, A21 ;

then 0 <= I - (lim (lower_sum (f,T))) by A19, A30, SEQ_2:17;

then I - (lim (lower_sum (f,T))) = 0 by A23, XREAL_1:5;

hence I = lim (lower_sum (f,T)) ; :: thesis: verum

now :: thesis: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds

(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0

hence
f is integrable
by A3, INTEGRA4:12; :: thesis: verum(lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0

let T be DivSequence of A; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 )

assume A31: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0

hence (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = (lim (upper_sum (f,T))) - I by A18

.= I - I by A5, A31

.= 0 ;

:: thesis: verum

end;assume A31: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0

hence (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = (lim (upper_sum (f,T))) - I by A18

.= I - I by A5, A31

.= 0 ;

:: thesis: verum

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) ; :: thesis: verum