let x, z be Element of F_Complex; :: thesis: ( x <> 0. F_Complex implies ( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 ) )
set p = x * (rpoly (1,z));
assume A1: x <> 0. F_Complex ; :: thesis: ( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 )
A2: now :: thesis: ( Re z < 0 implies x * (rpoly (1,z)) is Hurwitz )
assume A3: Re z < 0 ; :: thesis: x * (rpoly (1,z)) is Hurwitz
now :: thesis: for y being Element of F_Complex st y is_a_root_of x * (rpoly (1,z)) holds
Re y < 0
let y be Element of F_Complex; :: thesis: ( y is_a_root_of x * (rpoly (1,z)) implies Re y < 0 )
assume y is_a_root_of x * (rpoly (1,z)) ; :: thesis: Re y < 0
then 0. F_Complex = eval ((x * (rpoly (1,z))),y) by POLYNOM5:def 7
.= x * (eval ((rpoly (1,z)),y)) by POLYNOM5:30
.= x * (y - z) by Th29 ;
then y - z = 0. F_Complex by A1, VECTSP_1:12;
hence Re y < 0 by A3, RLVECT_1:21; :: thesis: verum
end;
hence x * (rpoly (1,z)) is Hurwitz ; :: thesis: verum
end;
now :: thesis: ( x * (rpoly (1,z)) is Hurwitz implies Re z < 0 )
eval ((x * (rpoly (1,z))),z) = x * (eval ((rpoly (1,z)),z)) by POLYNOM5:30
.= x * (z - z) by Th29
.= x * (0. F_Complex) by RLVECT_1:15
.= 0. F_Complex ;
then A4: z is_a_root_of x * (rpoly (1,z)) by POLYNOM5:def 7;
assume x * (rpoly (1,z)) is Hurwitz ; :: thesis: Re z < 0
hence Re z < 0 by A4; :: thesis: verum
end;
hence ( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 ) by A2; :: thesis: verum