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 = 0
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 = 0
let n be Element of NAT ; :: thesis: ( A = [.(x + ((2 * n) * PI )),(x + (((2 * n) + 1) * PI )).] implies integral (sin (#) cos ),A = 0 )
assume A = [.(x + ((2 * n) * PI )),(x + (((2 * n) + 1) * PI )).] ; :: thesis: integral (sin (#) cos ),A = 0
then ( upper_bound A = x + (((2 * n) + 1) * PI ) & lower_bound A = x + ((2 * n) * PI ) ) by Th37;
then integral (sin (#) cos ),A = (1 / 2) * (((cos . (x + ((2 * n) * PI ))) * (cos . (x + ((2 * n) * PI )))) - ((cos . (x + (((2 * n) + 1) * PI ))) * (cos . (x + (((2 * n) + 1) * PI ))))) by Th90
.= (1 / 2) * (((cos x) * (cos (x + ((2 * n) * PI )))) - ((cos (x + (((2 * n) + 1) * PI ))) * (cos (x + (((2 * n) + 1) * PI ))))) by Th3
.= (1 / 2) * (((cos x) * (cos x)) - ((cos (x + (((2 * n) + 1) * PI ))) * (cos (x + (((2 * n) + 1) * PI ))))) by Th3
.= (1 / 2) * (((cos x) * (cos x)) - ((- (cos x)) * (cos (x + (((2 * n) + 1) * PI ))))) by Th4
.= (1 / 2) * (((cos x) * (cos x)) - ((- (cos x)) * (- (cos x)))) by Th4
.= 0 ;
hence integral (sin (#) cos ),A = 0 ; :: thesis: verum