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:132;
then A3: a <> 0. F_Complex by COMPLEX1:133, COMPLFLD:9;
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:27
.= (a * f) + (0_. F_Complex ) by Th9
.= a * f by POLYNOM3:29 ;
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:7;
A7: b19 = - (b9 * (((|.a.| ^2 ) - (|.b.| ^2 )) " )) by COMPLFLD:4;
A8: 0 < |.b.| by A5, COMPLEX1:133, COMPLFLD:9;
then |.a9.| * |.b9.| > |.b9.| * |.b9.| by A1, XREAL_1:70;
then A9: (|.a9.| ^2 ) - (|.b9.| ^2 ) <> 0 by A1, A2, XREAL_1:70;
A10: - (- (b * zz)) <> 0. F_Complex by A5, A9, COMPLFLD:9, RLVECT_1:30;

A11: now

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

now

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 6
.= (eval (a * f),z) - (eval (b * (f *' )),z) by POLYNOM4:24
.= (a * (eval f,z)) - (eval (b * (f *' )),z) by POLYNOM5:31
.= (a * (eval f,z)) - (b * (eval (f *' ),z)) by POLYNOM5:31 ;

now

A14: 0 <= |.b.| by COMPLEX1:132;
A15: |.a.| * |.(eval f,z).| = |.(a * (eval f,z)).| by COMPLEX1:151;
A16: |.b.| * |.(eval (f *' ),z).| = |.(b * (eval (f *' ),z)).| by COMPLEX1:151;
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, Th49;
|.(eval f,z).| = |.(eval (f *' ),z).| by A4, A12, A18, Th50;
then |.a.| * |.(eval f,z).| > |.b.| * |.(eval (f *' ),z).| by A1, A19, XREAL_1:70;
hence contradiction by A13, A15, A16, VECTSP_1:66; :: thesis: verum

end;

suppose Re z > 0 ; :: thesis: contradiction

then A20: |.(eval f,z).| > |.(eval (f *' ),z).| by A4, A12, Th50;
then |.(eval f,z).| > 0 by COMPLEX1:132;
then A21: |.a.| * |.(eval f,z).| > |.b.| * |.(eval f,z).| by A1, XREAL_1:70;
|.b.| * |.(eval f,z).| >= |.b.| * |.(eval (f *' ),z).| by A14, A20, XREAL_1:66;
hence contradiction by A13, A15, A16, A21, VECTSP_1:66; :: thesis: verum

end;

end;

end;

hence Re z < 0 ; :: thesis: verum

end;

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

end;

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

A23: now

let z be Element of COMPLEX ; :: thesis: (z *' ) * z = |.z.| ^2
A24: Im (z * (z *' )) = 0 by COMPLEX1:126;
A25: (Re (z * (z *' ))) + ((Im (z * (z *' ))) * <i> ) = z * (z *' ) by COMPLEX1:29;
A26: (Im z) ^2 >= 0 by XREAL_1:65;
A27: (Re z) ^2 >= 0 by XREAL_1:65;
Re (z * (z *' )) = ((Re z) ^2 ) + ((Im z) ^2 ) by COMPLEX1:126;
hence (z *' ) * z = |.z.| ^2 by A24, A25, A27, A26, SQUARE_1:def 4; :: 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:9, XCMPLX_0:def 7
.= (((|.a9.| ^2 ) * ((b9 " ) * b9)) - (|.b9.| ^2 )) * (b9 " ) by A28
.= (((|.a9.| ^2 ) * 1) - (|.b9.| ^2 )) * (b9 " ) by A5, COMPLFLD:9, XCMPLX_0:def 7 ;
then A30: - (((((a9 *' ) * a9) * (b9 " )) - (b9 *' )) " ) = - ((((|.a9.| ^2 ) - (|.b9.| ^2 )) " ) * ((b9 " ) " )) by XCMPLX_1:205
.= b19 by COMPLFLD:4 ;
A31: b19 = - (b9 * (((|.a.| ^2 ) - (|.b.| ^2 )) " )) by COMPLFLD:4
.= (- b9) * (((|.a.| ^2 ) - (|.b.| ^2 )) " ) ;
then (- (b * zz)) " = b19 " by A5, A9, COMPLFLD:7, COMPLFLD:9;
then A32: - ((- (b * zz)) " ) = - (b19 " ) by COMPLFLD:4;

A33: now

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

end;

A35: now

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

end;

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

A43: now

assume b19 = 0. F_Complex ; :: thesis: contradiction
then (- b) * zz = 0. F_Complex by VECTSP_1:41;
then - b = 0. F_Complex by A42, COMPLFLD:9;
then b = - (0. F_Complex ) by RLVECT_1:30;
hence contradiction by A5, RLVECT_1:25; :: 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:30 ;
then A44: (a * f) - ((a * f) - (b * (f *' ))) = ((b * (f *' )) + ((a * f) - (b * (f *' )))) - ((a * f) - (b * (f *' ))) by POLYNOM3:29
.= (b * (f *' )) + (((a * f) - (b * (f *' ))) - ((a * f) - (b * (f *' )))) by POLYNOM3:26
.= (b * (f *' )) + (0_. F_Complex ) by POLYNOM3:30 ;
A45: f *' = (1_ F_Complex ) * (f *' ) by POLYNOM5:28
.= ((b " ) * b) * (f *' ) by A5, VECTSP_1:def 22
.= (b " ) * (b * (f *' )) by Th14
.= (b " ) * ((a * f) - ((a * f) - (b * (f *' )))) by A44, POLYNOM3:29 ;
((a * f) - (b * (f *' ))) *' = ((a * f) *' ) + ((- (b * (f *' ))) *' ) by Th46
.= ((a * f) *' ) + (- ((b * (f *' )) *' )) by Th45
.= ((a *' ) * (f *' )) + (- ((b * (f *' )) *' )) by Th44
.= ((a *' ) * (f *' )) + (- ((b *' ) * ((f *' ) *' ))) by Th44
.= ((a *' ) * (f *' )) + (- ((b *' ) * f)) by Th43 ;
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:30 ;
A47: - (b9 *' ) = - (b *' ) by COMPLFLD:4;
A48: f = (1_ F_Complex ) * f by POLYNOM5:28
.= (((- ((- (b * zz)) " )) " ) * (- ((- (b * zz)) " ))) * f by A5, A29, A9, A30, A40, COMPLFLD:9, VECTSP_1:def 22
.= ((- ((- (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:29
.= (((- ((- (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 Lm4
.= (((- ((- (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:9
.= ((- (- (b * zz))) * (((a * f) - (b * (f *' ))) *' )) + (((a *' ) * zz) * ((a * f) - (b * (f *' )))) by A10, VECTSP_1:73
.= (- ((- (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:11;
|.(((|.a.| ^2 ) - (|.b.| ^2 )) " ).| > 0 by A42, COMPLEX1:133;
then A50: |.((a *' ) * zz).| > |.(- (b * zz)).| by A1, A22, A39, XREAL_1:70;
then |.((a *' ) * zz).| > 0 by COMPLEX1:132;
then (a *' ) * zz <> 0. F_Complex by COMPLEX1:133, COMPLFLD:9;
then deg f <= max (deg ((a * f) - (b * (f *' )))),(deg ((- (b * zz)) * (((a * f) - (b * (f *' ))) *' ))) by A49, POLYNOM5:26;
then deg f <= max (deg ((a * f) - (b * (f *' )))),(deg (((a * f) - (b * (f *' ))) *' )) by A43, POLYNOM5:26;
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

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

now

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 6
.= (eval (((a *' ) * zz) * ((a * f) - (b * (f *' )))),z) - (eval ((- (b * zz)) * (((a * f) - (b * (f *' ))) *' )),z) by POLYNOM4:24
.= (((a *' ) * zz) * (eval ((a * f) - (b * (f *' ))),z)) - (eval ((- (b * zz)) * (((a * f) - (b * (f *' ))) *' )),z) by POLYNOM5:31
.= (((a *' ) * zz) * (eval ((a * f) - (b * (f *' ))),z)) - ((- (b * zz)) * (eval (((a * f) - (b * (f *' ))) *' ),z)) by POLYNOM5:31 ;

now

A54: 0 <= |.(- (b * zz)).| by COMPLEX1:132;
A55: |.((a *' ) * zz).| * |.(eval ((a * f) - (b * (f *' ))),z).| = |.(((a *' ) * zz) * (eval ((a * f) - (b * (f *' ))),z)).| by COMPLEX1:151;
A56: |.(- (b * zz)).| * |.(eval (((a * f) - (b * (f *' ))) *' ),z).| = |.((- (b * zz)) * (eval (((a * f) - (b * (f *' ))) *' ),z)).| by COMPLEX1:151;
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, Th49;
|.(eval ((a * f) - (b * (f *' ))),z).| = |.(eval (((a * f) - (b * (f *' ))) *' ),z).| by A51, A52, A58, Th50;
then |.((a *' ) * zz).| * |.(eval ((a * f) - (b * (f *' ))),z).| > |.(- (b * zz)).| * |.(eval (((a * f) - (b * (f *' ))) *' ),z).| by A50, A59, XREAL_1:70;
hence contradiction by A53, A55, A56, VECTSP_1:66; :: 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, Th50;
then |.(eval ((a * f) - (b * (f *' ))),z).| > 0 by COMPLEX1:132;
then A61: |.((a *' ) * zz).| * |.(eval ((a * f) - (b * (f *' ))),z).| > |.(- (b * zz)).| * |.(eval ((a * f) - (b * (f *' ))),z).| by A50, XREAL_1:70;
|.(- (b * zz)).| * |.(eval ((a * f) - (b * (f *' ))),z).| >= |.(- (b * zz)).| * |.(eval (((a * f) - (b * (f *' ))) *' ),z).| by A54, A60, XREAL_1:66;
hence contradiction by A53, A55, A56, A61, VECTSP_1:66; :: thesis: verum

end;

end;

end;

hence Re z < 0 ; :: thesis: verum

end;

hence f is Hurwitz by Def8; :: thesis: verum

end;

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

end;

end;