let A be non empty closed_interval Subset of REAL; :: thesis: for x being Real
for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x))
let x be Real; :: thesis: for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x))
let n be Element of NAT ; :: thesis: ( A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] implies integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x)) )
assume A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] ; :: thesis: integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x))
then ( upper_bound A = x + (((2 * n) + 1) * PI) & lower_bound A = x + ((2 * n) * PI) ) by Th37;
then integral ((sin - cos),A) = (((- cos) . (x + (((2 * n) + 1) * PI))) - ((- cos) . (x + ((2 * n) * PI)))) - ((sin . (x + (((2 * n) + 1) * PI))) - (sin . (x + ((2 * n) * PI)))) by Th78
.= ((- (cos . (x + (((2 * n) + 1) * PI)))) - ((- cos) . (x + ((2 * n) * PI)))) - ((sin . (x + (((2 * n) + 1) * PI))) - (sin . (x + ((2 * n) * PI)))) by VALUED_1:8
.= ((- (cos (x + (((2 * n) + 1) * PI)))) - (- (cos (x + ((2 * n) * PI))))) - ((sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI)))) by VALUED_1:8
.= ((- (- (cos x))) - (- (cos (x + ((2 * n) * PI))))) - ((sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI)))) by Th4
.= ((- (- (cos x))) - (- (cos x))) - ((sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI)))) by Th3
.= ((- (- (cos x))) - (- (cos x))) - ((- (sin x)) - (sin (x + ((2 * n) * PI)))) by Th2
.= ((cos x) + (cos x)) - ((- (sin x)) - (sin x)) by Th1
.= (2 * (cos x)) + (2 * (sin x)) ;
hence integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x)) ; :: thesis: verum