let k be odd Element of NAT ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Re ((power F_Complex) . (x,k)) = 0
let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Re ((power F_Complex) . (x,k)) = 0 )
assume A1: Re x = 0 ; :: thesis: Re ((power F_Complex) . (x,k)) = 0
defpred S₁[ Nat] means for k1 being Element of NAT st k1 = $1 & k1 is odd holds
for x being Element of F_Complex st Re x = 0 holds
Re ((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 = 1 & S₁[k] ) or ( k = 0 & S₁[k] ) or ( k >= 2 & S₁[k] ) )

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

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

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

let k1 be Element of NAT ; :: thesis: ( k1 = k & k1 is odd implies for x being Element of F_Complex st Re x = 0 holds
Re ((power F_Complex) . (x,k1)) = 0 )
assume A5: ( k1 = k & k1 is odd ) ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Re ((power F_Complex) . (x,k1)) = 0
let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Re ((power F_Complex) . (x,k1)) = 0 )
assume A6: Re x = 0 ; :: thesis: Re ((power F_Complex) . (x,k1)) = 0
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;
1 = 0 + 1 ;
then (power F_Complex) . (x,1) = ((power F_Complex) . (x,z)) * x by GROUP_1:def 7
.= (1_ F_Complex) * x by GROUP_1:def 7
.= x ;
hence Re ((power F_Complex) . (x,k1)) = 0 by A6, A5, A4; :: thesis: verum

end;

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

end;

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

hence S₁[k] ; :: 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 ;
A7: ( n1 + 1 = k & n + 1 = n1 ) ;

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

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

proof

consider t being Integer such that
A11: k = (2 * t) + 1 by A8, ABIAN:1;
n = (2 * (t - 1)) + 1 by A11;
hence n is odd ; :: thesis: verum

end;

A12: 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;

A13: (power F_Complex) . (x,k1) = ((power F_Complex) . (x,n1)) * x by A8, A7, 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;
A14: Im (x * x) = ((Re x) * (Im x)) + ((Re x) * (Im x)) by COMPLEX1:9
.= 0 by A9 ;
A15: Re ((power F_Complex) . (x,n)) = 0 by A10, A12, A3, A9;
thus Re ((power F_Complex) . (x,k1)) = ((Re ((power F_Complex) . (x,n))) * (Re (x * x))) - ((Im ((power F_Complex) . (x,n))) * (Im (x * x))) by A13, COMPLEX1:9
.= 0 by A14, A15 ; :: 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 Re ((power F_Complex) . (x,k)) = 0 by A1; :: thesis: verum