let A be non empty closed_interval Subset of REAL; :: thesis: for X being set
for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds
integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A))
let X be set ; :: thesis: for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds
integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A))
let f be PartFunc of REAL,REAL; :: thesis: ( A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded implies integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) )
assume that
A1: ( A c= X & f is_differentiable_on X ) and
A2: f `| X is_integrable_on A and
A3: (f `| X) | A is bounded ; :: thesis: integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A))
(f `| X) || A is integrable by A2;
then A4: upper_integral ((f `| X) || A) = lower_integral ((f `| X) || A) by INTEGRA1:def 16;
A5: for r being Real st r in rng (upper_sum_set ((f `| X) || A)) holds
(f . (upper_bound A)) - (f . (lower_bound A)) <= r
proof
let r be Real; :: thesis: ( r in rng (upper_sum_set ((f `| X) || A)) implies (f . (upper_bound A)) - (f . (lower_bound A)) <= r )
assume r in rng (upper_sum_set ((f `| X) || A)) ; :: thesis: (f . (upper_bound A)) - (f . (lower_bound A)) <= r
then consider D being Element of divs A such that
A6: ( D in dom (upper_sum_set ((f `| X) || A)) & r = (upper_sum_set ((f `| X) || A)) . D ) by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = upper_sum (((f `| X) || A),D) by A6, INTEGRA1:def 10;
hence (f . (upper_bound A)) - (f . (lower_bound A)) <= r by A1, A3, Th12; :: thesis: verum
end;
(f . (upper_bound A)) - (f . (lower_bound A)) <= lower_bound (rng (upper_sum_set ((f `| X) || A))) by A5, SEQ_4:43;
then A7: upper_integral ((f `| X) || A) >= (f . (upper_bound A)) - (f . (lower_bound A)) by INTEGRA1:def 14;
A8: for r being Real st r in rng (lower_sum_set ((f `| X) || A)) holds
r <= (f . (upper_bound A)) - (f . (lower_bound A))
proof
let r be Real; :: thesis: ( r in rng (lower_sum_set ((f `| X) || A)) implies r <= (f . (upper_bound A)) - (f . (lower_bound A)) )
assume r in rng (lower_sum_set ((f `| X) || A)) ; :: thesis: r <= (f . (upper_bound A)) - (f . (lower_bound A))
then consider D being Element of divs A such that
A9: ( D in dom (lower_sum_set ((f `| X) || A)) & r = (lower_sum_set ((f `| X) || A)) . D ) by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = lower_sum (((f `| X) || A),D) by A9, INTEGRA1:def 11;
hence r <= (f . (upper_bound A)) - (f . (lower_bound A)) by A1, A3, Th12; :: thesis: verum
end;
upper_bound (rng (lower_sum_set ((f `| X) || A))) <= (f . (upper_bound A)) - (f . (lower_bound A)) by A8, SEQ_4:45;
then upper_integral ((f `| X) || A) <= (f . (upper_bound A)) - (f . (lower_bound A)) by A4, INTEGRA1:def 15;
then upper_integral ((f `| X) || A) = (f . (upper_bound A)) - (f . (lower_bound A)) by A7, XXREAL_0:1;
hence integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) by INTEGRA1:def 17; :: thesis: verum