let n be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL st A = [.(- (PI / 2)),(PI / 2).] holds
integral (((#Z n) * cos ) (#) sin ),A = 0
let A be closed-interval Subset of REAL ; :: thesis: ( A = [.(- (PI / 2)),(PI / 2).] implies integral (((#Z n) * cos ) (#) sin ),A = 0 )
assume A = [.(- (PI / 2)),(PI / 2).] ; :: thesis: integral (((#Z n) * cos ) (#) sin ),A = 0
then ( upper_bound A = PI / 2 & lower_bound A = - (PI / 2) ) by INTEGRA8:37;
then integral (((#Z n) * cos ) (#) sin ),A = (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) . (PI / 2)) - (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) . (- (PI / 2))) by Th22
.= ((- (1 / (n + 1))) * (((#Z (n + 1)) * cos ) . (PI / 2))) - (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) . (- (PI / 2))) by VALUED_1:6
.= ((- (1 / (n + 1))) * (((#Z (n + 1)) * cos ) . (PI / 2))) - ((- (1 / (n + 1))) * (((#Z (n + 1)) * cos ) . (- (PI / 2)))) by VALUED_1:6
.= ((- (1 / (n + 1))) * ((#Z (n + 1)) . (cos . (PI / 2)))) - ((- (1 / (n + 1))) * (((#Z (n + 1)) * cos ) . (- (PI / 2)))) by FUNCT_1:23, SIN_COS:27
.= ((- (1 / (n + 1))) * ((#Z (n + 1)) . (cos . (PI / 2)))) - ((- (1 / (n + 1))) * ((#Z (n + 1)) . (cos . (- (PI / 2))))) by FUNCT_1:23, SIN_COS:27
.= ((- (1 / (n + 1))) * ((#Z (n + 1)) . (cos . (PI / 2)))) - ((- (1 / (n + 1))) * ((#Z (n + 1)) . (cos . (PI / 2)))) by SIN_COS:33
.= 0 ;
hence integral (((#Z n) * cos ) (#) sin ),A = 0 ; :: thesis: verum