let n be Nat; :: thesis: for im being imaginary Element of F_Complex
for r being real Element of F_Complex st n is even holds
( even_part (<%im,r%> `^ n) is real & odd_part (<%im,r%> `^ n) is imaginary )
let im be imaginary Element of F_Complex; :: thesis: for r being real Element of F_Complex st n is even holds
( even_part (<%im,r%> `^ n) is real & odd_part (<%im,r%> `^ n) is imaginary )
let r be real Element of F_Complex; :: thesis: ( n is even implies ( even_part (<%im,r%> `^ n) is real & odd_part (<%im,r%> `^ n) is imaginary ) )
assume A1: n is even ; :: thesis: ( even_part (<%im,r%> `^ n) is real & odd_part (<%im,r%> `^ n) is imaginary )
set pC = power F_Complex;
set IRn = <%im,r%> `^ n;
thus even_part (<%im,r%> `^ n) is real :: thesis: odd_part (<%im,r%> `^ n) is imaginary

proof

let k be Nat; :: according to HURWITZ2:def 8 :: thesis: (even_part (<%im,r%> `^ n)) . k is object

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

suppose k is odd ; :: thesis: (even_part (<%im,r%> `^ n)) . k is object

hence (even_part (<%im,r%> `^ n)) . k is object by HURWITZ2:def 1; :: thesis: verum

end;

suppose A2: k is even ; :: thesis: (even_part (<%im,r%> `^ n)) . k is object

A3: (<%im,r%> `^ n) . k = (n choose k) * ((r |^ k) * (im |^ (n -' k))) by Th13;
( n -' k = n - k or n -' k = 0 ) by XREAL_0:def 2;
hence (even_part (<%im,r%> `^ n)) . k is object by HURWITZ2:def 1, A3, A1, A2; :: thesis: verum

end;

end;

end;

thus odd_part (<%im,r%> `^ n) is imaginary :: thesis: verum

proof

let k be Nat; :: according to BASEL_2:def 4 :: thesis: (odd_part (<%im,r%> `^ n)) . k is imaginary

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

suppose k is even ; :: thesis: (odd_part (<%im,r%> `^ n)) . k is imaginary

hence (odd_part (<%im,r%> `^ n)) . k is imaginary by HURWITZ2:def 2; :: thesis: verum

end;

suppose A4: k is odd ; :: thesis: (odd_part (<%im,r%> `^ n)) . k is imaginary

A5: (<%im,r%> `^ n) . k = (n choose k) * ((r |^ k) * (im |^ (n -' k))) by Th13;

per cases ( k <= n or k > n ) ;

suppose k <= n ; :: thesis: (odd_part (<%im,r%> `^ n)) . k is imaginary

then n -' k = n - k by XREAL_1:233;
hence (odd_part (<%im,r%> `^ n)) . k is imaginary by HURWITZ2:def 2, A5, A1, A4; :: thesis: verum

end;

suppose k > n ; :: thesis: (odd_part (<%im,r%> `^ n)) . k is imaginary

then n choose k = 0 by NEWTON:def 3;
hence (odd_part (<%im,r%> `^ n)) . k is imaginary by A4, A5, HURWITZ2:def 2; :: thesis: verum

end;

end;

end;

end;

end;