let f be Polynomial of F_Complex; :: thesis: for z being Element of F_Complex st z <> 0. F_Complex holds
( f is Hurwitz iff z * f is Hurwitz )
let z be Element of F_Complex; :: thesis: ( z <> 0. F_Complex implies ( f is Hurwitz iff z * f is Hurwitz ) )
assume A1: z <> 0. F_Complex ; :: thesis: ( f is Hurwitz iff z * f is Hurwitz )
A2: now :: thesis: ( f is Hurwitz implies z * f is Hurwitz )
assume A3: f is Hurwitz ; :: thesis: z * f is Hurwitz
now :: thesis: for x being Element of F_Complex st x is_a_root_of z * f holds
Re x < 0
let x be Element of F_Complex; :: thesis: ( x is_a_root_of z * f implies Re x < 0 )
assume x is_a_root_of z * f ; :: thesis: Re x < 0
then 0. F_Complex = eval ((z * f),x) by POLYNOM5:def 7
.= z * (eval (f,x)) by POLYNOM5:30 ;
then eval (f,x) = 0. F_Complex by A1, VECTSP_1:12;
then x is_a_root_of f by POLYNOM5:def 7;
hence Re x < 0 by A3; :: thesis: verum
end;
hence z * f is Hurwitz ; :: thesis: verum
end;
now :: thesis: ( z * f is Hurwitz implies f is Hurwitz )
assume A4: z * f is Hurwitz ; :: thesis: f is Hurwitz
now :: thesis: for x being Element of F_Complex st x is_a_root_of f holds
Re x < 0
let x be Element of F_Complex; :: thesis: ( x is_a_root_of f implies Re x < 0 )
assume A5: x is_a_root_of f ; :: thesis: Re x < 0
eval ((z * f),x) = z * (eval (f,x)) by POLYNOM5:30
.= z * (0. F_Complex) by A5, POLYNOM5:def 7
.= 0. F_Complex ;
then x is_a_root_of z * f by POLYNOM5:def 7;
hence Re x < 0 by A4; :: thesis: verum
end;
hence f is Hurwitz ; :: thesis: verum
end;
hence ( f is Hurwitz iff z * f is Hurwitz ) by A2; :: thesis: verum