let f be Polynomial of F_Complex; :: thesis: ( f is Hurwitz implies for x being Element of F_Complex st Re x >= 0 holds
0 < |.(eval (f,x)).| )
assume A1: f is Hurwitz ; :: thesis: for x being Element of F_Complex st Re x >= 0 holds
0 < |.(eval (f,x)).|
let x be Element of F_Complex; :: thesis: ( Re x >= 0 implies 0 < |.(eval (f,x)).| )
assume A2: Re x >= 0 ; :: thesis: 0 < |.(eval (f,x)).|
eval (f,x) <> 0. F_Complex by A1, A2, POLYNOM5:def 7;
hence 0 < |.(eval (f,x)).| by COMPLEX1:47, COMPLFLD:7; :: thesis: verum