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_{1}[ 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 ;

_{1}[k]
from NAT_1:sch 4(A2);

hence Im ((power F_Complex) . (x,k)) = 0 by A1; :: thesis: verum

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

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_{1}[n] ) holds

S_{1}[k]

for k being Nat holds SS

S

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume A3: for n being Nat st n < k holds

S_{1}[n]
; :: thesis: S_{1}[k]

_{1}[k]
; :: thesis: verum

end;S

assume A3: for n being Nat st n < k holds

S

now :: thesis: ( ( k = 0 & S_{1}[k] ) or ( k = 1 & S_{1}[k] ) or ( k >= 2 & S_{1}[k] ) )end;

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

end;

case A4:
k = 0
; :: thesis: S_{1}[k]

_{1}[k]
; :: thesis: verum

end;

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

hence
Sfor 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;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

case
k >= 2
; :: thesis: S_{1}[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 ) ;

_{1}[k]
; :: thesis: verum

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

hence
Sfor 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

.= (((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;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;A10: k = 2 * t by A7, ABIAN:def 2;

n = 2 * (t - 1) by A10;

hence n is even ; :: thesis: verum

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

A12: (power F_Complex) . (x,k1) =
((power F_Complex) . (x,n1)) * x
by A7, A6, GROUP_1:def 7
assume
n >= k
; :: thesis: contradiction

then (k - 2) - k >= k - k by XREAL_1:11;

hence contradiction ; :: thesis: verum

end;then (k - 2) - k >= k - k by XREAL_1:11;

hence contradiction ; :: thesis: verum

.= (((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

hence Im ((power F_Complex) . (x,k)) = 0 by A1; :: thesis: verum