let r be Real; :: thesis: for A being closed-interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)
let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL
for D being Division of A st f | A is bounded & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)
let f be Function of A,REAL ; :: thesis: for D being Division of A st f | A is bounded & r <= 0 holds
(lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)
let D be Division of A; :: thesis: ( f | A is bounded & r <= 0 implies (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) )
assume that
A1: f | A is bounded and
A2: r <= 0 ; :: thesis: (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A)
A3: dom (lower_sum_set (r (#) f)) = divs A by INTEGRA1:def 12;
X: (r (#) f) | A is bounded by A1, RFUNCT_1:97;
then A4: ( (r (#) f) | A is bounded_below & (r (#) f) | A is bounded_above ) ;
( f | A is bounded_below & f | A is bounded_above ) by A1;
then A5: rng f is bounded_below by INTEGRA1:13;
D in divs A by INTEGRA1:def 3;
then (lower_sum_set (r (#) f)) . D = lower_sum (r (#) f),D by A3, INTEGRA1:def 12;
then A6: (lower_sum_set (r (#) f)) . D <= upper_sum (r (#) f),D by X, INTEGRA1:30;
A7: upper_sum (r (#) f),D <= (upper_bound (rng (r (#) f))) * (vol A) by A4, INTEGRA1:29;
upper_bound (rng (r (#) f)) = upper_bound (r ** (rng f)) by Th17
.= r * (lower_bound (rng f)) by A2, A5, Th16 ;
hence (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) by A6, A7, XXREAL_0:2; :: thesis: verum