A1: now :: thesis: for y, z being Element of F_Complex st rpoly (1,z) is Hurwitz & Re y > 0 holds
|.(eval ((rpoly (1,z)),y)).| > |.(eval (((rpoly (1,z)) *'),y)).|
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;
A4: y = (Re y) + ((Im y) * <i>) by COMPLEX1:13;
A5: y - z = eval ((rpoly (1,z)),y) by Th29;
A6: z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;
A7: - y = - y9 by COMPLFLD:2;
eval (((rpoly (1,z)) *'),y) = (- y) - (z *') by Th47;
then A8: eval (((rpoly (1,z)) *'),y) = (- y9) - (z9 *') by A7, COMPLFLD:3;
A9: |.(y9 + (z9 *')).| = |.(- (y9 + (z9 *'))).| by COMPLEX1:52;
assume Re y > 0 ; :: thesis: |.(eval ((rpoly (1,z)),y)).| > |.(eval (((rpoly (1,z)) *'),y)).|
then |.(y9 - z9).| > |.(y9 + (z9 *')).| by A3, A4, A6, Lm14;
hence |.(eval ((rpoly (1,z)),y)).| > |.(eval (((rpoly (1,z)) *'),y)).| by A5, A8, A9, COMPLFLD:3; :: thesis: verum
end;
A10: now :: thesis: for a, y, z being Element of F_Complex st rpoly (1,z) is Hurwitz & a <> 0. F_Complex & Re y > 0 holds
|.(eval ((a * (rpoly (1,z))),y)).| > |.(eval (((a * (rpoly (1,z))) *'),y)).|
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:53
.= |.((a *') * (eval (((rpoly (1,z)) *'),y))).| by COMPLEX1:65
.= |.(eval (((a *') * ((rpoly (1,z)) *')),y)).| by POLYNOM5:30
.= |.(eval (((a * (rpoly (1,z))) *'),y)).| by Th43 ;
A15: |.(eval ((a * (rpoly (1,z))),y)).| = |.(a * (eval ((rpoly (1,z)),y))).| by POLYNOM5:30
.= |.a.| * |.(eval ((rpoly (1,z)),y)).| by COMPLEX1:65 ;
|.a.| > 0 by A12, COMPLEX1:47, COMPLFLD:7;
hence |.(eval ((a * (rpoly (1,z))),y)).| > |.(eval (((a * (rpoly (1,z))) *'),y)).| by A1, A11, A13, A15, A14, XREAL_1:68; :: thesis: verum
end;
A16: now :: thesis: for y, z being Element of F_Complex st rpoly (1,z) is Hurwitz & Re y < 0 holds
|.(eval ((rpoly (1,z)),y)).| < |.(eval (((rpoly (1,z)) *'),y)).|
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;
A19: y = (Re y) + ((Im y) * <i>) by COMPLEX1:13;
A20: y - z = eval ((rpoly (1,z)),y) by Th29;
A21: z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;
A22: - y = - y9 by COMPLFLD:2;
eval (((rpoly (1,z)) *'),y) = (- y) - (z *') by Th47;
then A23: eval (((rpoly (1,z)) *'),y) = (- y9) - (z9 *') by A22, COMPLFLD:3;
A24: |.(y9 + (z9 *')).| = |.(- (y9 + (z9 *'))).| by COMPLEX1:52;
assume Re y < 0 ; :: thesis: |.(eval ((rpoly (1,z)),y)).| < |.(eval (((rpoly (1,z)) *'),y)).|
then |.(y9 - z9).| < |.(y9 + (z9 *')).| by A18, A19, A21, Lm14;
hence |.(eval ((rpoly (1,z)),y)).| < |.(eval (((rpoly (1,z)) *'),y)).| by A20, A23, A24, COMPLFLD:3; :: thesis: verum
end;
A25: now :: thesis: for a, y, z being Element of F_Complex st rpoly (1,z) is Hurwitz & a <> 0. F_Complex & Re y < 0 holds
|.(eval ((a * (rpoly (1,z))),y)).| < |.(eval (((a * (rpoly (1,z))) *'),y)).|
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:53
.= |.((a *') * (eval (((rpoly (1,z)) *'),y))).| by COMPLEX1:65
.= |.(eval (((a *') * ((rpoly (1,z)) *')),y)).| by POLYNOM5:30
.= |.(eval (((a * (rpoly (1,z))) *'),y)).| by Th43 ;
A30: |.(eval ((a * (rpoly (1,z))),y)).| = |.(a * (eval ((rpoly (1,z)),y))).| by POLYNOM5:30
.= |.a.| * |.(eval ((rpoly (1,z)),y)).| by COMPLEX1:65 ;
|.a.| > 0 by A27, COMPLEX1:47, COMPLFLD:7;
hence |.(eval ((a * (rpoly (1,z))),y)).| < |.(eval (((a * (rpoly (1,z))) *'),y)).| by A16, A26, A28, A30, A29, XREAL_1:68; :: thesis: verum
end;
defpred S1[ 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 :: thesis: for y, z being Element of F_Complex st rpoly (1,z) is Hurwitz & Re y = 0 holds
|.(eval ((rpoly (1,z)),y)).| = |.(eval (((rpoly (1,z)) *'),y)).|
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;
A36: y = (Re y) + ((Im y) * <i>) by COMPLEX1:13;
A37: y - z = eval ((rpoly (1,z)),y) by Th29;
A38: z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
reconsider y9 = y, z9 = z as Element of COMPLEX by COMPLFLD:def 1;
A39: - y = - y9 by COMPLFLD:2;
eval (((rpoly (1,z)) *'),y) = (- y) - (z *') by Th47;
then A40: eval (((rpoly (1,z)) *'),y) = (- y9) - (z9 *') by A39, COMPLFLD:3;
A41: |.(y9 + (z9 *')).| = |.(- (y9 + (z9 *'))).| by COMPLEX1:52;
assume Re y = 0 ; :: thesis: |.(eval ((rpoly (1,z)),y)).| = |.(eval (((rpoly (1,z)) *'),y)).|
then |.(y9 - z9).| = |.(y9 + (z9 *')).| by A35, A36, A38, Lm14;
hence |.(eval ((rpoly (1,z)),y)).| = |.(eval (((rpoly (1,z)) *'),y)).| by A37, A40, A41, COMPLFLD:3; :: thesis: verum
end;
A42: now :: thesis: for a, y, z being Element of F_Complex st rpoly (1,z) is Hurwitz & a <> 0. F_Complex & Re y = 0 holds
|.(eval ((a * (rpoly (1,z))),y)).| = |.(eval (((a * (rpoly (1,z))) *'),y)).|
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:30
.= |.a.| * |.(eval ((rpoly (1,z)),y)).| by COMPLEX1:65 ;
A45: |.a.| * |.(eval (((rpoly (1,z)) *'),y)).| = |.(a *').| * |.(eval (((rpoly (1,z)) *'),y)).| by COMPLEX1:53
.= |.((a *') * (eval (((rpoly (1,z)) *'),y))).| by COMPLEX1:65
.= |.(eval (((a *') * ((rpoly (1,z)) *')),y)).| by POLYNOM5:30
.= |.(eval (((a * (rpoly (1,z))) *'),y)).| by Th43 ;
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 :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A47: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for f being Polynomial of F_Complex st deg f >= 1 & f is Hurwitz & deg f = k + 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 & deg f = k + 1 implies for x being Element of F_Complex holds
( ( Re b3 < 0 implies |.(eval (b2,b3)).| < |.(eval ((b2 *'),b3)).| ) & ( Re b3 > 0 implies |.(eval (b2,b3)).| > |.(eval ((b2 *'),b3)).| ) & ( Re b3 = 0 implies |.(eval (b2,b3)).| = |.(eval ((b2 *'),b3)).| ) ) )
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 b3 < 0 implies |.(eval (b2,b3)).| < |.(eval ((b2 *'),b3)).| ) & ( Re b3 > 0 implies |.(eval (b2,b3)).| > |.(eval ((b2 *'),b3)).| ) & ( Re b3 = 0 implies |.(eval (b2,b3)).| = |.(eval ((b2 *'),b3)).| ) )
let x be Element of F_Complex; :: thesis: ( ( Re b2 < 0 implies |.(eval (b1,b2)).| < |.(eval ((b1 *'),b2)).| ) & ( Re b2 > 0 implies |.(eval (b1,b2)).| > |.(eval ((b1 *'),b2)).| ) & ( Re b2 = 0 implies |.(eval (b1,b2)).| = |.(eval ((b1 *'),b2)).| ) )
per cases ( k + 1 = 1 or k + 1 > 1 ) by A48, A50, XXREAL_0:1;
suppose k + 1 = 1 ; :: thesis: ( ( Re b2 < 0 implies |.(eval (b1,b2)).| < |.(eval ((b1 *'),b2)).| ) & ( Re b2 > 0 implies |.(eval (b1,b2)).| > |.(eval ((b1 *'),b2)).| ) & ( Re b2 = 0 implies |.(eval (b1,b2)).| = |.(eval ((b1 *'),b2)).| ) )
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 b2 < 0 implies |.(eval (b1,b2)).| < |.(eval ((b1 *'),b2)).| ) & ( Re b2 > 0 implies |.(eval (b1,b2)).| > |.(eval ((b1 *'),b2)).| ) & ( Re b2 = 0 implies |.(eval (b1,b2)).| = |.(eval ((b1 *'),b2)).| ) )
A54: (k + 1) + 1 > (k + 1) + 0 by XREAL_1:6;
then A55: f <> 0_. F_Complex by A50, POLYNOM4:3;
len f > 1 by A48, A50, A54, XXREAL_0:2;
then f is with_roots by POLYNOM5:74;
then consider z being Element of F_Complex such that
A56: z is_a_root_of f by POLYNOM5:def 8;
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:34;
rpoly (1,z) <> 0_. F_Complex by A57, A55, POLYNOM3:34;
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 :: thesis: ( Re x > 0 implies |.(eval (f,x)).| > |.(eval ((f *'),x)).| )
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:24;
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:46;
then A67: |.r19.| * |.e9.| >= |.r19.| * |.e19.| by A66, XREAL_1:64;
0 <= |.e19.| by COMPLEX1:46;
then |.r9.| * |.e9.| > |.r19.| * |.e9.| by A1, A60, A65, A66, XREAL_1:68;
then |.r9.| * |.e9.| > |.r19.| * |.e19.| by A67, XXREAL_0:2;
then |.(r9 * e9).| > |.r19.| * |.e19.| by COMPLEX1:65;
then A68: |.((eval ((rpoly (1,z)),x)) * (eval (f1,x))).| > |.((eval (((rpoly (1,z)) *'),x)) * (eval ((f1 *'),x))).| by COMPLEX1:65;
(eval ((rpoly (1,z)),x)) * (eval (f1,x)) = eval (((rpoly (1,z)) *' f1),x) by POLYNOM4:24;
hence |.(eval (f,x)).| > |.(eval ((f *'),x)).| by A57, A68, A64, Th46; :: thesis: verum
end;
A69: now :: thesis: ( Re x < 0 implies |.(eval (f,x)).| < |.(eval ((f *'),x)).| )
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:46;
assume A71: Re x < 0 ; :: thesis: |.(eval (f,x)).| < |.(eval ((f *'),x)).|
then A72: |.r9.| < |.r19.| by A16, A60;
0 <= |.e9.| by COMPLEX1:46;
then A73: |.r9.| * |.e9.| <= |.r19.| * |.e9.| by A72, XREAL_1:64;
|.e9.| < |.e19.| by A47, A50, A59, A61, A62, A71;
then |.r19.| * |.e9.| < |.r19.| * |.e19.| by A72, A70, XREAL_1:68;
then |.r9.| * |.e9.| < |.r19.| * |.e19.| by A73, XXREAL_0:2;
then |.(r9 * e9).| < |.r19.| * |.e19.| by COMPLEX1:65;
then A74: |.((eval ((rpoly (1,z)),x)) * (eval (f1,x))).| < |.((eval (((rpoly (1,z)) *'),x)) * (eval ((f1 *'),x))).| by COMPLEX1:65;
A75: (eval (((rpoly (1,z)) *'),x)) * (eval ((f1 *'),x)) = eval ((((rpoly (1,z)) *') *' (f1 *')),x) by POLYNOM4:24;
(eval ((rpoly (1,z)),x)) * (eval (f1,x)) = eval (((rpoly (1,z)) *' f1),x) by POLYNOM4:24;
hence |.(eval (f,x)).| < |.(eval ((f *'),x)).| by A57, A74, A75, Th46; :: thesis: verum
end;
now :: thesis: ( Re x = 0 implies |.(eval (f,x)).| = |.(eval ((f *'),x)).| )
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:24;
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:65;
then A78: |.((eval ((rpoly (1,z)),x)) * (eval (f1,x))).| = |.((eval (((rpoly (1,z)) *'),x)) * (eval ((f1 *'),x))).| by COMPLEX1:65;
(eval ((rpoly (1,z)),x)) * (eval (f1,x)) = eval (((rpoly (1,z)) *' f1),x) by POLYNOM4:24;
hence |.(eval (f,x)).| = |.(eval ((f *'),x)).| by A57, A78, A76, Th46; :: 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 S1[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: S1[ 0 ] ;
A80: for k being Nat holds S1[k] from NAT_1:sch 2(A79, A46);
 f <> 0_. F_Complex by A31, Th20;
then deg f is Element of NAT by Lm8;
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