let k be even Element of NAT ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Im ((power F_Complex) . (x,k)) = 0
let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Im ((power F_Complex) . (x,k)) = 0 )
assume A1: Re x = 0 ; :: thesis: Im ((power F_Complex) . (x,k)) = 0
defpred S₁[ Nat] means for k1 being Element of NAT st k1 = $1 & k1 is even holds
for x being Element of F_Complex st Re x = 0 holds
Im ((power F_Complex) . (x,k1)) = 0 ;

A2: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A3: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]

now :: thesis: ( ( k = 0 & S₁[k] ) or ( k = 1 & S₁[k] ) or ( k >= 2 & S₁[k] ) )

per cases ( k = 0 or k = 1 or k >= 2 ) by NAT_1:23;

case A4: k = 0 ; :: thesis: S₁[k]

now :: thesis: for k1 being Element of NAT st k1 = k & k1 is even holds
for x being Element of F_Complex st Re x = 0 holds
Im ((power F_Complex) . (x,k1)) = 0

let k1 be Element of NAT ; :: thesis: ( k1 = k & k1 is even implies for x being Element of F_Complex st Re x = 0 holds
Im ((power F_Complex) . (x,k1)) = 0 )
assume A5: ( k1 = k & k1 is even ) ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Im ((power F_Complex) . (x,k1)) = 0
let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Im ((power F_Complex) . (x,k1)) = 0 )
assume Re x = 0 ; :: thesis: Im ((power F_Complex) . (x,k1)) = 0
(power F_Complex) . (x,0) = 1_ F_Complex by GROUP_1:def 7
.= 1r by COMPLFLD:def 1 ;
hence Im ((power F_Complex) . (x,k1)) = 0 by A4, A5, COMPLEX1:6; :: thesis: verum

end;

hence S₁[k] ; :: thesis: verum

end;

case k = 1 ; :: thesis: S₁[k]

hence S₁[k] by Lm1; :: thesis: verum

end;

case k >= 2 ; :: thesis: S₁[k]

then reconsider n = k - 2 as Element of NAT by INT_1:5;
reconsider n1 = n + 1 as Element of NAT ;
A6: ( n1 + 1 = k & n + 1 = n1 ) ;

now :: thesis: for k1 being Element of NAT st k1 = k & k1 is even holds
for x being Element of F_Complex st Re x = 0 holds
Im ((power F_Complex) . (x,k1)) = 0

let k1 be Element of NAT ; :: thesis: ( k1 = k & k1 is even implies for x being Element of F_Complex st Re x = 0 holds
Im ((power F_Complex) . (x,k1)) = 0 )
assume A7: ( k1 = k & k1 is even ) ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Im ((power F_Complex) . (x,k1)) = 0
let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Im ((power F_Complex) . (x,k1)) = 0 )
assume A8: Re x = 0 ; :: thesis: Im ((power F_Complex) . (x,k1)) = 0
A9: n is even

proof

consider t being Nat such that
A10: k = 2 * t by A7, ABIAN:def 2;
n = 2 * (t - 1) by A10;
hence n is even ; :: thesis: verum

end;

A11: now :: thesis: not n >= k

assume n >= k ; :: thesis: contradiction
then (k - 2) - k >= k - k by XREAL_1:11;
hence contradiction ; :: thesis: verum

end;

A12: (power F_Complex) . (x,k1) = ((power F_Complex) . (x,n1)) * x by A7, A6, GROUP_1:def 7
.= (((power F_Complex) . (x,n)) * x) * x by GROUP_1:def 7
.= ((power F_Complex) . (x,n)) * (x * x) ;
set z1 = (power F_Complex) . (x,n);
set z2 = x * x;
A13: Im (x * x) = ((Re x) * (Im x)) + ((Re x) * (Im x)) by COMPLEX1:9
.= 0 by A8 ;
A14: Im ((power F_Complex) . (x,n)) = 0 by A9, A11, A3, A8;
thus Im ((power F_Complex) . (x,k1)) = ((Re ((power F_Complex) . (x,n))) * (Im (x * x))) + ((Re (x * x)) * (Im ((power F_Complex) . (x,n)))) by A12, COMPLEX1:9
.= 0 by A13, A14 ; :: thesis: verum

end;

hence S₁[k] ; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(A2);
hence Im ((power F_Complex) . (x,k)) = 0 by A1; :: thesis: verum