let i, n be Nat; :: thesis: for A being non empty closed_interval Subset of REAL holds integral ((((- 1) |^ i) (#) ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))),A) = (((- 1) |^ i) * (((1 / ((2 * n) + 1)) * ((upper_bound A) |^ ((2 * n) + 1))) - ((1 / ((2 * n) + 1)) * ((lower_bound A) |^ ((2 * n) + 1))))) + (integral ((((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A))
let A be non empty closed_interval Subset of REAL; :: thesis: integral ((((- 1) |^ i) (#) ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))),A) = (((- 1) |^ i) * (((1 / ((2 * n) + 1)) * ((upper_bound A) |^ ((2 * n) + 1))) - ((1 / ((2 * n) + 1)) * ((lower_bound A) |^ ((2 * n) + 1))))) + (integral ((((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A))
set II = (- 1) |^ i;
set i1 = i + 1;
set n1 = n + 1;
set II1 = (- 1) |^ (i + 1);
set Z0 = #Z 0;
set Z2 = #Z 2;
set Z2n = #Z (2 * n);
set f = ((- 1) |^ i) (#) (#Z (2 * n));
set g = ((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)));
A1: dom ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) = dom (((- 1) |^ i) (#) ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))) by VALUED_1:def 5;
dom ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2))) = dom (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))) by VALUED_1:def 5;
then A2: dom (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))) = REAL by Th4;
A3: dom (((- 1) |^ i) (#) (#Z (2 * n))) = REAL by FUNCT_2:def 1;
then A4: dom ((((- 1) |^ i) (#) (#Z (2 * n))) + (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2))))) = REAL /\ REAL by A2, VALUED_1:def 1;
for x being Element of REAL holds (((- 1) |^ i) (#) ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))) . x = ((((- 1) |^ i) (#) (#Z (2 * n))) + (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2))))) . x
proof
let x be Element of REAL ; :: thesis: (((- 1) |^ i) (#) ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))) . x = ((((- 1) |^ i) (#) (#Z (2 * n))) + (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2))))) . x
x |^ (((2 * n) + 1) + 1) = x * (x |^ ((2 * n) + 1)) by NEWTON:6
.= x * (x * (x |^ (2 * n))) by NEWTON:6 ;
then (x |^ (2 * n)) + (x |^ (2 * (n + 1))) = (x |^ (2 * n)) * (1 + (x ^2)) ;
then A5: ((x |^ (2 * n)) + (x |^ (2 * (n + 1)))) / (1 + (x ^2)) = x |^ (2 * n) by XCMPLX_1:89;
A6: - (((- 1) |^ i) * ((x |^ (2 * (n + 1))) / (1 + (x ^2)))) = ((- 1) * ((- 1) |^ i)) * ((x |^ (2 * (n + 1))) / (1 + (x ^2)))
.= ((- 1) |^ (i + 1)) * ((x |^ (2 * (n + 1))) / (1 + (x ^2))) by NEWTON:6 ;
x |^ (2 * n) = x #Z (2 * n) by PREPOWER:36
.= (#Z (2 * n)) . x by TAYLOR_1:def 1 ;
then A7: ((- 1) |^ i) * (x |^ (2 * n)) = (((- 1) |^ i) (#) (#Z (2 * n))) . x by VALUED_1:6;
A8: ((- 1) |^ (i + 1)) * ((x |^ (2 * (n + 1))) / (1 + (x ^2))) = ((- 1) |^ (i + 1)) * (((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2))) . x) by Th4
.= (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))) . x by VALUED_1:6 ;
thus (((- 1) |^ i) (#) ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))) . x = ((- 1) |^ i) * (((#Z (2 * n)) / ((#Z 0) + (#Z 2))) . x) by VALUED_1:6
.= ((- 1) |^ i) * ((x |^ (2 * n)) / (1 + (x ^2))) by Th4
.= ((- 1) |^ i) * ((x |^ (2 * n)) - ((x |^ (2 * (n + 1))) / (1 + (x ^2)))) by A5
.= (((- 1) |^ i) * (x |^ (2 * n))) + (((- 1) |^ (i + 1)) * ((x |^ (2 * (n + 1))) / (1 + (x ^2)))) by A6
.= ((((- 1) |^ i) (#) (#Z (2 * n))) + (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2))))) . x by A7, A8, A4, VALUED_1:def 1 ; :: thesis: verum
end;
then A9: (((- 1) |^ i) (#) (#Z (2 * n))) + (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))) = ((- 1) |^ i) (#) ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) by A1, Th4, A4;
A10: dom (#Z (2 * n)) = REAL by FUNCT_2:def 1;
( (((- 1) |^ i) (#) (#Z (2 * n))) | A is continuous & (#Z (2 * n)) | A is continuous ) ;
then A11: ( ((- 1) |^ i) (#) (#Z (2 * n)) is_integrable_on A & (((- 1) |^ i) (#) (#Z (2 * n))) | A is bounded & #Z (2 * n) is_integrable_on A & (#Z (2 * n)) | A is bounded ) by A10, INTEGRA5:10, INTEGRA5:11, A3;
(#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)) is continuous by Th4;
then (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))) | A is continuous ;
then A12: ( ((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2))) is_integrable_on A & (((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))) | A is bounded ) by INTEGRA5:10, INTEGRA5:11, A2;
A13: 2 * n in NAT by ORDINAL1:def 12;
thus integral ((((- 1) |^ i) (#) ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))),A) = (integral ((((- 1) |^ i) (#) (#Z (2 * n))),A)) + (integral ((((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A)) by A3, A2, A11, A12, A9, INTEGRA6:11
.= (((- 1) |^ i) * (integral ((#Z (2 * n)),A))) + (integral ((((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A)) by A10, A11, INTEGRA6:9
.= (((- 1) |^ i) * (((1 / ((2 * n) + 1)) * ((upper_bound A) |^ ((2 * n) + 1))) - ((1 / ((2 * n) + 1)) * ((lower_bound A) |^ ((2 * n) + 1))))) + (integral ((((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A)) by INTEGRA9:19, A13 ; :: thesis: verum