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 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:84
.= 0 - 0 by SIN_COS:82, SIN_COS:84 ;
hence integral cos ,A = 0 ; :: thesis: verum