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