let f be Polynomial of F_Complex ; :: thesis: ( deg f >= 1 implies for rho being Element of F_Complex st Re rho < 0 & f is Hurwitz holds
(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 & f is Hurwitz holds
(F* f,rho) div (rpoly 1,rho) is Hurwitz
let rho be Element of F_Complex ; :: thesis: ( Re rho < 0 & f is Hurwitz implies (F* f,rho) div (rpoly 1,rho) is Hurwitz )
assume A2: Re rho < 0 ; :: thesis: ( not f is Hurwitz or (F* f,rho) div (rpoly 1,rho) is Hurwitz )
reconsider ef = eval f,rho, ef1 = eval (f *' ),rho as Element of F_Complex ;
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 s being Polynomial of F_Complex such that
A3: (ef1 * f) - (ef * (f *' )) = (rpoly 1,rho) *' s by Th33;
assume A4: f is Hurwitz ; :: thesis: (F* f,rho) div (rpoly 1,rho) is Hurwitz
then |.(eval f,rho).| < |.(eval (f *' ),rho).| by A1, A2, Th50;
then (ef1 * f) - (ef * (f *' )) is Hurwitz by A1, A4, Th51;
then A5: s is Hurwitz by A3, Th41;
- 1 < deg (rpoly 1,rho) by Th27;
then A6: deg (0_. F_Complex ) < deg (rpoly 1,rho) by Th20;
(ef1 * f) - (ef * (f *' )) = (s *' (rpoly 1,rho)) + (0_. F_Complex ) by A3, POLYNOM3:29;
hence (F* f,rho) div (rpoly 1,rho) is Hurwitz by A5, A6, Def5; :: thesis: verum