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 )
let f be Polynomial of F_Complex ; :: thesis: ( deg f >= 1 implies ( f is Hurwitz iff (a * f) - (b * (f *' )) is Hurwitz ) )
assume A2: deg f >= 1 ; :: thesis: ( f is Hurwitz iff (a * f) - (b * (f *' )) is Hurwitz )
set g = (a * f) - (b * (f *' ));
A3: 0 < |.a.| by A1, COMPLEX1:132;
then A4: a <> 0. F_Complex by COMPLEX1:133, COMPLFLD:9;

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 A4, Th40; :: thesis: verum

end;

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

then A6: 0 < |.b.| by COMPLEX1:133, COMPLFLD:9;

A7: now

assume A8: 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 A9: 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

assume A10: Re z >= 0 ; :: thesis: contradiction
A11: |.a.| * |.(eval f,z).| = |.(a * (eval f,z)).| by COMPLEX1:151;
A12: |.b.| * |.(eval (f *' ),z).| = |.(b * (eval (f *' ),z)).| by COMPLEX1:151;
A13: 0 <= |.b.| by COMPLEX1:132;

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

suppose Re z = 0 ; :: thesis: contradiction

then ( |.(eval f,z).| = |.(eval (f *' ),z).| & |.(eval f,z).| > 0 ) by A2, A8, Th49, Th50;
then |.a.| * |.(eval f,z).| > |.b.| * |.(eval (f *' ),z).| by A1, XREAL_1:70;
hence contradiction by A9, A11, A12, VECTSP_1:66; :: thesis: verum

end;

suppose Re z > 0 ; :: thesis: contradiction

then A14: |.(eval f,z).| > |.(eval (f *' ),z).| by A2, A8, Th50;
then |.(eval f,z).| > 0 by COMPLEX1:132;
then A15: |.a.| * |.(eval f,z).| > |.b.| * |.(eval f,z).| by A1, XREAL_1:70;
|.b.| * |.(eval f,z).| >= |.b.| * |.(eval (f *' ),z).| by A13, A14, XREAL_1:66;
hence contradiction by A9, A11, A12, A15, 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;

A16: ((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 ;
reconsider a' = a, b' = 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 a1' = (a *' ) * zz, b1' = - (b * zz) as Element of COMPLEX by COMPLFLD:def 1;

A17: now

let z be Element of COMPLEX ; :: thesis: (z *' ) * z = |.z.| ^2
A18: ( Re (z * (z *' )) = ((Re z) ^2 ) + ((Im z) ^2 ) & Im (z * (z *' )) = 0 ) by COMPLEX1:126;
A19: (Re (z * (z *' ))) + ((Im (z * (z *' ))) * <i> ) = z * (z *' ) by COMPLEX1:29;
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:65;
then ((Re z) ^2 ) + ((Im z) ^2 ) >= 0 + 0 ;
hence (z *' ) * z = |.z.| ^2 by A18, A19, SQUARE_1:def 4; :: thesis: verum

end;

then A20: ( (b' *' ) * b' = |.b'.| ^2 & (a' *' ) * a' = |.a'.| ^2 ) ;
A21: (((a' *' ) * a') * (b' " )) - (b' *' ) = (((|.a'.| ^2 ) * (b' " )) - (b' *' )) * 1 by A17
.= (((|.a'.| ^2 ) * (b' " )) - (b' *' )) * (b' * (b' " )) by A5, COMPLFLD:9, XCMPLX_0:def 7
.= (((|.a'.| ^2 ) * ((b' " ) * b')) - (|.b'.| ^2 )) * (b' " ) by A20
.= (((|.a'.| ^2 ) * 1) - (|.b'.| ^2 )) * (b' " ) by A5, COMPLFLD:9, XCMPLX_0:def 7 ;
(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 A22: (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 ;
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 A22, POLYNOM3:29 ;
then ((a * f) - (b * (f *' ))) *' = ((a *' ) * (((b " ) * (a * f)) + ((b " ) * (- ((a * f) - (b * (f *' ))))))) + (- ((b *' ) * f)) by A16, 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 A23: (((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 ;
b' " = b " by A5, COMPLFLD:7;
then A24: (((a' *' ) * a') * (b' " )) - (b' *' ) = (((a *' ) * a) * (b " )) - (b *' ) by COMPLFLD:5;
|.a'.| * |.b'.| > |.b'.| * |.b'.| by A1, A6, XREAL_1:70;
then A25: (|.a'.| ^2 ) - (|.b'.| ^2 ) <> 0 by A1, A3, XREAL_1:70;
then A26: ((|.a'.| ^2 ) - (|.b'.| ^2 )) " <> 0 ;
b' " <> 0 by A5, COMPLFLD:9;
then A27: ((a *' ) * ((b " ) * a)) + (- (b *' )) <> 0. F_Complex by A21, A24, A25, COMPLFLD:9, RLVECT_1:def 12;
b1' = - (b' * (((|.a.| ^2 ) - (|.b.| ^2 )) " )) by COMPLFLD:4
.= (- b') * (((|.a.| ^2 ) - (|.b.| ^2 )) " ) ;
then A28: b1' <> 0 by A5, A26, COMPLFLD:9;

A29: now

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

end;

A30: now

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

end;

A32: now

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

end;

A33: b1' = - (b' * (((|.a.| ^2 ) - (|.b.| ^2 )) " )) by COMPLFLD:4;
A34: - (((((a' *' ) * a') * (b' " )) - (b' *' )) " ) = - ((((|.a'.| ^2 ) - (|.b'.| ^2 )) " ) * ((b' " ) " )) by A21, XCMPLX_1:205
.= b1' by COMPLFLD:4 ;
A35: (a' *' ) * ((b' " ) * a') = (a *' ) * ((b " ) * a) by A5, COMPLFLD:7;
A36: - (b' *' ) = - (b *' ) by COMPLFLD:4;
- (- (b * zz)) = - b1' by COMPLFLD:4;
then A37: (- b1') " = (- (- (b * zz))) " by A29, COMPLFLD:7
.= - ((- (b * zz)) " ) by A28, Th1, COMPLFLD:9 ;
A38: (- ((- (b * zz)) " )) " = - (((- (b * zz)) " ) " ) by A30, Th1
.= - (- (b * zz)) by A28, COMPLFLD:9, VECTSP_1:73 ;
(- (b * zz)) " = b1' " by A28, COMPLFLD:7, COMPLFLD:9;
then - ((- (b * zz)) " ) = - (b1' " ) by COMPLFLD:4;
then (- ((- (b * zz)) " )) " = (- (b1' " )) " by A32, COMPLFLD:7;
then A39: ((- (b1' " )) " ) * ((a' *' ) * (b' " )) = (- (- (b' * (((|.a.| ^2 ) - (|.b.| ^2 )) " )))) * ((a' *' ) * (b' " )) by A33, A38, COMPLFLD:4
.= ((b' * (b' " )) * (((|.a.| ^2 ) - (|.b.| ^2 )) " )) * (a' *' )
.= (1 * (((|.a.| ^2 ) - (|.b.| ^2 )) " )) * (a' *' ) by A5, COMPLFLD:9, XCMPLX_0:def 7
.= a1' ;
A40: (a *' ) * (b " ) = (a' *' ) * (b' " ) by A5, COMPLFLD:7;
(- (b * zz)) " = b1' " by A28, COMPLFLD:7, COMPLFLD:9;
then - ((- (b * zz)) " ) = - (b1' " ) by COMPLFLD:4;
then A41: ((- ((- (b * zz)) " )) " ) * ((a *' ) * (b " )) = (a *' ) * zz by A32, A39, A40, COMPLFLD:7;
A42: f = (1_ F_Complex ) * f by POLYNOM5:28
.= (((- ((- (b * zz)) " )) " ) * (- ((- (b * zz)) " ))) * f by A27, A34, A35, A36, A37, VECTSP_1:def 22
.= ((- ((- (b * zz)) " )) " ) * ((- ((- (b * zz)) " )) * f) by Th14
.= ((- ((- (b * zz)) " )) " ) * ((((a * f) - (b * (f *' ))) *' ) + (- (((a *' ) * (b " )) * (- ((a * f) - (b * (f *' ))))))) by A23, A34, A35, A36, A37, 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 A41, Th14
.= ((((- (- (b * zz))) " ) " ) * (((a * f) - (b * (f *' ))) *' )) + (((a *' ) * zz) * ((a * f) - (b * (f *' )))) by A28, Th1, COMPLFLD:9
.= ((- (- (b * zz))) * (((a * f) - (b * (f *' ))) *' )) + (((a *' ) * zz) * ((a * f) - (b * (f *' )))) by A29, VECTSP_1:73
.= (- ((- (b * zz)) * (((a * f) - (b * (f *' ))) *' ))) + (((a *' ) * zz) * ((a * f) - (b * (f *' )))) by Th15 ;
A43: |.((a *' ) * zz).| = |.(a *' ).| * |.(((|.a.| ^2 ) - (|.b.| ^2 )) " ).| by COMPLEX1:151
.= |.a.| * |.(((|.a.| ^2 ) - (|.b.| ^2 )) " ).| by COMPLEX1:139 ;
A44: |.(- (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 ;
A45: |.a.| * |.a.| > |.b.| * |.a.| by A1, A3, XREAL_1:70;
|.b.| * |.a.| > |.b.| * |.b.| by A1, A6, XREAL_1:70;
then |.a.| ^2 > |.b.| * |.b.| by A45, XXREAL_0:2;
then (|.a.| ^2 ) - (|.b.| ^2 ) > (|.b.| ^2 ) - (|.b.| ^2 ) by XREAL_1:11;
then A46: ((|.a.| ^2 ) - (|.b.| ^2 )) " > 0 ;
then |.(((|.a.| ^2 ) - (|.b.| ^2 )) " ).| > 0 by COMPLEX1:133;
then A47: |.((a *' ) * zz).| > |.(- (b * zz)).| by A1, A43, A44, XREAL_1:70;

A48: now

assume b1' = 0. F_Complex ; :: thesis: contradiction
then (- b) * zz = 0. F_Complex by VECTSP_1:41;
then - b = 0. F_Complex by A46, COMPLFLD:9;
then b = - (0. F_Complex ) by RLVECT_1:30;
hence contradiction by A5, RLVECT_1:25; :: thesis: verum

end;

|.((a *' ) * zz).| > 0 by A47, COMPLEX1:132;
then A49: ( (a *' ) * zz <> 0. F_Complex & - (b * zz) <> 0. F_Complex ) by A48, COMPLEX1:133, COMPLFLD:9;
deg f <= max (deg (((a *' ) * zz) * ((a * f) - (b * (f *' ))))),(deg (- ((- (b * zz)) * (((a * f) - (b * (f *' ))) *' )))) by A42, Th22;
then deg f <= max (deg (((a *' ) * zz) * ((a * f) - (b * (f *' ))))),(deg ((- (b * zz)) * (((a * f) - (b * (f *' ))) *' ))) by POLYNOM4:11;
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 A48, POLYNOM5:26;
then deg f <= max (deg ((a * f) - (b * (f *' )))),(deg ((a * f) - (b * (f *' )))) by Th42;
then A50: deg ((a * f) - (b * (f *' ))) >= 1 by A2, XXREAL_0:2;

now

assume A51: (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 A52: 0. F_Complex = eval ((((a *' ) * zz) * ((a * f) - (b * (f *' )))) - ((- (b * zz)) * (((a * f) - (b * (f *' ))) *' ))),z by A42, 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

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

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

suppose Re z = 0 ; :: thesis: contradiction

then ( |.(eval ((a * f) - (b * (f *' ))),z).| = |.(eval (((a * f) - (b * (f *' ))) *' ),z).| & |.(eval ((a * f) - (b * (f *' ))),z).| > 0 ) by A50, A51, Th49, Th50;
then |.((a *' ) * zz).| * |.(eval ((a * f) - (b * (f *' ))),z).| > |.(- (b * zz)).| * |.(eval (((a * f) - (b * (f *' ))) *' ),z).| by A47, XREAL_1:70;
hence contradiction by A52, A54, A55, VECTSP_1:66; :: thesis: verum

end;

suppose Re z > 0 ; :: thesis: contradiction

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

end;

end;