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