let a, b be Element of F_Complex; :: thesis: ( |.a.| > |.b.| implies for f being Polynomial of F_Complex st deg f >= 1 holds
( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) )
assume A1: |.a.| > |.b.| ; :: thesis: for f being Polynomial of F_Complex st deg f >= 1 holds
( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz )
then A2: 0 < |.a.| by COMPLEX1:46;
then A3: a <> 0. F_Complex by COMPLEX1:47, COMPLFLD:7;
let f be Polynomial of F_Complex; :: thesis: ( deg f >= 1 implies ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) )
assume A4: deg f >= 1 ; :: thesis: ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz )
set g = (a * f) - (b * (f *'));

per cases ( b = 0. F_Complex or b <> 0. F_Complex ) ;

suppose b = 0. F_Complex ; :: thesis: ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz )

then (a * f) - (b * (f *')) = (a * f) - (0_. F_Complex) by POLYNOM5:26
.= (a * f) + (0_. F_Complex) by Th9
.= a * f by POLYNOM3:28 ;
hence ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) by A3, Th40; :: thesis: verum

end;

suppose A5: b <> 0. F_Complex ; :: thesis: ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz )

reconsider a9 = a, b9 = b as Element of COMPLEX by COMPLFLD:def 1;
((|.a.| ^2) - (|.b.| ^2)) " in COMPLEX by XCMPLX_0:def 2;
then reconsider zz = ((|.a.| ^2) - (|.b.| ^2)) " as Element of F_Complex by COMPLFLD:def 1;
set a1 = (a *') * zz;
set b1 = - (b * zz);
reconsider a19 = (a *') * zz, b19 = - (b * zz) as Element of COMPLEX by COMPLFLD:def 1;
A6: (a *') * (b ") = (a9 *') * (b9 ") by A5, COMPLFLD:5;
A7: b19 = - (b9 * (((|.a.| ^2) - (|.b.| ^2)) ")) by COMPLFLD:2;
A8: 0 < |.b.| by A5, COMPLEX1:47, COMPLFLD:7;
then |.a9.| * |.b9.| > |.b9.| * |.b9.| by A1, XREAL_1:68;
then A9: (|.a9.| ^2) - (|.b9.| ^2) <> 0 by A1, A2, XREAL_1:68;
then A10: - (- (b * zz)) <> 0. F_Complex by A5, COMPLFLD:7, RLVECT_1:17;

A11: now :: thesis: ( f is Hurwitz implies (a * f) - (b * (f *')) is Hurwitz )

assume A12: f is Hurwitz ; :: thesis: (a * f) - (b * (f *')) is Hurwitz

now :: thesis: for z being Element of F_Complex st z is_a_root_of (a * f) - (b * (f *')) holds
Re z < 0

let z be Element of F_Complex; :: thesis: ( z is_a_root_of (a * f) - (b * (f *')) implies Re z < 0 )
assume z is_a_root_of (a * f) - (b * (f *')) ; :: thesis: Re z < 0
then A13: 0. F_Complex = eval (((a * f) - (b * (f *'))),z) by POLYNOM5:def 7
.= (eval ((a * f),z)) - (eval ((b * (f *')),z)) by POLYNOM4:21
.= (a * (eval (f,z))) - (eval ((b * (f *')),z)) by POLYNOM5:30
.= (a * (eval (f,z))) - (b * (eval ((f *'),z))) by POLYNOM5:30 ;

now :: thesis: not Re z >= 0

A14: 0 <= |.b.| by COMPLEX1:46;
A15: |.a.| * |.(eval (f,z)).| = |.(a * (eval (f,z))).| by COMPLEX1:65;
A16: |.b.| * |.(eval ((f *'),z)).| = |.(b * (eval ((f *'),z))).| by COMPLEX1:65;
assume A17: Re z >= 0 ; :: thesis: contradiction

per cases ( Re z = 0 or Re z > 0 ) by A17;

suppose A18: Re z = 0 ; :: thesis: contradiction

then A19: |.(eval (f,z)).| > 0 by A12, Th48;
|.(eval (f,z)).| = |.(eval ((f *'),z)).| by A4, A12, A18, Th49;
then |.a.| * |.(eval (f,z)).| > |.b.| * |.(eval ((f *'),z)).| by A1, A19, XREAL_1:68;
hence contradiction by A13, A15, A16, VECTSP_1:19; :: thesis: verum

end;

suppose Re z > 0 ; :: thesis: contradiction

then A20: |.(eval (f,z)).| > |.(eval ((f *'),z)).| by A4, A12, Th49;
then |.(eval (f,z)).| > 0 by COMPLEX1:46;
then A21: |.a.| * |.(eval (f,z)).| > |.b.| * |.(eval (f,z)).| by A1, XREAL_1:68;
|.b.| * |.(eval (f,z)).| >= |.b.| * |.(eval ((f *'),z)).| by A14, A20, XREAL_1:64;
hence contradiction by A13, A15, A16, A21, VECTSP_1:19; :: thesis: verum

end;

end;

end;

hence Re z < 0 ; :: thesis: verum

end;

hence (a * f) - (b * (f *')) is Hurwitz ; :: thesis: verum

end;

A22: |.((a *') * zz).| = |.(a *').| * |.(((|.a.| ^2) - (|.b.| ^2)) ").| by COMPLEX1:65
.= |.a.| * |.(((|.a.| ^2) - (|.b.| ^2)) ").| by COMPLEX1:53 ;

A23: now :: thesis: for z being Element of COMPLEX holds (z *') * z = |.z.| ^2

let z be Element of COMPLEX ; :: thesis: (z *') * z = |.z.| ^2
A24: Im (z * (z *')) = 0 by COMPLEX1:40;
A25: (Re (z * (z *'))) + ((Im (z * (z *'))) * <i>) = z * (z *') by COMPLEX1:13;
A26: (Im z) ^2 >= 0 by XREAL_1:63;
A27: (Re z) ^2 >= 0 by XREAL_1:63;
Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) by COMPLEX1:40;
hence (z *') * z = |.z.| ^2 by A24, A25, A27, A26, SQUARE_1:def 2; :: thesis: verum

end;

then A28: (b9 *') * b9 = |.b9.| ^2 ;
A29: (((a9 *') * a9) * (b9 ")) - (b9 *') = (((|.a9.| ^2) * (b9 ")) - (b9 *')) * 1 by A23
.= (((|.a9.| ^2) * (b9 ")) - (b9 *')) * (b9 * (b9 ")) by A5, COMPLFLD:7, XCMPLX_0:def 7
.= (((|.a9.| ^2) * ((b9 ") * b9)) - (|.b9.| ^2)) * (b9 ") by A28
.= (((|.a9.| ^2) * 1) - (|.b9.| ^2)) * (b9 ") by A5, COMPLFLD:7, XCMPLX_0:def 7 ;
then A30: - (((((a9 *') * a9) * (b9 ")) - (b9 *')) ") = - ((((|.a9.| ^2) - (|.b9.| ^2)) ") * ((b9 ") ")) by XCMPLX_1:204
.= b19 by COMPLFLD:2 ;
A31: b19 = - (b9 * (((|.a.| ^2) - (|.b.| ^2)) ")) by COMPLFLD:2
.= (- b9) * (((|.a.| ^2) - (|.b.| ^2)) ") ;
then (- (b * zz)) " = b19 " by A5, A9, COMPLFLD:5, COMPLFLD:7;
then A32: - ((- (b * zz)) ") = - (b19 ") by COMPLFLD:2;

A33: now :: thesis: not (- (b * zz)) " = 0. F_Complex

assume A34: (- (b * zz)) " = 0. F_Complex ; :: thesis: contradiction
((- (b * zz)) ") * (- (b * zz)) = 1_ F_Complex by A5, A9, A31, COMPLFLD:7, VECTSP_1:def 10;
hence contradiction by A34; :: thesis: verum

end;

A35: now :: thesis: not - ((- (b * zz)) ") = 0. F_Complex

assume - ((- (b * zz)) ") = 0. F_Complex ; :: thesis: contradiction
then - (- ((- (b * zz)) ")) = 0. F_Complex by RLVECT_1:12;
hence contradiction by A33, RLVECT_1:17; :: thesis: verum

end;

(- (b * zz)) " = b19 " by A5, A9, A31, COMPLFLD:5, COMPLFLD:7;
then - ((- (b * zz)) ") = - (b19 ") by COMPLFLD:2;
then A36: (- ((- (b * zz)) ")) " = (- (b19 ")) " by A35, COMPLFLD:5;
(- ((- (b * zz)) ")) " = - (((- (b * zz)) ") ") by A33, Th1
.= - (- (b * zz)) by A5, A9, A31, COMPLFLD:7, VECTSP_1:24 ;
then ((- (b19 ")) ") * ((a9 *') * (b9 ")) = (- (- (b9 * (((|.a.| ^2) - (|.b.| ^2)) ")))) * ((a9 *') * (b9 ")) by A7, A36, COMPLFLD:2
.= ((b9 * (b9 ")) * (((|.a.| ^2) - (|.b.| ^2)) ")) * (a9 *')
.= (1 * (((|.a.| ^2) - (|.b.| ^2)) ")) * (a9 *') by A5, COMPLFLD:7, XCMPLX_0:def 7
.= a19 ;
then A37: ((- ((- (b * zz)) ")) ") * ((a *') * (b ")) = (a *') * zz by A35, A6, A32, COMPLFLD:5;
A38: (a9 *') * ((b9 ") * a9) = (a *') * ((b ") * a) by A5, COMPLFLD:5;
A39: |.(- (b * zz)).| = |.(- (b * (((|.a.| ^2) - (|.b.| ^2)) "))).| by COMPLFLD:2
.= |.(b * (((|.a.| ^2) - (|.b.| ^2)) ")).| by COMPLEX1:52
.= |.b.| * |.(((|.a.| ^2) - (|.b.| ^2)) ").| by COMPLEX1:65 ;
- (- (b * zz)) = - b19 by COMPLFLD:2;
then A40: (- b19) " = (- (- (b * zz))) " by A10, COMPLFLD:5
.= - ((- (b * zz)) ") by A5, A9, A31, Th1, COMPLFLD:7 ;
A41: |.b.| * |.a.| > |.b.| * |.b.| by A1, A8, XREAL_1:68;
|.a.| * |.a.| > |.b.| * |.a.| by A1, A2, XREAL_1:68;
then |.a.| ^2 > |.b.| * |.b.| by A41, XXREAL_0:2;
then A42: (|.a.| ^2) - (|.b.| ^2) > (|.b.| ^2) - (|.b.| ^2) by XREAL_1:9;

A43: now :: thesis: not b19 = 0. F_Complex

assume b19 = 0. F_Complex ; :: thesis: contradiction
then (- b) * zz = 0. F_Complex by VECTSP_1:9;
then - b = 0. F_Complex by A42, COMPLFLD:7;
then b = - (0. F_Complex) by RLVECT_1:17;
hence contradiction by A5, RLVECT_1:12; :: thesis: verum

end;

(b * (f *')) + ((a * f) - (b * (f *'))) = (a * f) + ((- (b * (f *'))) + (b * (f *'))) by POLYNOM3:26
.= (a * f) + ((b * (f *')) - (b * (f *')))
.= (a * f) + (0_. F_Complex) by POLYNOM3:29 ;
then A44: (a * f) - ((a * f) - (b * (f *'))) = ((b * (f *')) + ((a * f) - (b * (f *')))) - ((a * f) - (b * (f *'))) by POLYNOM3:28
.= (b * (f *')) + (((a * f) - (b * (f *'))) - ((a * f) - (b * (f *')))) by POLYNOM3:26
.= (b * (f *')) + (0_. F_Complex) by POLYNOM3:29 ;
A45: f *' = (1_ F_Complex) * (f *') by POLYNOM5:27
.= ((b ") * b) * (f *') by A5, VECTSP_1:def 10
.= (b ") * (b * (f *')) by Th14
.= (b ") * ((a * f) - ((a * f) - (b * (f *')))) by A44, POLYNOM3:28 ;
((a * f) - (b * (f *'))) *' = ((a * f) *') + ((- (b * (f *'))) *') by Th45
.= ((a * f) *') + (- ((b * (f *')) *')) by Th44
.= ((a *') * (f *')) + (- ((b * (f *')) *')) by Th43
.= ((a *') * (f *')) + (- ((b *') * ((f *') *'))) by Th43
.= ((a *') * (f *')) + (- ((b *') * f)) ;
then ((a * f) - (b * (f *'))) *' = ((a *') * (((b ") * (a * f)) + ((b ") * (- ((a * f) - (b * (f *'))))))) + (- ((b *') * f)) by A45, Th18
.= (((a *') * ((b ") * (a * f))) + ((a *') * ((b ") * (- ((a * f) - (b * (f *'))))))) + (- ((b *') * f)) by Th18
.= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + (((a *') * ((b ") * (a * f))) + (- ((b *') * f))) by POLYNOM3:26
.= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + (((a *') * (((b ") * a) * f)) + (- ((b *') * f))) by Th14
.= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + ((((a *') * ((b ") * a)) * f) + (- ((b *') * f))) by Th14
.= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + ((((a *') * ((b ") * a)) * f) + ((- (b *')) * f)) by Th15
.= ((a *') * ((b ") * (- ((a * f) - (b * (f *')))))) + ((((a *') * ((b ") * a)) + (- (b *'))) * f) by Th17
.= (((a *') * (b ")) * (- ((a * f) - (b * (f *'))))) + ((((a *') * ((b ") * a)) + (- (b *'))) * f) by Th14 ;
then A46: (((a * f) - (b * (f *'))) *') + (- (((a *') * (b ")) * (- ((a * f) - (b * (f *')))))) = ((((a *') * ((b ") * a)) + (- (b *'))) * f) + ((((a *') * (b ")) * (- ((a * f) - (b * (f *'))))) - (((a *') * (b ")) * (- ((a * f) - (b * (f *')))))) by POLYNOM3:26
.= ((((a *') * ((b ") * a)) + (- (b *'))) * f) + (0_. F_Complex) by POLYNOM3:29 ;
A47: - (b9 *') = - (b *') by COMPLFLD:2;
A48: f = (1_ F_Complex) * f by POLYNOM5:27
.= (((- ((- (b * zz)) ")) ") * (- ((- (b * zz)) "))) * f by A5, A29, A9, A30, A40, COMPLFLD:7, VECTSP_1:def 10
.= ((- ((- (b * zz)) ")) ") * ((- ((- (b * zz)) ")) * f) by Th14
.= ((- ((- (b * zz)) ")) ") * ((((a * f) - (b * (f *'))) *') + (- (((a *') * (b ")) * (- ((a * f) - (b * (f *'))))))) by A46, A30, A38, A47, A40, POLYNOM3:28
.= (((- ((- (b * zz)) ")) ") * (((a * f) - (b * (f *'))) *')) + (((- ((- (b * zz)) ")) ") * (- (((a *') * (b ")) * (- ((a * f) - (b * (f *'))))))) by Th18
.= (((- ((- (b * zz)) ")) ") * (((a * f) - (b * (f *'))) *')) + (((- ((- (b * zz)) ")) ") * (((a *') * (b ")) * (- (- ((a * f) - (b * (f *'))))))) by Th16
.= (((- ((- (b * zz)) ")) ") * (((a * f) - (b * (f *'))) *')) + (((- ((- (b * zz)) ")) ") * (((a *') * (b ")) * ((a * f) - (b * (f *'))))) by Lm3
.= (((- ((- (b * zz)) ")) ") * (((a * f) - (b * (f *'))) *')) + (((a *') * zz) * ((a * f) - (b * (f *')))) by A37, Th14
.= ((((- (- (b * zz))) ") ") * (((a * f) - (b * (f *'))) *')) + (((a *') * zz) * ((a * f) - (b * (f *')))) by A5, A9, A31, Th1, COMPLFLD:7
.= ((- (- (b * zz))) * (((a * f) - (b * (f *'))) *')) + (((a *') * zz) * ((a * f) - (b * (f *')))) by A10, VECTSP_1:24
.= (- ((- (b * zz)) * (((a * f) - (b * (f *'))) *'))) + (((a *') * zz) * ((a * f) - (b * (f *')))) by Th15 ;
then deg f <= max ((deg (((a *') * zz) * ((a * f) - (b * (f *'))))),(deg (- ((- (b * zz)) * (((a * f) - (b * (f *'))) *'))))) by Th22;
then A49: deg f <= max ((deg (((a *') * zz) * ((a * f) - (b * (f *'))))),(deg ((- (b * zz)) * (((a * f) - (b * (f *'))) *')))) by POLYNOM4:8;
|.(((|.a.| ^2) - (|.b.| ^2)) ").| > 0 by A42, COMPLEX1:47;
then A50: |.((a *') * zz).| > |.(- (b * zz)).| by A1, A22, A39, XREAL_1:68;
then |.((a *') * zz).| > 0 by COMPLEX1:46;
then (a *') * zz <> 0. F_Complex by COMPLEX1:47, COMPLFLD:7;
then deg f <= max ((deg ((a * f) - (b * (f *')))),(deg ((- (b * zz)) * (((a * f) - (b * (f *'))) *')))) by A49, POLYNOM5:25;
then deg f <= max ((deg ((a * f) - (b * (f *')))),(deg (((a * f) - (b * (f *'))) *'))) by A43, POLYNOM5:25;
then deg f <= max ((deg ((a * f) - (b * (f *')))),(deg ((a * f) - (b * (f *'))))) by Th42;
then A51: deg ((a * f) - (b * (f *'))) >= 1 by A4, XXREAL_0:2;

now :: thesis: ( (a * f) - (b * (f *')) is Hurwitz implies f is Hurwitz )

assume A52: (a * f) - (b * (f *')) is Hurwitz ; :: thesis: f is Hurwitz

now :: thesis: for z being Element of F_Complex st z is_a_root_of f holds
Re z < 0

let z be Element of F_Complex; :: thesis: ( z is_a_root_of f implies Re z < 0 )
assume z is_a_root_of f ; :: thesis: Re z < 0
then A53: 0. F_Complex = eval (((((a *') * zz) * ((a * f) - (b * (f *')))) - ((- (b * zz)) * (((a * f) - (b * (f *'))) *'))),z) by A48, POLYNOM5:def 7
.= (eval ((((a *') * zz) * ((a * f) - (b * (f *')))),z)) - (eval (((- (b * zz)) * (((a * f) - (b * (f *'))) *')),z)) by POLYNOM4:21
.= (((a *') * zz) * (eval (((a * f) - (b * (f *'))),z))) - (eval (((- (b * zz)) * (((a * f) - (b * (f *'))) *')),z)) by POLYNOM5:30
.= (((a *') * zz) * (eval (((a * f) - (b * (f *'))),z))) - ((- (b * zz)) * (eval ((((a * f) - (b * (f *'))) *'),z))) by POLYNOM5:30 ;

now :: thesis: not Re z >= 0

A54: 0 <= |.(- (b * zz)).| by COMPLEX1:46;
A55: |.((a *') * zz).| * |.(eval (((a * f) - (b * (f *'))),z)).| = |.(((a *') * zz) * (eval (((a * f) - (b * (f *'))),z))).| by COMPLEX1:65;
A56: |.(- (b * zz)).| * |.(eval ((((a * f) - (b * (f *'))) *'),z)).| = |.((- (b * zz)) * (eval ((((a * f) - (b * (f *'))) *'),z))).| by COMPLEX1:65;
assume A57: Re z >= 0 ; :: thesis: contradiction

per cases ( Re z = 0 or Re z > 0 ) by A57;

suppose A58: Re z = 0 ; :: thesis: contradiction

then A59: |.(eval (((a * f) - (b * (f *'))),z)).| > 0 by A52, Th48;
|.(eval (((a * f) - (b * (f *'))),z)).| = |.(eval ((((a * f) - (b * (f *'))) *'),z)).| by A51, A52, A58, Th49;
then |.((a *') * zz).| * |.(eval (((a * f) - (b * (f *'))),z)).| > |.(- (b * zz)).| * |.(eval ((((a * f) - (b * (f *'))) *'),z)).| by A50, A59, XREAL_1:68;
hence contradiction by A53, A55, A56, VECTSP_1:19; :: thesis: verum

end;

suppose Re z > 0 ; :: thesis: contradiction

then A60: |.(eval (((a * f) - (b * (f *'))),z)).| > |.(eval ((((a * f) - (b * (f *'))) *'),z)).| by A51, A52, Th49;
then |.(eval (((a * f) - (b * (f *'))),z)).| > 0 by COMPLEX1:46;
then A61: |.((a *') * zz).| * |.(eval (((a * f) - (b * (f *'))),z)).| > |.(- (b * zz)).| * |.(eval (((a * f) - (b * (f *'))),z)).| by A50, XREAL_1:68;
|.(- (b * zz)).| * |.(eval (((a * f) - (b * (f *'))),z)).| >= |.(- (b * zz)).| * |.(eval ((((a * f) - (b * (f *'))) *'),z)).| by A54, A60, XREAL_1:64;
hence contradiction by A53, A55, A56, A61, VECTSP_1:19; :: thesis: verum

end;

end;

end;

hence Re z < 0 ; :: thesis: verum

end;

hence f is Hurwitz ; :: thesis: verum

end;

hence ( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz ) by A11; :: thesis: verum

end;

end;