let k be Nat; :: thesis: for r being Complex holds OddEvenPowers (r,((2 * (k + 1)) + 1)) = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> ^ (OddEvenPowers (r,((2 * k) + 1)))
let r be Complex; :: thesis: OddEvenPowers (r,((2 * (k + 1)) + 1)) = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> ^ (OddEvenPowers (r,((2 * k) + 1)))
set n = (2 * (k + 1)) + 1;
set N = (2 * k) + 1;
set f = OddEvenPowers (r,((2 * (k + 1)) + 1));
set p = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*>;
set q = OddEvenPowers (r,((2 * k) + 1));
A1: len (OddEvenPowers (r,((2 * (k + 1)) + 1))) = (2 * (k + 1)) + 1 by Def3;
A2: len <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> = 2 by FINSEQ_1:44;
A3: len (OddEvenPowers (r,((2 * k) + 1))) = (2 * k) + 1 by Def3;
A4: dom (OddEvenPowers (r,((2 * (k + 1)) + 1))) = Seg ((len <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*>) + (len (OddEvenPowers (r,((2 * k) + 1))))) by A1, A2, A3, FINSEQ_1:def 3;
A5: for x being Nat st x in dom <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> holds
(OddEvenPowers (r,((2 * (k + 1)) + 1))) . x = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> . x

proof

let x be Nat; :: thesis: ( x in dom <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> implies (OddEvenPowers (r,((2 * (k + 1)) + 1))) . x = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> . x )
assume x in dom <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> ; :: thesis: (OddEvenPowers (r,((2 * (k + 1)) + 1))) . x = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> . x
then ( 1 <= x & x <= 2 ) by A2, FINSEQ_3:25;
then not not x = 1 + 0 & ... & not x = 1 + 1 by NAT_1:62;

per cases then ( x = 1 or x = 2 ) ;

suppose A6: x = 1 ; :: thesis: (OddEvenPowers (r,((2 * (k + 1)) + 1))) . x = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> . x

set m = ((2 * (k + 1)) + 1) - 1;
1 <= (2 * (k + 1)) + 1 by NAT_1:11;
then (OddEvenPowers (r,((2 * (k + 1)) + 1))) . ((2 * 0) + 1) = r |^ (((2 * (k + 1)) + 1) - 1) by Def3;
hence (OddEvenPowers (r,((2 * (k + 1)) + 1))) . x = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> . x by A6; :: thesis: verum

end;

suppose A7: x = 2 ; :: thesis: (OddEvenPowers (r,((2 * (k + 1)) + 1))) . x = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> . x

A8: (2 * (k + 1)) + 1 = ((2 * k) + 1) + 2 ;
then A9: 2 <= (2 * (k + 1)) + 1 by NAT_1:11;
reconsider m = ((2 * (k + 1)) + 1) - (2 * 1) as Element of NAT by A8;
(OddEvenPowers (r,((2 * (k + 1)) + 1))) . (2 * 1) = - (r |^ m) by A9, Def3;
hence (OddEvenPowers (r,((2 * (k + 1)) + 1))) . x = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> . x by A7; :: thesis: verum

end;

end;

end;

for x being Nat st x in dom (OddEvenPowers (r,((2 * k) + 1))) holds
(OddEvenPowers (r,((2 * (k + 1)) + 1))) . ((len <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*>) + x) = (OddEvenPowers (r,((2 * k) + 1))) . x

proof

let x be Nat; :: thesis: ( x in dom (OddEvenPowers (r,((2 * k) + 1))) implies (OddEvenPowers (r,((2 * (k + 1)) + 1))) . ((len <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*>) + x) = (OddEvenPowers (r,((2 * k) + 1))) . x )
assume A10: x in dom (OddEvenPowers (r,((2 * k) + 1))) ; :: thesis: (OddEvenPowers (r,((2 * (k + 1)) + 1))) . ((len <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*>) + x) = (OddEvenPowers (r,((2 * k) + 1))) . x
A11: 1 <= x by A10, FINSEQ_3:25;
A12: x <= (2 * k) + 1 by A3, A10, FINSEQ_3:25;
x <= x + 2 by NAT_1:11;
then A13: 1 <= x + 2 by A11, XXREAL_0:2;
A14: x + 2 <= ((2 * k) + 1) + 2 by A12, XREAL_1:6;
reconsider m = ((2 * k) + 1) - x as Element of NAT by A12, INT_1:5;
reconsider m2 = ((2 * (k + 1)) + 1) - (x + 2) as Element of NAT by A14, INT_1:5;

per cases ( x is odd or x is even ) ;

suppose A15: x is odd ; :: thesis: (OddEvenPowers (r,((2 * (k + 1)) + 1))) . ((len <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*>) + x) = (OddEvenPowers (r,((2 * k) + 1))) . x

then A16: (OddEvenPowers (r,((2 * k) + 1))) . x = r |^ m by A11, A12, Def3;
(OddEvenPowers (r,((2 * (k + 1)) + 1))) . (x + 2) = r |^ m2 by A13, A14, A15, Def3;
hence (OddEvenPowers (r,((2 * (k + 1)) + 1))) . ((len <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*>) + x) = (OddEvenPowers (r,((2 * k) + 1))) . x by A16, FINSEQ_1:44; :: thesis: verum

end;

suppose A17: x is even ; :: thesis: (OddEvenPowers (r,((2 * (k + 1)) + 1))) . ((len <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*>) + x) = (OddEvenPowers (r,((2 * k) + 1))) . x

then A18: (OddEvenPowers (r,((2 * k) + 1))) . x = - (r |^ m) by A11, A12, Def3;
(OddEvenPowers (r,((2 * (k + 1)) + 1))) . (x + 2) = - (r |^ m2) by A13, A14, A17, Def3;
hence (OddEvenPowers (r,((2 * (k + 1)) + 1))) . ((len <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*>) + x) = (OddEvenPowers (r,((2 * k) + 1))) . x by A18, FINSEQ_1:44; :: thesis: verum

end;

end;

end;

hence OddEvenPowers (r,((2 * (k + 1)) + 1)) = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> ^ (OddEvenPowers (r,((2 * k) + 1))) by A4, A5, FINSEQ_1:def 7; :: thesis: verum