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