let A be closed-interval Subset of REAL ; 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 ; ( A = [.((2 * n) * PI ),(((2 * n) + 1) * PI ).] implies integral (sin + cos ),A = 2 )
assume
A = [.((2 * n) * PI ),(((2 * n) + 1) * PI ).]
; 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: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
; verum