let f be Polynomial of F_Complex; :: thesis: ( deg f >= 1 implies for rho being Element of F_Complex st Re rho < 0 & |.(eval (f,rho)).| < |.(eval ((f *'),rho)).| holds
( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ) )
assume A1: deg f >= 1 ; :: thesis: for rho being Element of F_Complex st Re rho < 0 & |.(eval (f,rho)).| < |.(eval ((f *'),rho)).| holds
( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz )
let rho be Element of F_Complex; :: thesis: ( Re rho < 0 & |.(eval (f,rho)).| < |.(eval ((f *'),rho)).| implies ( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ) )
assume that
A2: Re rho < 0 and
A3: |.(eval (f,rho)).| < |.(eval ((f *'),rho)).| ; :: thesis: ( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz )
reconsider ef = eval (f,rho), ef1 = eval ((f *'),rho) as Element of F_Complex ;

now :: thesis: ( (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz implies f is Hurwitz )

- 1 < deg (rpoly (1,rho)) by Th27;
then A4: deg (0_. F_Complex) < deg (rpoly (1,rho)) by Th20;
eval (((ef1 * f) - (ef * (f *'))),rho) = (eval ((ef1 * f),rho)) - (eval ((ef * (f *')),rho)) by POLYNOM4:21
.= (ef1 * (eval (f,rho))) - (eval ((ef * (f *')),rho)) by POLYNOM5:30
.= (ef1 * (eval (f,rho))) - (ef * (eval ((f *'),rho))) by POLYNOM5:30
.= 0. F_Complex by RLVECT_1:15 ;
then rho is_a_root_of (ef1 * f) - (ef * (f *')) by POLYNOM5:def 7;
then consider t being Polynomial of F_Complex such that
A5: F* (f,rho) = (rpoly (1,rho)) *' t by Th33;
F* (f,rho) = ((rpoly (1,rho)) *' t) + (0_. F_Complex) by A5, POLYNOM3:28;
then A6: F* (f,rho) = ((F* (f,rho)) div (rpoly (1,rho))) *' (rpoly (1,rho)) by A5, A4, Def5;
(1_ F_Complex) * (rpoly (1,rho)) is Hurwitz by A2, Th39;
then A7: rpoly (1,rho) is Hurwitz by POLYNOM5:27;
assume (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ; :: thesis: f is Hurwitz
then F* (f,rho) is Hurwitz by A6, A7, Th41;
hence f is Hurwitz by A1, A3, Th50; :: thesis: verum

end;

hence ( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz ) by A1, A2, Th51; :: thesis: verum