let A be non empty closed_interval Subset of REAL; :: thesis: integral ((sin (#) cos),A) = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A))))
A1: [#] REAL is open Subset of REAL ;
sin | A is continuous ;
then A2: (- cos) `| REAL is_integrable_on A by Lm5, Th29, INTEGRA5:11;
(- sin) | A is continuous ;
then A3: cos `| REAL is_integrable_on A by Lm7, Th28, INTEGRA5:11;
( ((- cos) `| REAL) | A is bounded & (cos `| REAL) | A is bounded ) by Lm5, Lm7, Th28, Th29, INTEGRA5:10;
then integral ((sin (#) cos),A) = ((((- cos) . (upper_bound A)) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral (((- cos) (#) (- sin)),A)) by A2, A3, A1, Th26, Th28, Th29, INTEGRA5:21, SIN_COS:67
.= ((((- cos) . (upper_bound A)) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral ((sin (#) cos),A)) by Lm4
.= (((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral ((sin (#) cos),A)) by VALUED_1:8
.= (((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - ((- (cos . (lower_bound A))) * (cos . (lower_bound A)))) - (integral ((sin (#) cos),A)) by VALUED_1:8
.= (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) - (integral ((sin (#) cos),A)) ;
hence integral ((sin (#) cos),A) = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) ; :: thesis: verum