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

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

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

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

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;( 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

proof

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

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

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;

end;