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

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

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

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

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_{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 = 1 & S_{1}[k] ) or ( k = 0 & S_{1}[k] ) or ( k >= 2 & S_{1}[k] ) )end;

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

end;

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

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

end;

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

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

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 ;

A7: ( n1 + 1 = k & n + 1 = n1 ) ;

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

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

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

.= (((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;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;A11: k = (2 * t) + 1 by A8, ABIAN:1;

n = (2 * (t - 1)) + 1 by A11;

hence n is odd ; :: thesis: verum

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

A13: (power F_Complex) . (x,k1) =
((power F_Complex) . (x,n1)) * x
by A8, A7, 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;

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

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