let n be Nat; :: thesis: for im being imaginary Element of F_Complex
for r being real Element of F_Complex st n is odd holds
( even_part (<%im,r%> `^ n) is imaginary & odd_part (<%im,r%> `^ n) is real )
let im be imaginary Element of F_Complex; :: thesis: for r being real Element of F_Complex st n is odd holds
( even_part (<%im,r%> `^ n) is imaginary & odd_part (<%im,r%> `^ n) is real )
let r be real Element of F_Complex; :: thesis: ( n is odd implies ( even_part (<%im,r%> `^ n) is imaginary & odd_part (<%im,r%> `^ n) is real ) )
assume A1: n is odd ; :: thesis: ( even_part (<%im,r%> `^ n) is imaginary & odd_part (<%im,r%> `^ n) is real )
set pC = power F_Complex;
set IRn = <%im,r%> `^ n;
thus even_part (<%im,r%> `^ n) is imaginary :: thesis: odd_part (<%im,r%> `^ n) is real
proof
let k be Nat; :: according to BASEL_2:def 4 :: thesis: (even_part (<%im,r%> `^ n)) . k is imaginary
per cases ( k is odd or k is even ) ;
suppose A2: k is even ; :: thesis: (even_part (<%im,r%> `^ n)) . k is imaginary
A3: (<%im,r%> `^ n) . k = (n choose k) * ((r |^ k) * (im |^ (n -' k))) by Th13;
end;
end;
end;
thus odd_part (<%im,r%> `^ n) is real :: thesis: verum
proof
let k be Nat; :: according to HURWITZ2:def 8 :: thesis: (odd_part (<%im,r%> `^ n)) . k is object
per cases ( k is even or k is odd ) ;
suppose A4: k is odd ; :: thesis: (odd_part (<%im,r%> `^ n)) . k is object
A5: (<%im,r%> `^ n) . k = (n choose k) * ((r |^ k) * (im |^ (n -' k))) by Th13;
end;
end;
end;