let A be closed-interval Subset of REAL ; :: thesis: for x being Real
for n being Element of NAT st A = [.(x + ((2 * n) * PI )),(x + (((2 * n) + 1) * PI )).] holds
integral (sin + cos ),A = (2 * (cos x)) - (2 * (sin x))
let x be Real; :: thesis: for n being Element of NAT st A = [.(x + ((2 * n) * PI )),(x + (((2 * n) + 1) * PI )).] holds
integral (sin + cos ),A = (2 * (cos x)) - (2 * (sin x))
let n be Element of NAT ; :: thesis: ( A = [.(x + ((2 * n) * PI )),(x + (((2 * n) + 1) * PI )).] implies integral (sin + cos ),A = (2 * (cos x)) - (2 * (sin x)) )
assume A = [.(x + ((2 * n) * PI )),(x + (((2 * n) + 1) * PI )).] ; :: thesis: integral (sin + cos ),A = (2 * (cos x)) - (2 * (sin x))
then ( upper_bound A = x + (((2 * n) + 1) * PI ) & lower_bound A = x + ((2 * n) * PI ) ) by Th37;
then integral (sin + cos ),A = ((((- cos ) . (x + (((2 * n) + 1) * PI ))) - ((- cos ) . (x + ((2 * n) * PI )))) + (sin . (x + (((2 * n) + 1) * PI )))) - (sin . (x + ((2 * n) * PI ))) by Th69
.= (((- (cos . (x + (((2 * n) + 1) * PI )))) - ((- cos ) . (x + ((2 * n) * PI )))) + (sin . (x + (((2 * n) + 1) * PI )))) - (sin . (x + ((2 * n) * PI ))) by VALUED_1:8
.= (((- (cos (x + (((2 * n) + 1) * PI )))) - (- (cos (x + ((2 * n) * PI ))))) + (sin (x + (((2 * n) + 1) * PI )))) - (sin (x + ((2 * n) * PI ))) by VALUED_1:8
.= (((- (- (cos x))) - (- (cos (x + ((2 * n) * PI ))))) + (sin (x + (((2 * n) + 1) * PI )))) - (sin (x + ((2 * n) * PI ))) by Th4
.= (((- (- (cos x))) - (- (cos x))) + (sin (x + (((2 * n) + 1) * PI )))) - (sin (x + ((2 * n) * PI ))) by Th3
.= (((- (- (cos x))) - (- (cos x))) + (- (sin x))) - (sin (x + ((2 * n) * PI ))) by Th2
.= (((cos x) + (cos x)) - (sin x)) - (sin x) by Th1
.= (2 * (cos x)) - (2 * (sin x)) ;
hence integral (sin + cos ),A = (2 * (cos x)) - (2 * (sin x)) ; :: thesis: verum