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

- 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:24
.= (ef1 * (eval f,rho)) - (eval (ef * (f *' )),rho) by POLYNOM5:31
.= (ef1 * (eval f,rho)) - (ef * (eval (f *' ),rho)) by POLYNOM5:31
.= 0. F_Complex by RLVECT_1:28 ;
then rho is_a_root_of (ef1 * f) - (ef * (f *' )) by POLYNOM5:def 6;
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:29;
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:28;
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, Th51; :: thesis: verum

end;

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