let n be Element of NAT ; for A being non empty closed_interval Subset of REAL st A = [.0,(2 * PI).] holds
integral ((((#Z n) * cos) (#) sin),A) = 0
let A be non empty closed_interval Subset of REAL; ( A = [.0,(2 * PI).] implies integral ((((#Z n) * cos) (#) sin),A) = 0 )
assume
A = [.0,(2 * PI).]
; integral ((((#Z n) * cos) (#) sin),A) = 0
then
( upper_bound A = 2 * PI & lower_bound A = 0 )
by INTEGRA8:37;
then integral ((((#Z n) * cos) (#) sin),A) =
(((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . (2 * PI)) - (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . 0)
by Th22
.=
((- (1 / (n + 1))) * (((#Z (n + 1)) * cos) . (2 * PI))) - (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . 0)
by VALUED_1:6
.=
((- (1 / (n + 1))) * (((#Z (n + 1)) * cos) . (2 * PI))) - ((- (1 / (n + 1))) * (((#Z (n + 1)) * cos) . 0))
by VALUED_1:6
.=
((- (1 / (n + 1))) * ((#Z (n + 1)) . (cos . dp))) - ((- (1 / (n + 1))) * (((#Z (n + 1)) * cos) . 0))
by FUNCT_1:13, SIN_COS:24
.=
((- (1 / (n + 1))) * ((#Z (n + 1)) . (cos . (2 * PI)))) - ((- (1 / (n + 1))) * ((#Z (n + 1)) . (cos . 0)))
by FUNCT_1:13, SIN_COS:24, Lm6
.=
0
by SIN_COS:30, SIN_COS:76
;
hence
integral ((((#Z n) * cos) (#) sin),A) = 0
; verum