let p be real Polynomial of F_Complex; :: thesis: for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0

let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Re (eval ((odd_part p),x)) = 0 )

defpred S_{1}[ 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

Re (eval ((odd_part p),x)) = 0 ;

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

consider n being Nat such that

A19: len p = n ;

thus ( Re x = 0 implies Re (eval ((odd_part p),x)) = 0 ) by A18, A19; :: thesis: verum

Re (eval ((odd_part p),x)) = 0

let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Re (eval ((odd_part p),x)) = 0 )

defpred S

for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0 ;

A1: now :: thesis: for k being Nat st ( for n being Nat st n < k holds

S_{1}[n] ) holds

S_{1}[k]

A18:
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 A2: for n being Nat st n < k holds

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

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

end;S

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

S

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

Re (eval ((odd_part p),x)) = 0

hence
Sfor x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_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

Re (eval ((odd_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

Re (eval ((odd_part p),x)) = 0

Re (eval ((odd_part p),x)) = 0 ; :: thesis: verum

end;Re (eval ((odd_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

Re (eval ((odd_part p),x)) = 0

now :: thesis: ( ( k = 0 & ( for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0 ) ) or ( k >= 1 & ( for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0 ) ) )end;

hence
for x being Element of F_Complex st Re x = 0 holds Re (eval ((odd_part p),x)) = 0 ) ) or ( k >= 1 & ( for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0 ) ) )

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

end;

case
k = 0
; :: thesis: for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0

Re (eval ((odd_part p),x)) = 0

then
p = 0_. F_Complex
by A3, POLYNOM4:5;

then A4: odd_part p = 0_. F_Complex by Th7;

thus for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0 :: thesis: verum

end;then A4: odd_part p = 0_. F_Complex by Th7;

thus for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0 :: thesis: verum

proof

let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Re (eval ((odd_part p),x)) = 0 )

assume Re x = 0 ; :: thesis: Re (eval ((odd_part p),x)) = 0

eval ((odd_part p),x) = 0. F_Complex by A4, POLYNOM4:17

.= 0 by COMPLFLD:def 1 ;

hence Re (eval ((odd_part p),x)) = 0 by COMPLEX1:4; :: thesis: verum

end;assume Re x = 0 ; :: thesis: Re (eval ((odd_part p),x)) = 0

eval ((odd_part p),x) = 0. F_Complex by A4, POLYNOM4:17

.= 0 by COMPLFLD:def 1 ;

hence Re (eval ((odd_part p),x)) = 0 by COMPLEX1:4; :: thesis: verum

case A5:
k >= 1
; :: thesis: for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0

Re (eval ((odd_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: odd_part p = (odd_part (Leading-Monomial p)) + (odd_part (p - (Leading-Monomial p))) by Th16;

thus for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0 :: thesis: verum

end;(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: odd_part p = (odd_part (Leading-Monomial p)) + (odd_part (p - (Leading-Monomial p))) by Th16;

thus for x being Element of F_Complex st Re x = 0 holds

Re (eval ((odd_part p),x)) = 0 :: thesis: verum

proof

let x be Element of F_Complex; :: thesis: ( Re x = 0 implies Re (eval ((odd_part p),x)) = 0 )

assume A7: Re x = 0 ; :: thesis: Re (eval ((odd_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 ;

A13: Re (eval ((odd_part (Leading-Monomial p)),x)) = 0

.= 0 + (Re (eval ((odd_part (p - (Leading-Monomial p))),x))) by A13, COMPLEX1:8

.= 0 by A12, A8, A9, A7, A3, A2 ; :: thesis: verum

end;assume A7: Re x = 0 ; :: thesis: Re (eval ((odd_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

then A12:
t is real
;let n be Nat; :: thesis: t . n is Real

A10: n in NAT by ORDINAL1:def 12;

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

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

A13: Re (eval ((odd_part (Leading-Monomial p)),x)) = 0

proof

end;

thus Re (eval ((odd_part p),x)) =
Re ((eval ((odd_part (Leading-Monomial p)),x)) + (eval ((odd_part (p - (Leading-Monomial p))),x)))
by A6, POLYNOM4:19
now :: thesis: ( ( deg p is even & Re (eval ((odd_part (Leading-Monomial p)),x)) = 0 ) or ( deg p is odd & Re (eval ((odd_part (Leading-Monomial p)),x)) = 0 ) )end;

hence
Re (eval ((odd_part (Leading-Monomial p)),x)) = 0
; :: thesis: verumper cases
( deg p is even or deg p is odd )
;

end;

case
deg p is even
; :: thesis: Re (eval ((odd_part (Leading-Monomial p)),x)) = 0

then
odd_part (Leading-Monomial p) = 0_. F_Complex
by Th19;

then eval ((odd_part (Leading-Monomial p)),x) = 0. F_Complex by POLYNOM4:17

.= 0 by COMPLFLD:def 1 ;

hence Re (eval ((odd_part (Leading-Monomial p)),x)) = 0 by COMPLEX1:4; :: thesis: verum

end;then eval ((odd_part (Leading-Monomial p)),x) = 0. F_Complex by POLYNOM4:17

.= 0 by COMPLFLD:def 1 ;

hence Re (eval ((odd_part (Leading-Monomial p)),x)) = 0 by COMPLEX1:4; :: thesis: verum

case A14:
deg p is odd
; :: thesis: Re (eval ((odd_part (Leading-Monomial p)),x)) = 0

then A15: eval ((odd_part (Leading-Monomial p)),x) =
eval ((Leading-Monomial p),x)
by Th20

.= (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: Re ((power F_Complex) . (x,((len p) -' 1))) = 0 by A7, A14, Th6;

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 Re (eval ((odd_part (Leading-Monomial p)),x)) = ((Re (p . ((len p) -' 1))) * (Re ((power F_Complex) . (x,((len p) -' 1))))) - ((Im (p . ((len p) -' 1))) * (Im ((power F_Complex) . (x,((len p) -' 1))))) by A15, COMPLEX1:9

.= 0 by A17, A16 ; :: thesis: verum

end;.= (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: Re ((power F_Complex) . (x,((len p) -' 1))) = 0 by A7, A14, Th6;

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 Re (eval ((odd_part (Leading-Monomial p)),x)) = ((Re (p . ((len p) -' 1))) * (Re ((power F_Complex) . (x,((len p) -' 1))))) - ((Im (p . ((len p) -' 1))) * (Im ((power F_Complex) . (x,((len p) -' 1))))) by A15, COMPLEX1:9

.= 0 by A17, A16 ; :: thesis: verum

.= 0 + (Re (eval ((odd_part (p - (Leading-Monomial p))),x))) by A13, COMPLEX1:8

.= 0 by A12, A8, A9, A7, A3, A2 ; :: thesis: verum

Re (eval ((odd_part p),x)) = 0 ; :: thesis: verum

consider n being Nat such that

A19: len p = n ;

thus ( Re x = 0 implies Re (eval ((odd_part p),x)) = 0 ) by A18, A19; :: thesis: verum