A1: 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 A2: rpoly 1,z is Hurwitz ; :: thesis: ( Re y > 0 implies |.(eval (rpoly 1,z),y).| > |.(eval ((rpoly 1,z) *' ),y).| )
z is_a_root_of rpoly 1,z by Th30;
then A3: Re z < 0 by A2, Def8;
A4: y = (Re y) + ((Im y) * <i> ) by COMPLEX1:29;
A5: y - z = eval (rpoly 1,z),y by Th29;
A6: z = (Re z) + ((Im z) * <i> ) by COMPLEX1:29;
reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;
A7: - y = - y9 by COMPLFLD:4;
eval ((rpoly 1,z) *' ),y = (- y) - (z *' ) by Th48;
then A8: eval ((rpoly 1,z) *' ),y = (- y9) - (z9 *' ) by A7, COMPLFLD:5;
A9: |.(y9 + (z9 *' )).| = |.(- (y9 + (z9 *' ))).| by COMPLEX1:138;
assume Re y > 0 ; :: thesis: |.(eval (rpoly 1,z),y).| > |.(eval ((rpoly 1,z) *' ),y).|
then |.(y9 - z9).| > |.(y9 + (z9 *' )).| by A3, A4, A6, Lm15;
hence |.(eval (rpoly 1,z),y).| > |.(eval ((rpoly 1,z) *' ),y).| by A5, 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 that
A11: rpoly 1,z is Hurwitz and
A12: a <> 0. F_Complex ; :: thesis: ( Re y > 0 implies |.(eval (a * (rpoly 1,z)),y).| > |.(eval ((a * (rpoly 1,z)) *' ),y).| )
assume A13: Re y > 0 ; :: thesis: |.(eval (a * (rpoly 1,z)),y).| > |.(eval ((a * (rpoly 1,z)) *' ),y).|
A14: |.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 ;
A15: |.(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.| > 0 by A12, COMPLEX1:133, COMPLFLD:9;
hence |.(eval (a * (rpoly 1,z)),y).| > |.(eval ((a * (rpoly 1,z)) *' ),y).| by A1, A11, A13, A15, A14, XREAL_1:70; :: thesis: verum

end;

A16: 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 A17: rpoly 1,z is Hurwitz ; :: thesis: ( Re y < 0 implies |.(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 A17, Def8;
A19: y = (Re y) + ((Im y) * <i> ) by COMPLEX1:29;
A20: y - z = eval (rpoly 1,z),y by Th29;
A21: z = (Re z) + ((Im z) * <i> ) by COMPLEX1:29;
reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;
A22: - y = - y9 by COMPLFLD:4;
eval ((rpoly 1,z) *' ),y = (- y) - (z *' ) by Th48;
then A23: eval ((rpoly 1,z) *' ),y = (- y9) - (z9 *' ) by A22, COMPLFLD:5;
A24: |.(y9 + (z9 *' )).| = |.(- (y9 + (z9 *' ))).| by COMPLEX1:138;
assume Re y < 0 ; :: thesis: |.(eval (rpoly 1,z),y).| < |.(eval ((rpoly 1,z) *' ),y).|
then |.(y9 - z9).| < |.(y9 + (z9 *' )).| by A18, A19, A21, Lm15;
hence |.(eval (rpoly 1,z),y).| < |.(eval ((rpoly 1,z) *' ),y).| by A20, A23, A24, COMPLFLD:5; :: thesis: verum

end;

A25: 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 that
A26: rpoly 1,z is Hurwitz and
A27: a <> 0. F_Complex ; :: thesis: ( Re y < 0 implies |.(eval (a * (rpoly 1,z)),y).| < |.(eval ((a * (rpoly 1,z)) *' ),y).| )
assume A28: Re y < 0 ; :: thesis: |.(eval (a * (rpoly 1,z)),y).| < |.(eval ((a * (rpoly 1,z)) *' ),y).|
A29: |.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 ;
A30: |.(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.| > 0 by A27, COMPLEX1:133, COMPLFLD:9;
hence |.(eval (a * (rpoly 1,z)),y).| < |.(eval ((a * (rpoly 1,z)) *' ),y).| by A16, A26, A28, A30, A29, XREAL_1:70; :: thesis: verum

end;

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).| ) );
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 that
A31: deg f >= 1 and
A32: 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).| ) )

A33: 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 A34: rpoly 1,z is Hurwitz ; :: thesis: ( Re y = 0 implies |.(eval (rpoly 1,z),y).| = |.(eval ((rpoly 1,z) *' ),y).| )
z is_a_root_of rpoly 1,z by Th30;
then A35: Re z < 0 by A34, Def8;
A36: y = (Re y) + ((Im y) * <i> ) by COMPLEX1:29;
A37: y - z = eval (rpoly 1,z),y by Th29;
A38: z = (Re z) + ((Im z) * <i> ) by COMPLEX1:29;
reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;
A39: - y = - y9 by COMPLFLD:4;
eval ((rpoly 1,z) *' ),y = (- y) - (z *' ) by Th48;
then A40: eval ((rpoly 1,z) *' ),y = (- y9) - (z9 *' ) by A39, COMPLFLD:5;
A41: |.(y9 + (z9 *' )).| = |.(- (y9 + (z9 *' ))).| by COMPLEX1:138;
assume Re y = 0 ; :: thesis: |.(eval (rpoly 1,z),y).| = |.(eval ((rpoly 1,z) *' ),y).|
then |.(y9 - z9).| = |.(y9 + (z9 *' )).| by A35, A36, A38, Lm15;
hence |.(eval (rpoly 1,z),y).| = |.(eval ((rpoly 1,z) *' ),y).| by A37, A40, A41, COMPLFLD:5; :: thesis: verum

end;

A42: 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 that
A43: rpoly 1,z is Hurwitz and
a <> 0. F_Complex ; :: thesis: ( Re y = 0 implies |.(eval (a * (rpoly 1,z)),y).| = |.(eval ((a * (rpoly 1,z)) *' ),y).| )
A44: |.(eval (a * (rpoly 1,z)),y).| = |.(a * (eval (rpoly 1,z),y)).| by POLYNOM5:31
.= |.a.| * |.(eval (rpoly 1,z),y).| by COMPLEX1:151 ;
A45: |.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 ;
assume Re y = 0 ; :: thesis: |.(eval (a * (rpoly 1,z)),y).| = |.(eval ((a * (rpoly 1,z)) *' ),y).|
hence |.(eval (a * (rpoly 1,z)),y).| = |.(eval ((a * (rpoly 1,z)) *' ),y).| by A33, A43, A44, A45; :: thesis: verum

end;

A46: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A47: 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 that
A48: deg f >= 1 and
A49: f is Hurwitz and
A50: 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 A48, A50, 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
A51: z1 <> 0. F_Complex and
A52: f = z1 * (rpoly 1,z2) by A50, Th28;
rpoly 1,z2 is Hurwitz by A49, A51, A52, 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 A25, A10, A42, A51, A52; :: thesis: verum

end;

suppose A53: 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₂).| ) )

A54: (k + 1) + 1 > (k + 1) + 0 by XREAL_1:8;
then A55: f <> 0_. F_Complex by A50, POLYNOM4:6;
len f > 1 by A48, A50, A54, XXREAL_0:2;
then f is with_roots by POLYNOM5:75;
then consider z being Element of F_Complex such that
A56: z is_a_root_of f by POLYNOM5:def 7;
consider f1 being Polynomial of F_Complex such that
A57: f = (rpoly 1,z) *' f1 by A56, Th33;
A58: f1 <> 0_. F_Complex by A57, A55, POLYNOM3:35;
rpoly 1,z <> 0_. F_Complex by A57, A55, POLYNOM3:35;
then A59: deg f = (deg (rpoly 1,z)) + (deg f1) by A57, A58, Th23
.= 1 + (deg f1) by Th27 ;
A60: rpoly 1,z is Hurwitz by A49, A57, Th41;
A61: f1 is Hurwitz by A49, A57, Th41;
A62: k >= 1 by A53, NAT_1:13;

A63: now

reconsider r19 = eval ((rpoly 1,z) *' ),x, e19 = eval (f1 *' ),x as Element of COMPLEX by COMPLFLD:def 1;
reconsider r9 = eval (rpoly 1,z),x, e9 = eval f1,x as Element of COMPLEX by COMPLFLD:def 1;
A64: (eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x) = eval (((rpoly 1,z) *' ) *' (f1 *' )),x by POLYNOM4:27;
assume A65: Re x > 0 ; :: thesis: |.(eval f,x).| > |.(eval (f *' ),x).|
then A66: |.e9.| > |.e19.| by A47, A50, A59, A61, A62;
0 <= |.r19.| by COMPLEX1:132;
then A67: |.r19.| * |.e9.| >= |.r19.| * |.e19.| by A66, XREAL_1:66;
0 <= |.e19.| by COMPLEX1:132;
then |.r9.| * |.e9.| > |.r19.| * |.e9.| by A1, A60, A65, A66, XREAL_1:70;
then |.r9.| * |.e9.| > |.r19.| * |.e19.| by A67, XXREAL_0:2;
then |.(r9 * e9).| > |.r19.| * |.e19.| by COMPLEX1:151;
then A68: |.((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 by POLYNOM4:27;
hence |.(eval f,x).| > |.(eval (f *' ),x).| by A57, A68, A64, Th47; :: thesis: verum

end;

A69: now

reconsider r19 = eval ((rpoly 1,z) *' ),x, e19 = eval (f1 *' ),x as Element of COMPLEX by COMPLFLD:def 1;
reconsider r9 = eval (rpoly 1,z),x, e9 = eval f1,x as Element of COMPLEX by COMPLFLD:def 1;
A70: 0 <= |.r9.| by COMPLEX1:132;
assume A71: Re x < 0 ; :: thesis: |.(eval f,x).| < |.(eval (f *' ),x).|
then A72: |.r9.| < |.r19.| by A16, A60;
0 <= |.e9.| by COMPLEX1:132;
then A73: |.r9.| * |.e9.| <= |.r19.| * |.e9.| by A72, XREAL_1:66;
|.e9.| < |.e19.| by A47, A50, A59, A61, A62, A71;
then |.r19.| * |.e9.| < |.r19.| * |.e19.| by A72, A70, XREAL_1:70;
then |.r9.| * |.e9.| < |.r19.| * |.e19.| by A73, XXREAL_0:2;
then |.(r9 * e9).| < |.r19.| * |.e19.| by COMPLEX1:151;
then A74: |.((eval (rpoly 1,z),x) * (eval f1,x)).| < |.((eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x)).| by COMPLEX1:151;
A75: (eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x) = eval (((rpoly 1,z) *' ) *' (f1 *' )),x by POLYNOM4:27;
(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 A57, A74, A75, Th47; :: thesis: verum

end;

now

reconsider r19 = eval ((rpoly 1,z) *' ),x, e19 = eval (f1 *' ),x as Element of COMPLEX by COMPLFLD:def 1;
reconsider r9 = eval (rpoly 1,z),x, e9 = eval f1,x as Element of COMPLEX by COMPLFLD:def 1;
A76: (eval ((rpoly 1,z) *' ),x) * (eval (f1 *' ),x) = eval (((rpoly 1,z) *' ) *' (f1 *' )),x by POLYNOM4:27;
assume A77: Re x = 0 ; :: thesis: |.(eval f,x).| = |.(eval (f *' ),x).|
then |.(eval f1,x).| = |.(eval (f1 *' ),x).| by A47, A50, A59, A61, A62;
then |.r9.| * |.e9.| = |.r19.| * |.e19.| by A33, A60, A77;
then |.(r9 * e9).| = |.r19.| * |.e19.| by COMPLEX1:151;
then A78: |.((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 by POLYNOM4:27;
hence |.(eval f,x).| = |.(eval (f *' ),x).| by A57, A78, A76, 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 A69, A63; :: thesis: verum

end;

end;

end;

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

end;

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).| ) )
A79: S₁[ 0 ] ;
A80: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A79, A46);
f <> 0_. F_Complex by A31, Th20;
then deg f is Element of NAT by Lm9;
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 A31, A32, A80; :: thesis: verum