let A be non empty 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:79
.= (1 / 2) * ((1 * 1) - ((cos . (((2 * n) + 1) * PI)) * (cos . (((2 * n) + 1) * PI)))) by SIN_COS:77, SIN_COS:79
.= (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:79
.= (1 / 2) * ((1 * 1) - ((cos (0 + (2 * PI))) * (cos (0 + (2 * PI))))) by SIN_COS:79 ;
hence integral ((sin (#) cos),A) = 0 by SIN_COS:77; :: thesis: verum