let p be real Polynomial of F_Complex; 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; ( Re x = 0 implies Im (eval ((even_part p),x)) = 0 )
defpred S1[ 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 for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )assume A2:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[k]now 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;
( 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 )
;
for x being Element of F_Complex st Re x = 0 holds
Im (eval ((even_part p),x)) = 0 now ( ( 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 A5:
k >= 1
;
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
verumproof
let x be
Element of
F_Complex;
( Re x = 0 implies Im (eval ((even_part p),x)) = 0 )
assume A7:
Re x = 0
;
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
;
then A12:
t is
real
;
A13:
Im (eval ((even_part (Leading-Monomial p)),x)) = 0
proof
now ( ( 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 A14:
deg p is
even
;
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
;
verum end; end; end;
hence
Im (eval ((even_part (Leading-Monomial p)),x)) = 0
;
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
;
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
;
verum end; hence
S1[
k]
;
verum end;
A18:
for k being Nat holds S1[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; verum