let n be Nat; 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; 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; ( n is even implies ( even_part (<%im,r%> `^ n) is real & odd_part (<%im,r%> `^ n) is imaginary ) )
assume A1:
n is even
; ( 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
odd_part (<%im,r%> `^ n) is imaginary
thus
odd_part (<%im,r%> `^ n) is imaginary
verum