let p be real Polynomial of F_Complex; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0
let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Im (eval ((even_part p),x)) = 0 )
defpred S₁[ Nat] means for p being Polynomial of F_Complex st p is real & len p = $1 holds
for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0 ;

A1: 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 A2: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]

now :: thesis: for p being Polynomial of F_Complex st p is real & len p = k holds
for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0

let p be Polynomial of F_Complex; :: thesis: ( p is real & len p = k implies for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0 )
assume A3: ( p is real & len p = k ) ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0

now :: thesis: ( ( k = 0 & ( for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0 ) ) or ( k >= 1 & ( for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0 ) ) )

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

case k = 0 ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0

then p = 0_. F_Complex by A3, POLYNOM4:5;
then A4: even_part p = 0_. F_Complex by Th7;
thus for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0 :: thesis: verum

proof

let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Im (eval ((even_part p),x)) = 0 )
assume Re x = 0 ; :: thesis: Im (eval ((even_part p),x)) = 0
eval ((even_part p),x) = 0. F_Complex by A4, POLYNOM4:17
.= 0 by COMPLFLD:def 1 ;
hence Im (eval ((even_part p),x)) = 0 by COMPLEX1:4; :: thesis: verum

end;

end;

case A5: k >= 1 ; :: thesis: for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0

set LMp = Leading-Monomial p;
(Leading-Monomial p) + (p - (Leading-Monomial p)) = ((Leading-Monomial p) + (- (Leading-Monomial p))) + p by POLYNOM3:26
.= ((Leading-Monomial p) - (Leading-Monomial p)) + p
.= (0_. F_Complex) + p by POLYNOM3:29
.= p by POLYNOM3:28 ;
then A6: even_part p = (even_part (Leading-Monomial p)) + (even_part (p - (Leading-Monomial p))) by Th15;
thus for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0 :: thesis: verum

proof

let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Im (eval ((even_part p),x)) = 0 )
assume A7: Re x = 0 ; :: thesis: Im (eval ((even_part p),x)) = 0
consider t being Polynomial of F_Complex such that
A8: ( len t < len p & p = t + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
t . n = p . n ) ) by A5, A3, POLYNOM4:16;
A9: p - (Leading-Monomial p) = t + ((Leading-Monomial p) - (Leading-Monomial p)) by A8, POLYNOM3:26
.= t + (0_. F_Complex) by POLYNOM3:29
.= t by POLYNOM3:28 ;

now :: thesis: for n being Nat holds t . n is Real

let n be Nat; :: thesis: t . n is Real
A10: n in NAT by ORDINAL1:def 12;

now :: thesis: ( ( n < (len p) - 1 & t . n is Real ) or ( n >= (len p) - 1 & t . n is Real ) )

per cases ( n < (len p) - 1 or n >= (len p) - 1 ) ;

case n < (len p) - 1 ; :: thesis: t . n is Real

then t . n = p . n by A8, A10;
hence t . n is Real by A3; :: thesis: verum

end;

case A11: n >= (len p) - 1 ; :: thesis: t . n is Real

reconsider lp = (len p) - 1 as Element of NAT by A5, A3, INT_1:5;
len t < lp + 1 by A8;
then lp >= len t by NAT_1:13;
then t . n = 0. F_Complex by ALGSEQ_1:8, A11, XXREAL_0:2;
hence t . n is Real by COMPLFLD:def 1; :: thesis: verum

end;

end;

end;

hence t . n is Real ; :: thesis: verum

end;

then A12: t is real ;
A13: Im (eval ((even_part (Leading-Monomial p)),x)) = 0

proof

now :: thesis: ( ( deg p is odd & Im (eval ((even_part (Leading-Monomial p)),x)) = 0 ) or ( deg p is even & Im (eval ((even_part (Leading-Monomial p)),x)) = 0 ) )

per cases ( deg p is odd or deg p is even ) ;

case deg p is odd ; :: thesis: Im (eval ((even_part (Leading-Monomial p)),x)) = 0

then even_part (Leading-Monomial p) = 0_. F_Complex by Th18;
then eval ((even_part (Leading-Monomial p)),x) = 0. F_Complex by POLYNOM4:17
.= 0 by COMPLFLD:def 1 ;
hence Im (eval ((even_part (Leading-Monomial p)),x)) = 0 by COMPLEX1:4; :: thesis: verum

end;

case A14: deg p is even ; :: thesis: Im (eval ((even_part (Leading-Monomial p)),x)) = 0

then A15: eval ((even_part (Leading-Monomial p)),x) = eval ((Leading-Monomial p),x) by Th17
.= (p . ((len p) -' 1)) * ((power F_Complex) . (x,((len p) -' 1))) by POLYNOM4:22 ;
set z1 = p . ((len p) -' 1);
set z2 = (power F_Complex) . (x,((len p) -' 1));
(len p) -' 1 = deg p by A3, A5, XREAL_1:233;
then A16: Im ((power F_Complex) . (x,((len p) -' 1))) = 0 by A7, A14, Th5;
p . ((len p) -' 1) in REAL by A3, XREAL_0:def 1;
then A17: Im (p . ((len p) -' 1)) = 0 by COMPLEX1:def 2;
thus Im (eval ((even_part (Leading-Monomial p)),x)) = ((Re (p . ((len p) -' 1))) * (Im ((power F_Complex) . (x,((len p) -' 1))))) + ((Re ((power F_Complex) . (x,((len p) -' 1)))) * (Im (p . ((len p) -' 1)))) by A15, COMPLEX1:9
.= 0 by A16, A17 ; :: thesis: verum

end;

end;

end;

hence Im (eval ((even_part (Leading-Monomial p)),x)) = 0 ; :: thesis: verum

end;

thus Im (eval ((even_part p),x)) = Im ((eval ((even_part (Leading-Monomial p)),x)) + (eval ((even_part (p - (Leading-Monomial p))),x))) by A6, POLYNOM4:19
.= 0 + (Im (eval ((even_part (p - (Leading-Monomial p))),x))) by A13, COMPLEX1:8
.= 0 by A12, A8, A9, A7, A3, A2 ; :: thesis: verum

end;

end;

end;

end;

hence for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0 ; :: thesis: verum

end;

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

end;

A18: for k being Nat holds S₁[k] from NAT_1:sch 4(A1);
consider n being Nat such that
A19: len p = n ;
thus ( Re x = 0 implies Im (eval ((even_part p),x)) = 0 ) by A18, A19; :: thesis: verum