let f be Polynomial of F_Complex ; :: thesis: ( deg f >= 1 & f is Hurwitz implies for x being Element of F_Complex holds
( ( Re x < 0 implies |.(eval f,x).| < |.(eval (f *' ),x).| ) & ( Re x > 0 implies |.(eval f,x).| > |.(eval (f *' ),x).| ) & ( Re x = 0 implies |.(eval f,x).| = |.(eval (f *' ),x).| ) ) )
assume A1: ( deg f >= 1 & f is Hurwitz ) ; :: thesis: for x being Element of F_Complex holds
( ( Re x < 0 implies |.(eval f,x).| < |.(eval (f *' ),x).| ) & ( Re x > 0 implies |.(eval f,x).| > |.(eval (f *' ),x).| ) & ( Re x = 0 implies |.(eval f,x).| = |.(eval (f *' ),x).| ) )
let x be Element of F_Complex ; :: thesis: ( ( Re x < 0 implies |.(eval f,x).| < |.(eval (f *' ),x).| ) & ( Re x > 0 implies |.(eval f,x).| > |.(eval (f *' ),x).| ) & ( Re x = 0 implies |.(eval f,x).| = |.(eval (f *' ),x).| ) )
defpred S₁[ Nat] means for f being Polynomial of F_Complex st deg f >= 1 & f is Hurwitz & deg f = $1 holds
for x being Element of F_Complex holds
( ( Re x < 0 implies |.(eval f,x).| < |.(eval (f *' ),x).| ) & ( Re x > 0 implies |.(eval f,x).| > |.(eval (f *' ),x).| ) & ( Re x = 0 implies |.(eval f,x).| = |.(eval (f *' ),x).| ) );
A2: S₁[ 0 ] ;

A3: now

let y, z be Element of F_Complex ; :: thesis: ( rpoly 1,z is Hurwitz & Re y < 0 implies |.(eval (rpoly 1,z),y).| < |.(eval ((rpoly 1,z) *' ),y).| )
assume A4: rpoly 1,z is Hurwitz ; :: thesis: ( Re y < 0 implies |.(eval (rpoly 1,z),y).| < |.(eval ((rpoly 1,z) *' ),y).| )
assume A5: Re y < 0 ; :: thesis: |.(eval (rpoly 1,z),y).| < |.(eval ((rpoly 1,z) *' ),y).|
z is_a_root_of rpoly 1,z by Th30;
then A6: Re z < 0 by A4, Def8;
reconsider y' = y, z' = z as Element of COMPLEX by COMPLFLD:def 1;
A7: ( - y = - y' & - z = - z' ) by COMPLFLD:4;
( y - z = eval (rpoly 1,z),y & eval ((rpoly 1,z) *' ),y = (- y) - (z *' ) ) by Th29, Th48;
then A8: ( y - z = eval (rpoly 1,z),y & eval ((rpoly 1,z) *' ),y = (- y') - (z' *' ) ) by A7, COMPLFLD:5;
( y = (Re y) + ((Im y) * <i> ) & z = (Re z) + ((Im z) * <i> ) ) by COMPLEX1:29;
then A9: |.(y' - z').| < |.(y' + (z' *' )).| by A5, A6, Lm15;
|.(y' + (z' *' )).| = |.(- (y' + (z' *' ))).| by COMPLEX1:138;
hence |.(eval (rpoly 1,z),y).| < |.(eval ((rpoly 1,z) *' ),y).| by A8, A9, COMPLFLD:5; :: thesis: verum

end;

A10: now

let a, y, z be Element of F_Complex ; :: thesis: ( rpoly 1,z is Hurwitz & a <> 0. F_Complex & Re y < 0 implies |.(eval (a * (rpoly 1,z)),y).| < |.(eval ((a * (rpoly 1,z)) *' ),y).| )
assume A11: ( rpoly 1,z is Hurwitz & a <> 0. F_Complex ) ; :: thesis: ( Re y < 0 implies |.(eval (a * (rpoly 1,z)),y).| < |.(eval ((a * (rpoly 1,z)) *' ),y).| )
assume A12: Re y < 0 ; :: thesis: |.(eval (a * (rpoly 1,z)),y).| < |.(eval ((a * (rpoly 1,z)) *' ),y).|
A13: |.a.| > 0 by A11, COMPLEX1:133, COMPLFLD:9;
A14: |.(eval (a * (rpoly 1,z)),y).| = |.(a * (eval (rpoly 1,z),y)).| by POLYNOM5:31
.= |.a.| * |.(eval (rpoly 1,z),y).| by COMPLEX1:151 ;
|.a.| * |.(eval ((rpoly 1,z) *' ),y).| = |.(a *' ).| * |.(eval ((rpoly 1,z) *' ),y).| by COMPLEX1:139
.= |.((a *' ) * (eval ((rpoly 1,z) *' ),y)).| by COMPLEX1:151
.= |.(eval ((a *' ) * ((rpoly 1,z) *' )),y).| by POLYNOM5:31
.= |.(eval ((a * (rpoly 1,z)) *' ),y).| by Th44 ;
hence |.(eval (a * (rpoly 1,z)),y).| < |.(eval ((a * (rpoly 1,z)) *' ),y).| by A3, A11, A12, A13, A14, XREAL_1:70; :: thesis: verum

end;

A15: now

let y, z be Element of F_Complex ; :: thesis: ( rpoly 1,z is Hurwitz & Re y > 0 implies |.(eval (rpoly 1,z),y).| > |.(eval ((rpoly 1,z) *' ),y).| )
assume A16: rpoly 1,z is Hurwitz ; :: thesis: ( Re y > 0 implies |.(eval (rpoly 1,z),y).| > |.(eval ((rpoly 1,z) *' ),y).| )
assume A17: Re y > 0 ; :: thesis: |.(eval (rpoly 1,z),y).| > |.(eval ((rpoly 1,z) *' ),y).|
z is_a_root_of rpoly 1,z by Th30;
then A18: Re z < 0 by A16, Def8;
reconsider y' = y, z' = z as Element of COMPLEX by COMPLFLD:def 1;
A19: ( - y = - y' & - z = - z' ) by COMPLFLD:4;
( y - z = eval (rpoly 1,z),y & eval ((rpoly 1,z) *' ),y = (- y) - (z *' ) ) by Th29, Th48;
then A20: ( y - z = eval (rpoly 1,z),y & eval ((rpoly 1,z) *' ),y = (- y') - (z' *' ) ) by A19, COMPLFLD:5;
( y = (Re y) + ((Im y) * <i> ) & z = (Re z) + ((Im z) * <i> ) ) by COMPLEX1:29;
then A21: |.(y' - z').| > |.(y' + (z' *' )).| by A17, A18, Lm15;
|.(y' + (z' *' )).| = |.(- (y' + (z' *' ))).| by COMPLEX1:138;
hence |.(eval (rpoly 1,z),y).| > |.(eval ((rpoly 1,z) *' ),y).| by A20, A21, COMPLFLD:5; :: thesis: verum

end;

A22: now

let a, y, z be Element of F_Complex ; :: thesis: ( rpoly 1,z is Hurwitz & a <> 0. F_Complex & Re y > 0 implies |.(eval (a * (rpoly 1,z)),y).| > |.(eval ((a * (rpoly 1,z)) *' ),y).| )
assume A23: ( rpoly 1,z is Hurwitz & a <> 0. F_Complex ) ; :: thesis: ( Re y > 0 implies |.(eval (a * (rpoly 1,z)),y).| > |.(eval ((a * (rpoly 1,z)) *' ),y).| )
assume A24: Re y > 0 ; :: thesis: |.(eval (a * (rpoly 1,z)),y).| > |.(eval ((a * (rpoly 1,z)) *' ),y).|
A25: |.a.| > 0 by A23, COMPLEX1:133, COMPLFLD:9;
A26: |.(eval (a * (rpoly 1,z)),y).| = |.(a * (eval (rpoly 1,z),y)).| by POLYNOM5:31
.= |.a.| * |.(eval (rpoly 1,z),y).| by COMPLEX1:151 ;
|.a.| * |.(eval ((rpoly 1,z) *' ),y).| = |.(a *' ).| * |.(eval ((rpoly 1,z) *' ),y).| by COMPLEX1:139
.= |.((a *' ) * (eval ((rpoly 1,z) *' ),y)).| by COMPLEX1:151
.= |.(eval ((a *' ) * ((rpoly 1,z) *' )),y).| by POLYNOM5:31
.= |.(eval ((a * (rpoly 1,z)) *' ),y).| by Th44 ;
hence |.(eval (a * (rpoly 1,z)),y).| > |.(eval ((a * (rpoly 1,z)) *' ),y).| by A15, A23, A24, A25, A26, XREAL_1:70; :: thesis: verum

end;

A27: now

let y, z be Element of F_Complex ; :: thesis: ( rpoly 1,z is Hurwitz & Re y = 0 implies |.(eval (rpoly 1,z),y).| = |.(eval ((rpoly 1,z) *' ),y).| )
assume A28: rpoly 1,z is Hurwitz ; :: thesis: ( Re y = 0 implies |.(eval (rpoly 1,z),y).| = |.(eval ((rpoly 1,z) *' ),y).| )
assume A29: Re y = 0 ; :: thesis: |.(eval (rpoly 1,z),y).| = |.(eval ((rpoly 1,z) *' ),y).|
z is_a_root_of rpoly 1,z by Th30;
then A30: Re z < 0 by A28, Def8;
reconsider y' = y, z' = z as Element of COMPLEX by COMPLFLD:def 1;
A31: ( - y = - y' & - z = - z' ) by COMPLFLD:4;
( y - z = eval (rpoly 1,z),y & eval ((rpoly 1,z) *' ),y = (- y) - (z *' ) ) by Th29, Th48;
then A32: ( y - z = eval (rpoly 1,z),y & eval ((rpoly 1,z) *' ),y = (- y') - (z' *' ) ) by A31, COMPLFLD:5;
( y = (Re y) + ((Im y) * <i> ) & z = (Re z) + ((Im z) * <i> ) ) by COMPLEX1:29;
then A33: |.(y' - z').| = |.(y' + (z' *' )).| by A29, A30, Lm15;
|.(y' + (z' *' )).| = |.(- (y' + (z' *' ))).| by COMPLEX1:138;
hence |.(eval (rpoly 1,z),y).| = |.(eval ((rpoly 1,z) *' ),y).| by A32, A33, COMPLFLD:5; :: thesis: verum

end;

A34: now

let a, y, z be Element of F_Complex ; :: thesis: ( rpoly 1,z is Hurwitz & a <> 0. F_Complex & Re y = 0 implies |.(eval (a * (rpoly 1,z)),y).| = |.(eval ((a * (rpoly 1,z)) *' ),y).| )
assume A35: ( rpoly 1,z is Hurwitz & a <> 0. F_Complex ) ; :: thesis: ( Re y = 0 implies |.(eval (a * (rpoly 1,z)),y).| = |.(eval ((a * (rpoly 1,z)) *' ),y).| )
assume A36: Re y = 0 ; :: thesis: |.(eval (a * (rpoly 1,z)),y).| = |.(eval ((a * (rpoly 1,z)) *' ),y).|
A37: |.(eval (a * (rpoly 1,z)),y).| = |.(a * (eval (rpoly 1,z),y)).| by POLYNOM5:31
.= |.a.| * |.(eval (rpoly 1,z),y).| by COMPLEX1:151 ;
|.a.| * |.(eval ((rpoly 1,z) *' ),y).| = |.(a *' ).| * |.(eval ((rpoly 1,z) *' ),y).| by COMPLEX1:139
.= |.((a *' ) * (eval ((rpoly 1,z) *' ),y)).| by COMPLEX1:151
.= |.(eval ((a *' ) * ((rpoly 1,z) *' )),y).| by POLYNOM5:31
.= |.(eval ((a * (rpoly 1,z)) *' ),y).| by Th44 ;
hence |.(eval (a * (rpoly 1,z)),y).| = |.(eval ((a * (rpoly 1,z)) *' ),y).| by A27, A35, A36, A37; :: thesis: verum

end;

A38: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A39: S₁[k] ; :: thesis: S₁[k + 1]

now

let f be Polynomial of F_Complex ; :: thesis: ( deg f >= 1 & f is Hurwitz & deg f = k + 1 implies for x being Element of F_Complex holds
( ( Re b₃ < 0 implies |.(eval b₂,b₃).| < |.(eval (b₂ *' ),b₃).| ) & ( Re b₃ > 0 implies |.(eval b₂,b₃).| > |.(eval (b₂ *' ),b₃).| ) & ( Re b₃ = 0 implies |.(eval b₂,b₃).| = |.(eval (b₂ *' ),b₃).| ) ) )
assume A40: ( deg f >= 1 & f is Hurwitz & deg f = k + 1 ) ; :: thesis: for x being Element of F_Complex holds
( ( Re b₃ < 0 implies |.(eval b₂,b₃).| < |.(eval (b₂ *' ),b₃).| ) & ( Re b₃ > 0 implies |.(eval b₂,b₃).| > |.(eval (b₂ *' ),b₃).| ) & ( Re b₃ = 0 implies |.(eval b₂,b₃).| = |.(eval (b₂ *' ),b₃).| ) )
let x be Element of F_Complex ; :: thesis: ( ( Re b₂ < 0 implies |.(eval b₁,b₂).| < |.(eval (b₁ *' ),b₂).| ) & ( Re b₂ > 0 implies |.(eval b₁,b₂).| > |.(eval (b₁ *' ),b₂).| ) & ( Re b₂ = 0 implies |.(eval b₁,b₂).| = |.(eval (b₁ *' ),b₂).| ) )

per cases ( k + 1 = 1 or k + 1 > 1 ) by A40, XXREAL_0:1;

suppose k + 1 = 1 ; :: thesis: ( ( Re b₂ < 0 implies |.(eval b₁,b₂).| < |.(eval (b₁ *' ),b₂).| ) & ( Re b₂ > 0 implies |.(eval b₁,b₂).| > |.(eval (b₁ *' ),b₂).| ) & ( Re b₂ = 0 implies |.(eval b₁,b₂).| = |.(eval (b₁ *' ),b₂).| ) )

then consider z1, z2 being Element of F_Complex such that
A41: ( z1 <> 0. F_Complex & f = z1 * (rpoly 1,z2) ) by A40, Th28;
rpoly 1,z2 is Hurwitz by A40, A41, Th40;
hence ( ( Re x < 0 implies |.(eval f,x).| < |.(eval (f *' ),x).| ) & ( Re x > 0 implies |.(eval f,x).| > |.(eval (f *' ),x).| ) & ( Re x = 0 implies |.(eval f,x).| = |.(eval (f *' ),x).| ) ) by A10, A22, A34, A41; :: thesis: verum

end;

suppose A42: k + 1 > 1 ; :: thesis: ( ( Re b₂ < 0 implies |.(eval b₁,b₂).| < |.(eval (b₁ *' ),b₂).| ) & ( Re b₂ > 0 implies |.(eval b₁,b₂).| > |.(eval (b₁ *' ),b₂).| ) & ( Re b₂ = 0 implies |.(eval b₁,b₂).| = |.(eval (b₁ *' ),b₂).| ) )

A43: (k + 1) + 1 > (k + 1) + 0 by XREAL_1:8;
then len f > 1 by A40, XXREAL_0:2;
then f is with_roots by POLYNOM5:75;
then consider z being Element of F_Complex such that
A44: z is_a_root_of f by POLYNOM5:def 7;
consider f1 being Polynomial of F_Complex such that
A45: f = (rpoly 1,z) *' f1 by A44, Th33;
A46: f <> 0_. F_Complex by A40, A43, POLYNOM4:6;
then A47: rpoly 1,z <> 0_. F_Complex by A45, POLYNOM3:35;
f1 <> 0_. F_Complex by A45, A46, POLYNOM3:35;
then A48: deg f = (deg (rpoly 1,z)) + (deg f1) by A45, A47, Th23
.= 1 + (deg f1) by Th27 ;
A49: ( f1 is Hurwitz & rpoly 1,z is Hurwitz ) by A40, A45, Th41;
A50: k >= 1 by A42, NAT_1:13;

A51: now

assume A52: Re x < 0 ; :: thesis: |.(eval f,x).| < |.(eval (f *' ),x).|
reconsider r' = eval (rpoly 1,z),x, e' = eval f1,x as Element of COMPLEX by COMPLFLD:def 1;
reconsider r1' = eval ((rpoly 1,z) *' ),x, e1' = eval (f1 *' ),x as Element of COMPLEX by COMPLFLD:def 1;
A53: ( |.e'.| < |.e1'.| & |.r'.| < |.r1'.| ) by A3, A39, A40, A48, A49, A50, A52;
A54: ( 0 <= |.e'.| & 0 <= |.r'.| ) by COMPLEX1:132;
then A55: |.r1'.| * |.e'.| < |.r1'.| * |.e1'.| by A53, XREAL_1:70;
|.r'.| * |.e'.| <= |.r1'.| * |.e'.| by A53, A54, XREAL_1:66;
then |.r'.| * |.e'.| < |.r1'.| * |.e1'.| by A55, XXREAL_0:2;
then |.(r' * e').| < |.r1'.| * |.e1'.| by COMPLEX1:151;
then A56: |.((eval (rpoly 1,z),x) * (eval f1,x)).| < |.((eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x)).| by COMPLEX1:151;
( (eval (rpoly 1,z),x) * (eval f1,x) = eval ((rpoly 1,z) *' f1),x & (eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x) = eval (((rpoly 1,z) *' ) *' (f1 *' )),x ) by POLYNOM4:27;
hence |.(eval f,x).| < |.(eval (f *' ),x).| by A45, A56, Th47; :: thesis: verum

end;

A57: now

assume A58: Re x > 0 ; :: thesis: |.(eval f,x).| > |.(eval (f *' ),x).|
reconsider r' = eval (rpoly 1,z),x, e' = eval f1,x as Element of COMPLEX by COMPLFLD:def 1;
reconsider r1' = eval ((rpoly 1,z) *' ),x, e1' = eval (f1 *' ),x as Element of COMPLEX by COMPLFLD:def 1;
A59: ( |.e'.| > |.e1'.| & |.r'.| > |.r1'.| ) by A15, A39, A40, A48, A49, A50, A58;
A60: ( 0 <= |.e1'.| & 0 <= |.r1'.| ) by COMPLEX1:132;
then A61: |.r'.| * |.e'.| > |.r1'.| * |.e'.| by A59, XREAL_1:70;
|.r1'.| * |.e'.| >= |.r1'.| * |.e1'.| by A59, A60, XREAL_1:66;
then |.r'.| * |.e'.| > |.r1'.| * |.e1'.| by A61, XXREAL_0:2;
then |.(r' * e').| > |.r1'.| * |.e1'.| by COMPLEX1:151;
then A62: |.((eval (rpoly 1,z),x) * (eval f1,x)).| > |.((eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x)).| by COMPLEX1:151;
( (eval (rpoly 1,z),x) * (eval f1,x) = eval ((rpoly 1,z) *' f1),x & (eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x) = eval (((rpoly 1,z) *' ) *' (f1 *' )),x ) by POLYNOM4:27;
hence |.(eval f,x).| > |.(eval (f *' ),x).| by A45, A62, Th47; :: thesis: verum

end;

now

assume A63: Re x = 0 ; :: thesis: |.(eval f,x).| = |.(eval (f *' ),x).|
then A64: |.(eval f1,x).| = |.(eval (f1 *' ),x).| by A39, A40, A48, A49, A50;
reconsider r' = eval (rpoly 1,z),x, e' = eval f1,x as Element of COMPLEX by COMPLFLD:def 1;
reconsider r1' = eval ((rpoly 1,z) *' ),x, e1' = eval (f1 *' ),x as Element of COMPLEX by COMPLFLD:def 1;
|.r'.| * |.e'.| = |.r1'.| * |.e1'.| by A27, A49, A63, A64;
then |.(r' * e').| = |.r1'.| * |.e1'.| by COMPLEX1:151;
then A65: |.((eval (rpoly 1,z),x) * (eval f1,x)).| = |.((eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x)).| by COMPLEX1:151;
( (eval (rpoly 1,z),x) * (eval f1,x) = eval ((rpoly 1,z) *' f1),x & (eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x) = eval (((rpoly 1,z) *' ) *' (f1 *' )),x ) by POLYNOM4:27;
hence |.(eval f,x).| = |.(eval (f *' ),x).| by A45, A65, Th47; :: thesis: verum

end;

hence ( ( Re x < 0 implies |.(eval f,x).| < |.(eval (f *' ),x).| ) & ( Re x > 0 implies |.(eval f,x).| > |.(eval (f *' ),x).| ) & ( Re x = 0 implies |.(eval f,x).| = |.(eval (f *' ),x).| ) ) by A51, A57; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A66: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A38);
f <> 0_. F_Complex by A1, Th20;
then deg f is Element of NAT by Lm9;
then consider j being Element of NAT such that
A67: deg f = j ;
thus ( ( Re x < 0 implies |.(eval f,x).| < |.(eval (f *' ),x).| ) & ( Re x > 0 implies |.(eval f,x).| > |.(eval (f *' ),x).| ) & ( Re x = 0 implies |.(eval f,x).| = |.(eval (f *' ),x).| ) ) by A1, A66, A67; :: thesis: verum