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