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: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 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, Th49;
then (ef1 * f) - (ef * (f *')) is Hurwitz by A1, A4, Th50;
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:28;
hence (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz by A5, A6, Def5; :: thesis: verum