let A be closed-interval Subset of REAL ; :: thesis: for n being Element of NAT st A = [.((2 * n) * PI ),(((2 * n) + 1) * PI ).] holds
integral (sin (#) cos ),A = 0
let n be Element of NAT ; :: thesis: ( A = [.((2 * n) * PI ),(((2 * n) + 1) * PI ).] implies integral (sin (#) cos ),A = 0 )
assume A = [.((2 * n) * PI ),(((2 * n) + 1) * PI ).] ; :: thesis: integral (sin (#) cos ),A = 0
then ( upper_bound A = ((2 * n) + 1) * PI & lower_bound A = (2 * n) * PI ) by Th37;
then integral (sin (#) cos ),A = (1 / 2) * (((cos . ((2 * n) * PI )) * (cos . ((2 * n) * PI ))) - ((cos . (((2 * n) + 1) * PI )) * (cos . (((2 * n) + 1) * PI )))) by Th90
.= (1 / 2) * (((cos 0 ) * (cos (0 + ((2 * n) * PI )))) - ((cos . (((2 * n) + 1) * PI )) * (cos . (((2 * n) + 1) * PI )))) by Th3
.= (1 / 2) * (((cos 0 ) * (cos 0 )) - ((cos . (((2 * n) + 1) * PI )) * (cos . (((2 * n) + 1) * PI )))) by Th3
.= (1 / 2) * (((cos (0 + (2 * PI ))) * (cos 0 )) - ((cos . (((2 * n) + 1) * PI )) * (cos . (((2 * n) + 1) * PI )))) by SIN_COS:84
.= (1 / 2) * ((1 * 1) - ((cos . (((2 * n) + 1) * PI )) * (cos . (((2 * n) + 1) * PI )))) by SIN_COS:82, SIN_COS:84
.= (1 / 2) * ((1 * 1) - ((- (cos 0 )) * (cos (0 + (((2 * n) + 1) * PI ))))) by Th4
.= (1 / 2) * ((1 * 1) - ((- (cos 0 )) * (- (cos 0 )))) by Th4
.= (1 / 2) * ((1 * 1) - ((cos 0 ) * (cos 0 )))
.= (1 / 2) * ((1 * 1) - ((cos (0 + (2 * PI ))) * (cos 0 ))) by SIN_COS:84
.= (1 / 2) * ((1 * 1) - ((cos (0 + (2 * PI ))) * (cos (0 + (2 * PI ))))) by SIN_COS:84 ;
hence integral (sin (#) cos ),A = 0 by SIN_COS:82; :: thesis: verum