A1:
now 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;
( 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
;
( 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
;
|.(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;
verum end;
A10:
now 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;
( 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
;
( Re y > 0 implies |.(eval ((a * (rpoly (1,z))),y)).| > |.(eval (((a * (rpoly (1,z))) *'),y)).| )assume A13:
Re y > 0
;
|.(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;
verum end;
A16:
now 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;
( 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
;
( 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
;
|.(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;
verum end;
A25:
now 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;
( 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
;
( Re y < 0 implies |.(eval ((a * (rpoly (1,z))),y)).| < |.(eval (((a * (rpoly (1,z))) *'),y)).| )assume A28:
Re y < 0
;
|.(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;
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; ( 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
; 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 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;
( 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
;
( 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
;
|.(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;
verum end;
A42:
now 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;
( 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
;
( 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
;
|.(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;
verum end;
A46:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A47:
S1[
k]
;
S1[k + 1]now 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;
( 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
;
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;
( ( 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
;
( ( 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;
verum end; suppose A53:
k + 1
> 1
;
( ( 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 ( 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
;
|.(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;
verum end; A69:
now ( 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
;
|.(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;
verum end; now ( 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
;
|.(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;
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;
verum end; end; end; hence
S1[
k + 1]
;
verum end;
let x be Element of F_Complex; ( ( 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; verum