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 (cos,A) = 0
let n be Element of NAT ; :: thesis: ( A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] implies integral (cos,A) = 0 )
assume A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] ; :: thesis: integral (cos,A) = 0
then ( upper_bound A = ((2 * n) + 1) * PI & lower_bound A = (2 * n) * PI ) by Th37;
then integral (cos,A) = (sin (0 + (((2 * n) + 1) * PI))) - (sin (0 + ((2 * n) * PI))) by Th39
.= (- (sin 0)) - (sin (0 + ((2 * n) * PI))) by Th2
.= (- (sin 0)) - (sin 0) by Th1
.= (- (sin (0 + (2 * PI)))) - (sin 0) by SIN_COS:79
.= 0 - 0 by SIN_COS:77, SIN_COS:79 ;
hence integral (cos,A) = 0 ; :: thesis: verum