let p be non constant real with_positive_coefficients Polynomial of F_Complex; :: thesis: ( [(even_part p),(odd_part p)] is positive & even_part p, odd_part p have_no_common_roots implies ( ( for x being Element of F_Complex st Re x = 0 & eval ((odd_part p),x) <> 0 holds
Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ) & (even_part p) + (odd_part p) is Hurwitz ) )
assume A1: ( [(even_part p),(odd_part p)] is positive & even_part p, odd_part p have_no_common_roots ) ; :: thesis: ( ( for x being Element of F_Complex st Re x = 0 & eval ((odd_part p),x) <> 0 holds
Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ) & (even_part p) + (odd_part p) is Hurwitz )
set p1 = even_part p;
set p2 = odd_part p;
set z = [(even_part p),(odd_part p)];

per cases ( (even_part p) - (odd_part p) = 0_. F_Complex or (even_part p) - (odd_part p) <> 0_. F_Complex ) ;

suppose (even_part p) - (odd_part p) = 0_. F_Complex ; :: thesis: ( ( for x being Element of F_Complex st Re x = 0 & eval ((odd_part p),x) <> 0 holds
Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ) & (even_part p) + (odd_part p) is Hurwitz )

then (even_part p) + ((odd_part p) + (- (odd_part p))) = (0_. F_Complex) + (odd_part p) by POLYNOM3:26;
then (even_part p) + ((odd_part p) - (odd_part p)) = (0_. F_Complex) + (odd_part p) ;
then (even_part p) + (0_. F_Complex) = (0_. F_Complex) + (odd_part p) by POLYNOM3:29;
then A2: even_part p = (0_. F_Complex) + (odd_part p) by POLYNOM3:28;
A3: for x being Element of F_Complex holds eval ((odd_part p),x) <> 0. F_Complex

proof

let x be Element of F_Complex; :: thesis: eval ((odd_part p),x) <> 0. F_Complex
assume eval ((odd_part p),x) = 0. F_Complex ; :: thesis: contradiction
then x is_a_root_of odd_part p by POLYNOM5:def 7;
then x is_a_common_root_of even_part p, odd_part p by A2, POLYNOM3:28;
hence contradiction by A1; :: thesis: verum

end;

A4: for x being Element of F_Complex holds eval ([(even_part p),(odd_part p)],x) = 1. F_Complex

proof

let x be Element of F_Complex; :: thesis: eval ([(even_part p),(odd_part p)],x) = 1. F_Complex
A5: eval ((odd_part p),x) <> 0. F_Complex by A3;
thus eval ([(even_part p),(odd_part p)],x) = (eval ((odd_part p),x)) * ((eval ((odd_part p),x)) ") by A2, POLYNOM3:28
.= 1. F_Complex by A5, VECTSP_1:def 10 ; :: thesis: verum

end;

A6: Re (1. F_Complex) = 1 by COMPLFLD:def 1, COMPLEX1:6;

now :: thesis: for x being Element of F_Complex st x is_a_root_of (even_part p) + (odd_part p) holds
Re x < 0

let x be Element of F_Complex; :: thesis: ( x is_a_root_of (even_part p) + (odd_part p) implies Re x < 0 )
assume x is_a_root_of (even_part p) + (odd_part p) ; :: thesis: Re x < 0
then 0. F_Complex = eval (((even_part p) + (odd_part p)),x) by POLYNOM5:def 7
.= (eval ((even_part p),x)) + (eval ((odd_part p),x)) by POLYNOM4:19
.= (eval ((odd_part p),x)) + (eval ((odd_part p),x)) by A2, POLYNOM3:28 ;
then 2 * (eval ((odd_part p),x)) = 0 by COMPLFLD:def 1;
then 0. F_Complex = eval ((odd_part p),x) by COMPLFLD:def 1;
hence Re x < 0 by A3; :: thesis: verum

end;

hence ( ( for x being Element of F_Complex st Re x = 0 & eval ((odd_part p),x) <> 0 holds
Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ) & (even_part p) + (odd_part p) is Hurwitz ) by A4, A6; :: thesis: verum

end;

suppose (even_part p) - (odd_part p) <> 0_. F_Complex ; :: thesis: ( ( for x being Element of F_Complex st Re x = 0 & eval ((odd_part p),x) <> 0 holds
Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ) & (even_part p) + (odd_part p) is Hurwitz )

then reconsider pp = (even_part p) - (odd_part p) as non zero Polynomial of F_Complex by UPROOTS:def 5;
set w = [((even_part p) + (odd_part p)),pp];

A7: now :: thesis: for x being Element of F_Complex st eval (([(even_part p),(odd_part p)] `2),x) = 0. F_Complex holds
eval ([((even_part p) + (odd_part p)),pp],x) = 1. F_Complex

let x be Element of F_Complex; :: thesis: ( eval (([(even_part p),(odd_part p)] `2),x) = 0. F_Complex implies eval ([((even_part p) + (odd_part p)),pp],x) = 1. F_Complex )
assume A8: eval (([(even_part p),(odd_part p)] `2),x) = 0. F_Complex ; :: thesis: eval ([((even_part p) + (odd_part p)),pp],x) = 1. F_Complex
A9: eval (pp,x) = (eval ((even_part p),x)) - (eval ((odd_part p),x)) by POLYNOM4:21
.= eval ((even_part p),x) by RLVECT_1:13, A8 ;
A10: eval (((even_part p) + (odd_part p)),x) = (eval ((even_part p),x)) + (eval ((odd_part p),x)) by POLYNOM4:19
.= eval ((even_part p),x) by RLVECT_1:def 4, A8 ;

A11: now :: thesis: not eval ((even_part p),x) = 0. F_Complex

assume eval ((even_part p),x) = 0. F_Complex ; :: thesis: contradiction
then x is_a_common_root_of even_part p, odd_part p by A8, POLYNOM5:def 7;
hence contradiction by A1; :: thesis: verum

end;

thus eval ([((even_part p) + (odd_part p)),pp],x) = ((eval ((even_part p),x)) ") * (eval ((even_part p),x)) by A10, A9
.= 1. F_Complex by VECTSP_1:def 10, A11 ; :: thesis: verum

end;

A12: now :: thesis: for x being Element of F_Complex st eval ([((even_part p) + (odd_part p)),pp],x) = 1. F_Complex & eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) holds
eval (([(even_part p),(odd_part p)] `2),x) = 0. F_Complex

let x be Element of F_Complex; :: thesis: ( eval ([((even_part p) + (odd_part p)),pp],x) = 1. F_Complex & eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) implies eval (([(even_part p),(odd_part p)] `2),x) = 0. F_Complex )
assume A13: ( eval ([((even_part p) + (odd_part p)),pp],x) = 1. F_Complex & eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) ) ; :: thesis: eval (([(even_part p),(odd_part p)] `2),x) = 0. F_Complex

A14: now :: thesis: not eval (pp,x) = 0. F_Complex

assume eval (pp,x) = 0. F_Complex ; :: thesis: contradiction
then (eval ((even_part p),x)) - (eval ((odd_part p),x)) = 0. F_Complex by POLYNOM4:21;
then eval ((odd_part p),x) = ((eval ((even_part p),x)) - (eval ((odd_part p),x))) + (eval ((odd_part p),x)) by RLVECT_1:def 4
.= (eval ((even_part p),x)) + ((- (eval ((odd_part p),x))) + (eval ((odd_part p),x)))
.= (eval ((even_part p),x)) + (0. F_Complex) by RLVECT_1:5
.= eval ((even_part p),x) by RLVECT_1:def 4 ;
hence contradiction by A13; :: thesis: verum

end;

reconsider a = eval ((odd_part p),x) as Complex ;
(1. F_Complex) * (eval (pp,x)) = (eval (((even_part p) + (odd_part p)),x)) * (((eval (pp,x)) ") * (eval (pp,x))) by A13
.= (eval (((even_part p) + (odd_part p)),x)) * (1. F_Complex) by A14, VECTSP_1:def 10
.= eval (((even_part p) + (odd_part p)),x) ;
then eval (((even_part p) + (odd_part p)),x) = eval (pp,x)
.= (eval ((even_part p),x)) - (eval ((odd_part p),x)) by POLYNOM4:21 ;
then (eval ((even_part p),x)) + (eval ((odd_part p),x)) = (eval ((even_part p),x)) - (eval ((odd_part p),x)) by POLYNOM4:19;
then a = - a by COMPLFLD:2;
hence eval (([(even_part p),(odd_part p)] `2),x) = 0. F_Complex by COMPLFLD:def 1; :: thesis: verum

end;

A15: now :: thesis: for x being Element of F_Complex st eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) holds
(1 + (eval ([((even_part p) + (odd_part p)),pp],x))) / ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) = eval ([(even_part p),(odd_part p)],x)

let x be Element of F_Complex; :: thesis: ( eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) implies (1 + (eval ([((even_part p) + (odd_part p)),pp],x))) / ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) = eval ([(even_part p),(odd_part p)],x) )
assume A16: ( eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) ) ; :: thesis: (1 + (eval ([((even_part p) + (odd_part p)),pp],x))) / ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) = eval ([(even_part p),(odd_part p)],x)
(eval ([((even_part p) + (odd_part p)),pp],x)) - (1. F_Complex) <> (1. F_Complex) - (1. F_Complex) by A16, A12;
then A17: (eval ([((even_part p) + (odd_part p)),pp],x)) - (1. F_Complex) <> 0. F_Complex by RLVECT_1:15;
A18: 1 = 1. F_Complex by COMPLFLD:def 1, COMPLEX1:def 4;
then A19: (eval ([((even_part p) + (odd_part p)),pp],x)) - 1 = (eval ([((even_part p) + (odd_part p)),pp],x)) - (1. F_Complex) by COMPLFLD:3;
A20: eval (((even_part p) - (odd_part p)),x) = (eval ((even_part p),x)) - (eval ((odd_part p),x)) by POLYNOM4:21;

A21: now :: thesis: not eval (((even_part p) - (odd_part p)),x) = 0. F_Complex

assume eval (((even_part p) - (odd_part p)),x) = 0. F_Complex ; :: thesis: contradiction
then (eval ((even_part p),x)) - (eval ((odd_part p),x)) = 0. F_Complex by POLYNOM4:21;
hence contradiction by A16, RLVECT_1:21; :: thesis: verum

end;

A22: (eval (((even_part p) - (odd_part p)),x)) + (eval (((even_part p) + (odd_part p)),x)) = ((eval ((even_part p),x)) - (eval ((odd_part p),x))) + ((eval ((even_part p),x)) + (eval ((odd_part p),x))) by A20, POLYNOM4:19
.= ((eval ((odd_part p),x)) - (eval ((odd_part p),x))) + ((eval ((even_part p),x)) + (eval ((even_part p),x)))
.= (0. F_Complex) + ((eval ((even_part p),x)) + (eval ((even_part p),x))) by RLVECT_1:def 10
.= (eval ((even_part p),x)) + (eval ((even_part p),x)) by RLVECT_1:def 4 ;
A23: ((eval (((even_part p) + (odd_part p)),x)) * ((eval (((even_part p) - (odd_part p)),x)) ")) - ((eval (((even_part p) - (odd_part p)),x)) * ((eval (((even_part p) - (odd_part p)),x)) ")) = ((eval (((even_part p) + (odd_part p)),x)) * ((eval (((even_part p) - (odd_part p)),x)) ")) + ((- (eval (((even_part p) - (odd_part p)),x))) * ((eval (((even_part p) - (odd_part p)),x)) ")) by VECTSP_1:8
.= ((eval (((even_part p) + (odd_part p)),x)) + (- (eval (((even_part p) - (odd_part p)),x)))) * ((eval (((even_part p) - (odd_part p)),x)) ")
.= (((eval ((even_part p),x)) + (eval ((odd_part p),x))) - (eval (((even_part p) - (odd_part p)),x))) * ((eval (((even_part p) - (odd_part p)),x)) ") by POLYNOM4:19
.= (((eval ((even_part p),x)) + (eval ((odd_part p),x))) - ((eval ((even_part p),x)) - (eval ((odd_part p),x)))) * ((eval (((even_part p) - (odd_part p)),x)) ") by POLYNOM4:21
.= (((eval ((even_part p),x)) + (eval ((odd_part p),x))) + ((eval ((odd_part p),x)) + (- (eval ((even_part p),x))))) * ((eval (((even_part p) - (odd_part p)),x)) ") by RLVECT_1:33
.= ((((eval ((even_part p),x)) + (- (eval ((even_part p),x)))) + (eval ((odd_part p),x))) + (eval ((odd_part p),x))) * ((eval (((even_part p) - (odd_part p)),x)) ")
.= (((0. F_Complex) + (eval ((odd_part p),x))) + (eval ((odd_part p),x))) * ((eval (((even_part p) - (odd_part p)),x)) ") by RLVECT_1:def 10
.= ((eval ((odd_part p),x)) + (eval ((odd_part p),x))) * ((eval (((even_part p) - (odd_part p)),x)) ") by ALGSTR_1:def 2
.= (eval (((odd_part p) + (odd_part p)),x)) * ((eval (((even_part p) - (odd_part p)),x)) ") by POLYNOM4:19 ;
A24: (eval ([(even_part p),(odd_part p)],x)) * ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) = ((eval ((even_part p),x)) * ((eval ((odd_part p),x)) ")) * ((eval ([((even_part p) + (odd_part p)),pp],x)) - (1. F_Complex)) by COMPLEX1:def 4, COMPLFLD:8, COMPLFLD:3
.= ((eval ((even_part p),x)) * ((eval ((odd_part p),x)) ")) * ((eval ([((even_part p) + (odd_part p)),pp],x)) - ((eval (((even_part p) - (odd_part p)),x)) * ((eval (((even_part p) - (odd_part p)),x)) "))) by A21, VECTSP_1:def 10
.= ((eval ((even_part p),x)) * ((eval ((odd_part p),x)) ")) * (((eval ((odd_part p),x)) + (eval ((odd_part p),x))) * ((eval (((even_part p) - (odd_part p)),x)) ")) by A23, POLYNOM4:19
.= (((eval ((even_part p),x)) * 2) * (((eval ((odd_part p),x)) ") * (eval ((odd_part p),x)))) * ((eval (((even_part p) - (odd_part p)),x)) ")
.= (((eval ((even_part p),x)) * 2) * (1. F_Complex)) * ((eval (((even_part p) - (odd_part p)),x)) ") by A16, VECTSP_1:def 10
.= (2 * (eval ((even_part p),x))) * ((eval (((even_part p) - (odd_part p)),x)) ") by A18 ;
1 + (eval ([((even_part p) + (odd_part p)),pp],x)) = ((eval (((even_part p) - (odd_part p)),x)) * ((eval (((even_part p) - (odd_part p)),x)) ")) + ((eval (((even_part p) + (odd_part p)),x)) * ((eval (((even_part p) - (odd_part p)),x)) ")) by A18, A21, VECTSP_1:def 10
.= ((eval ((even_part p),x)) + (eval ((even_part p),x))) * ((eval (((even_part p) - (odd_part p)),x)) ") by A22 ;
then (1 + (eval ([((even_part p) + (odd_part p)),pp],x))) * (((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) ") = ((eval ([(even_part p),(odd_part p)],x)) * ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1)) * (((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) ") by A24
.= (eval ([(even_part p),(odd_part p)],x)) * (((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) * (((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) "))
.= (eval ([(even_part p),(odd_part p)],x)) * (((eval ([((even_part p) + (odd_part p)),pp],x)) - (1. F_Complex)) * (((eval ([((even_part p) + (odd_part p)),pp],x)) - (1. F_Complex)) ")) by A19, A17, COMPLFLD:5
.= (eval ([(even_part p),(odd_part p)],x)) * (1. F_Complex) by A17, VECTSP_1:def 10
.= eval ([(even_part p),(odd_part p)],x) ;
hence (1 + (eval ([((even_part p) + (odd_part p)),pp],x))) / ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) = eval ([(even_part p),(odd_part p)],x) ; :: thesis: verum

end;

A25: now :: thesis: for x being Real st 0 <= x & x * x = 1 holds
x = 1

let x be Real; :: thesis: ( 0 <= x & x * x = 1 implies x = 1 )
assume ( 0 <= x & x * x = 1 ) ; :: thesis: x = 1
then ( 0 < x & x = x " ) by XCMPLX_1:210;
hence x = 1 by XCMPLX_1:223; :: thesis: verum

end;

A26: for x being Element of F_Complex
for E2, E1 being Real st E2 = |.(eval ([((even_part p) + (odd_part p)),pp],x)).| ^2 & E1 = |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 & eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) holds
Re (eval ([(even_part p),(odd_part p)],x)) = (E2 - 1) / E1

proof

let x be Element of F_Complex; :: thesis: for E2, E1 being Real st E2 = |.(eval ([((even_part p) + (odd_part p)),pp],x)).| ^2 & E1 = |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 & eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) holds
Re (eval ([(even_part p),(odd_part p)],x)) = (E2 - 1) / E1
let E2, E1 be Real; :: thesis: ( E2 = |.(eval ([((even_part p) + (odd_part p)),pp],x)).| ^2 & E1 = |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 & eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) implies Re (eval ([(even_part p),(odd_part p)],x)) = (E2 - 1) / E1 )
assume A27: ( E2 = |.(eval ([((even_part p) + (odd_part p)),pp],x)).| ^2 & E1 = |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 ) ; :: thesis: ( not eval ((odd_part p),x) <> 0. F_Complex or not eval ((odd_part p),x) <> eval ((even_part p),x) or Re (eval ([(even_part p),(odd_part p)],x)) = (E2 - 1) / E1 )
assume A28: ( eval ((odd_part p),x) <> 0. F_Complex & eval ((odd_part p),x) <> eval ((even_part p),x) ) ; :: thesis: Re (eval ([(even_part p),(odd_part p)],x)) = (E2 - 1) / E1
set z1 = 1 + (eval ([((even_part p) + (odd_part p)),pp],x));
set z2 = (eval ([((even_part p) + (odd_part p)),pp],x)) - 1;
A29: Re (1 + (eval ([((even_part p) + (odd_part p)),pp],x))) = (Re (eval ([((even_part p) + (odd_part p)),pp],x))) + 1 by COMPLEX1:8, COMPLEX1:6, COMPLEX1:def 4;
A30: Re ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) = (Re (eval ([((even_part p) + (odd_part p)),pp],x))) - 1 by COMPLEX1:def 4, COMPLEX1:6, COMPLEX1:19;
A31: Im (1 + (eval ([((even_part p) + (odd_part p)),pp],x))) = 0 + (Im (eval ([((even_part p) + (odd_part p)),pp],x))) by COMPLEX1:8, COMPLEX1:6, COMPLEX1:def 4;
A32: Im ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) = (Im (eval ([((even_part p) + (odd_part p)),pp],x))) - (Im 1r) by COMPLEX1:19, COMPLEX1:def 4
.= (Im (eval ([((even_part p) + (odd_part p)),pp],x))) + 0 by COMPLEX1:6 ;
reconsider R2 = (Re ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1)) ^2 , I2 = (Im ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1)) ^2 as Real ;
reconsider RR = (Re (eval ([((even_part p) + (odd_part p)),pp],x))) ^2 , II = (Im (eval ([((even_part p) + (odd_part p)),pp],x))) ^2 as Real ;
Re ((1 + (eval ([((even_part p) + (odd_part p)),pp],x))) / ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1)) = (((Re (1 + (eval ([((even_part p) + (odd_part p)),pp],x)))) * (Re ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1))) + ((Im (1 + (eval ([((even_part p) + (odd_part p)),pp],x)))) * (Im ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1)))) / (R2 + I2) by COMPLEX1:24
.= ((RR + II) - 1) / (R2 + I2) by A29, A30, A31, A32
.= (|.((eval ([((even_part p) + (odd_part p)),pp],x)) * (eval ([((even_part p) + (odd_part p)),pp],x))).| - 1) / (R2 + I2) by COMPLEX1:68
.= ((|.(eval ([((even_part p) + (odd_part p)),pp],x)).| * |.(eval ([((even_part p) + (odd_part p)),pp],x)).|) - 1) / (R2 + I2) by COMPLEX1:65
.= (E2 - 1) / |.(((eval ([((even_part p) + (odd_part p)),pp],x)) - 1) * ((eval ([((even_part p) + (odd_part p)),pp],x)) - 1)).| by COMPLEX1:68, A27
.= (E2 - 1) / E1 by COMPLEX1:65, A27 ;
hence Re (eval ([(even_part p),(odd_part p)],x)) = (E2 - 1) / E1 by A28, A15; :: thesis: verum

end;

A33: for x being Element of F_Complex st eval ((odd_part p),x) <> eval ((even_part p),x) & Re (eval ([(even_part p),(odd_part p)],x)) >= 0 holds
|.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1

proof

let x be Element of F_Complex; :: thesis: ( eval ((odd_part p),x) <> eval ((even_part p),x) & Re (eval ([(even_part p),(odd_part p)],x)) >= 0 implies |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 )
reconsider E2 = |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 as Real ;
reconsider E1 = |.(eval ([((even_part p) + (odd_part p)),pp],x)).| ^2 as Real ;
assume A34: ( eval ((odd_part p),x) <> eval ((even_part p),x) & Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ) ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1
A35: E2 >= 0 by XREAL_1:63;

now :: thesis: ( ( eval ((odd_part p),x) = 0. F_Complex & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 ) or ( Re (eval ([(even_part p),(odd_part p)],x)) > 0 & eval ((odd_part p),x) <> 0. F_Complex & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 ) or ( Re (eval ([(even_part p),(odd_part p)],x)) = 0 & eval ((odd_part p),x) <> 0. F_Complex & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 ) )

per cases ( eval ((odd_part p),x) = 0. F_Complex or ( Re (eval ([(even_part p),(odd_part p)],x)) > 0 & eval ((odd_part p),x) <> 0. F_Complex ) or ( Re (eval ([(even_part p),(odd_part p)],x)) = 0 & eval ((odd_part p),x) <> 0. F_Complex ) ) by A34;

case eval ((odd_part p),x) = 0. F_Complex ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1

then eval ([((even_part p) + (odd_part p)),pp],x) = 1. F_Complex by A7
.= 1 by COMPLFLD:def 1, COMPLEX1:def 4 ;
hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 by COMPLEX1:48; :: thesis: verum

end;

case ( Re (eval ([(even_part p),(odd_part p)],x)) > 0 & eval ((odd_part p),x) <> 0. F_Complex ) ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1

then A36: (E1 - 1) / E2 > 0 by A34, A26;
then E1 - 1 > 0 by A35;
then A37: (E1 - 1) + 1 > 0 + 1 by XREAL_1:8;

now :: thesis: ( ( eval ([((even_part p) + (odd_part p)),pp],x) = 0 & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 ) or ( eval ([((even_part p) + (odd_part p)),pp],x) <> 0 & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 ) )

per cases ( eval ([((even_part p) + (odd_part p)),pp],x) = 0 or eval ([((even_part p) + (odd_part p)),pp],x) <> 0 ) ;

case eval ([((even_part p) + (odd_part p)),pp],x) = 0 ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1

hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 by A35, A36, COMPLEX1:44; :: thesis: verum

end;

case eval ([((even_part p) + (odd_part p)),pp],x) <> 0 ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1

then A38: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| > 0 by COMPLEX1:47;

now :: thesis: not |.(eval ([((even_part p) + (odd_part p)),pp],x)).| < 1

assume A39: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| < 1 ; :: thesis: contradiction
then E1 <= |.(eval ([((even_part p) + (odd_part p)),pp],x)).| by A38, SQUARE_1:42;
hence contradiction by A37, A39, XXREAL_0:2; :: thesis: verum

end;

hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 ; :: thesis: verum

end;

end;

end;

hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 ; :: thesis: verum

end;

case ( Re (eval ([(even_part p),(odd_part p)],x)) = 0 & eval ((odd_part p),x) <> 0. F_Complex ) ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1

then A40: (E1 - 1) / E2 = 0 by A34, A26;

now :: thesis: ( ( |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 = 0 & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 ) or ( |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 <> 0 & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 ) )

per cases ( |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 = 0 or |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 <> 0 ) ;

case |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 = 0 ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1

then |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| = 0 ;
then (eval ([((even_part p) + (odd_part p)),pp],x)) - 1 = 0 by COMPLEX1:45;
hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 by COMPLEX1:48; :: thesis: verum

end;

case |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 <> 0 ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1

then E1 - 1 = 0 by A40;
hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 by A25, COMPLEX1:46; :: thesis: verum

end;

end;

end;

hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 ; :: thesis: verum

end;

end;

end;

hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 ; :: thesis: verum

end;

thus for x being Element of F_Complex st Re x = 0 & eval ((odd_part p),x) <> 0 holds
Re (eval ([(even_part p),(odd_part p)],x)) >= 0 :: thesis: (even_part p) + (odd_part p) is Hurwitz

proof

let x be Element of F_Complex; :: thesis: ( Re x = 0 & eval ((odd_part p),x) <> 0 implies Re (eval ([(even_part p),(odd_part p)],x)) >= 0 )
assume A41: ( Re x = 0 & eval ((odd_part p),x) <> 0 ) ; :: thesis: Re (eval ([(even_part p),(odd_part p)],x)) >= 0
then A42: Im (eval ((even_part p),x)) = 0 by Th28;
A43: Re (eval ((odd_part p),x)) = 0 by A41, Th29;
A44: eval ((odd_part p),x) <> 0. F_Complex by A41, COMPLFLD:def 1;
reconsider y1 = eval ((even_part p),x) as Complex ;
reconsider y2 = eval ((odd_part p),x) as Complex ;
Re ((eval ((even_part p),x)) / (eval ((odd_part p),x))) = Re (y1 / y2) by A44, COMPLFLD:6
.= 0 by A42, A43, Th1 ;
hence Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ; :: thesis: verum

end;

now :: thesis: for x being Element of F_Complex st Re x >= 0 holds
not x is_a_root_of (even_part p) + (odd_part p)

let x be Element of F_Complex; :: thesis: ( Re x >= 0 implies not x is_a_root_of (even_part p) + (odd_part p) )
assume A45: Re x >= 0 ; :: thesis: not x is_a_root_of (even_part p) + (odd_part p)
reconsider RW = |.(eval ([((even_part p) + (odd_part p)),pp],x)).| ^2 as Real ;

now :: thesis: ( ( eval ((odd_part p),x) = eval ((even_part p),x) & not x is_a_root_of (even_part p) + (odd_part p) ) or ( eval ((odd_part p),x) <> eval ((even_part p),x) & not x is_a_root_of (even_part p) + (odd_part p) ) )

per cases ( eval ((odd_part p),x) = eval ((even_part p),x) or eval ((odd_part p),x) <> eval ((even_part p),x) ) ;

case A46: eval ((odd_part p),x) = eval ((even_part p),x) ; :: thesis: not x is_a_root_of (even_part p) + (odd_part p)

A47: now :: thesis: not eval ((even_part p),x) = 0. F_Complex

assume eval ((even_part p),x) = 0. F_Complex ; :: thesis: contradiction
then x is_a_common_root_of even_part p, odd_part p by A46, POLYNOM5:def 7;
hence contradiction by A1; :: thesis: verum

end;

now :: thesis: not eval (((even_part p) + (odd_part p)),x) = 0. F_Complex

assume eval (((even_part p) + (odd_part p)),x) = 0. F_Complex ; :: thesis: contradiction
then A48: (eval ((even_part p),x)) + (eval ((even_part p),x)) = 0. F_Complex by A46, POLYNOM4:19
.= 0 by COMPLFLD:def 1 ;
reconsider a = eval ((even_part p),x) as Complex ;
thus contradiction by A48, A47, COMPLFLD:def 1; :: thesis: verum

end;

hence not x is_a_root_of (even_part p) + (odd_part p) by POLYNOM5:def 7; :: thesis: verum

end;

case A49: eval ((odd_part p),x) <> eval ((even_part p),x) ; :: thesis: not x is_a_root_of (even_part p) + (odd_part p)

now :: thesis: ( ( Re x = 0 & not x is_a_root_of (even_part p) + (odd_part p) ) or ( Re x > 0 & eval (([(even_part p),(odd_part p)] `2),x) <> 0 & not x is_a_root_of (even_part p) + (odd_part p) ) or ( Re x > 0 & eval (([(even_part p),(odd_part p)] `2),x) = 0 & not x is_a_root_of (even_part p) + (odd_part p) ) )

per cases ( Re x = 0 or ( Re x > 0 & eval (([(even_part p),(odd_part p)] `2),x) <> 0 ) or ( Re x > 0 & eval (([(even_part p),(odd_part p)] `2),x) = 0 ) ) by A45;

case A50: Re x = 0 ; :: thesis: not x is_a_root_of (even_part p) + (odd_part p)

then A51: Im (eval ((even_part p),x)) = 0 by Th28;
A52: Re (eval ((odd_part p),x)) = 0 by A50, Th29;

now :: thesis: ( ( eval ((odd_part p),x) = 0 & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 ) or ( eval ((odd_part p),x) <> 0 & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 ) )

per cases ( eval ((odd_part p),x) = 0 or eval ((odd_part p),x) <> 0 ) ;

case A53: eval ((odd_part p),x) = 0 ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1

then A54: eval ((odd_part p),x) = 0. F_Complex by COMPLFLD:def 1;
A55: eval (pp,x) = (eval ((even_part p),x)) - (eval ((odd_part p),x)) by POLYNOM4:21
.= (eval ((even_part p),x)) - (0. F_Complex) by A53, COMPLFLD:def 1
.= eval ((even_part p),x) by RLVECT_1:13 ;
A56: eval (((even_part p) + (odd_part p)),x) = (eval ((even_part p),x)) + (eval ((odd_part p),x)) by POLYNOM4:19
.= eval ((even_part p),x) by A53 ;

A57: now :: thesis: not eval ((even_part p),x) = 0. F_Complex

assume eval ((even_part p),x) = 0. F_Complex ; :: thesis: contradiction
then x is_a_common_root_of even_part p, odd_part p by A54, POLYNOM5:def 7;
hence contradiction by A1; :: thesis: verum

end;

eval ([((even_part p) + (odd_part p)),pp],x) = ((eval ((even_part p),x)) ") * (eval ((even_part p),x)) by A55, A56
.= 1. F_Complex by VECTSP_1:def 10, A57
.= 1r by COMPLFLD:def 1 ;
hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 by COMPLEX1:48; :: thesis: verum

end;

case A58: eval ((odd_part p),x) <> 0 ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1

then A59: eval ((odd_part p),x) <> 0. F_Complex by COMPLFLD:def 1;
A60: eval ((odd_part p),x) <> 0. F_Complex by A58, COMPLFLD:def 1;
reconsider y1 = eval ((even_part p),x) as Complex ;
reconsider y2 = eval ((odd_part p),x) as Complex ;
reconsider E1 = |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 as Real ;
Re ((eval ((even_part p),x)) / (eval ((odd_part p),x))) = Re (y1 / y2) by A59, COMPLFLD:6
.= 0 by A51, A52, Th1 ;
then Re (eval ([(even_part p),(odd_part p)],x)) = 0 ;
then A61: (RW - 1) / E1 = 0 by A49, A60, A26;

now :: thesis: ( ( |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 = 0 & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 ) or ( |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 <> 0 & |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 ) )

per cases ( |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 = 0 or |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 <> 0 ) ;

case |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 = 0 ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1

then |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| = 0 ;
then (eval ([((even_part p) + (odd_part p)),pp],x)) - 1 = 0 by COMPLEX1:45;
hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 by COMPLEX1:48; :: thesis: verum

end;

case |.((eval ([((even_part p) + (odd_part p)),pp],x)) - 1).| ^2 <> 0 ; :: thesis: |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1

then RW - 1 = 0 by A61;
hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 by A25, COMPLEX1:46; :: thesis: verum

end;

end;

end;

hence |.(eval ([((even_part p) + (odd_part p)),pp],x)).| = 1 ; :: thesis: verum

end;

end;

end;

then eval (([((even_part p) + (odd_part p)),pp] `1),x) <> 0 by COMPLEX1:47;
then eval (((even_part p) + (odd_part p)),x) <> 0. F_Complex by COMPLFLD:def 1;
hence not x is_a_root_of (even_part p) + (odd_part p) by POLYNOM5:def 7; :: thesis: verum

end;

case ( Re x > 0 & eval (([(even_part p),(odd_part p)] `2),x) <> 0 ) ; :: thesis: not x is_a_root_of (even_part p) + (odd_part p)

then Re (eval ([(even_part p),(odd_part p)],x)) > 0 by A1;
then |.(eval ([((even_part p) + (odd_part p)),pp],x)).| >= 1 by A33, A49;
then eval (([((even_part p) + (odd_part p)),pp] `1),x) <> 0 by COMPLEX1:47;
then eval (((even_part p) + (odd_part p)),x) <> 0. F_Complex by COMPLFLD:def 1;
hence not x is_a_root_of (even_part p) + (odd_part p) by POLYNOM5:def 7; :: thesis: verum

end;

case ( Re x > 0 & eval (([(even_part p),(odd_part p)] `2),x) = 0 ) ; :: thesis: not x is_a_root_of (even_part p) + (odd_part p)

then A62: eval ((odd_part p),x) = 0. F_Complex by COMPLFLD:def 1;
A63: eval (pp,x) = (eval ((even_part p),x)) - (eval ((odd_part p),x)) by POLYNOM4:21
.= eval ((even_part p),x) by A62, RLVECT_1:13 ;
A64: eval (((even_part p) + (odd_part p)),x) = (eval ((even_part p),x)) + (eval ((odd_part p),x)) by POLYNOM4:19
.= eval ((even_part p),x) by A62, RLVECT_1:def 4 ;

A65: now :: thesis: not eval ((even_part p),x) = 0. F_Complex

assume eval ((even_part p),x) = 0. F_Complex ; :: thesis: contradiction
then x is_a_common_root_of even_part p, odd_part p by A62, POLYNOM5:def 7;
hence contradiction by A1; :: thesis: verum

end;

eval ([((even_part p) + (odd_part p)),pp],x) = ((eval ((even_part p),x)) ") * (eval ((even_part p),x)) by A63, A64
.= 1. F_Complex by VECTSP_1:def 10, A65
.= 1r by COMPLFLD:def 1 ;
then eval (([((even_part p) + (odd_part p)),pp] `1),x) <> 0 by COMPLEX1:47, COMPLEX1:48;
then eval (((even_part p) + (odd_part p)),x) <> 0. F_Complex by COMPLFLD:def 1;
hence not x is_a_root_of (even_part p) + (odd_part p) by POLYNOM5:def 7; :: thesis: verum

end;

end;

end;

hence not x is_a_root_of (even_part p) + (odd_part p) ; :: thesis: verum

end;

end;

end;

hence not x is_a_root_of (even_part p) + (odd_part p) ; :: thesis: verum

end;

hence (even_part p) + (odd_part p) is Hurwitz ; :: thesis: verum

end;

end;