let p be Polynomial of F_Complex ; ( len p > 1 implies p is with_roots )
assume A1:
len p > 1
; p is with_roots
then A2:
len p >= 1 + 1
by NAT_1:13;
per cases
( len p > 2 or len p = 2 )
by A2, XXREAL_0:1;
suppose
len p > 2
;
p is with_roots then consider z0 being
Element of
F_Complex such that A3:
for
z being
Element of
F_Complex holds
|.(eval p,z).| >= |.(eval p,z0).|
by Th74;
set q =
Subst p,
<%z0,(1_ F_Complex )%>;
defpred S1[
Nat]
means ( $1
>= 1 &
(Subst p,<%z0,(1_ F_Complex )%>) . $1
<> 0. F_Complex );
len <%z0,(1_ F_Complex )%> = 2
by Th41;
then A4:
len (Subst p,<%z0,(1_ F_Complex )%>) =
(((2 * (len p)) - (len p)) - 2) + 2
by A1, Th53
.=
len p
;
A5:
ex
k being
Nat st
S1[
k]
proof
(len (Subst p,<%z0,(1_ F_Complex )%>)) - 1
>= 1
- 1
by A1, A4, XREAL_1:11;
then
(len (Subst p,<%z0,(1_ F_Complex )%>)) - 1
= (len (Subst p,<%z0,(1_ F_Complex )%>)) -' 1
by XREAL_0:def 2;
then reconsider k =
(len (Subst p,<%z0,(1_ F_Complex )%>)) - 1 as
Element of
NAT ;
take
k
;
S1[k]
len (Subst p,<%z0,(1_ F_Complex )%>) >= 1
+ 1
by A1, A4, NAT_1:13;
hence
k >= 1
by XREAL_1:21;
(Subst p,<%z0,(1_ F_Complex )%>) . k <> 0. F_Complex
len (Subst p,<%z0,(1_ F_Complex )%>) = k + 1
;
hence
(Subst p,<%z0,(1_ F_Complex )%>) . k <> 0. F_Complex
by ALGSEQ_1:25;
verum
end; consider k being
Nat such that A6:
S1[
k]
and A7:
for
n being
Nat st
S1[
n] holds
k <= n
from NAT_1:sch 5(A5);
A8:
k + 1
> 1
by A6, NAT_1:13;
reconsider k1 =
k as non
empty Element of
NAT by A6, ORDINAL1:def 13;
consider sq being
CRoot of
k1,
- (((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) / ((Subst p,<%z0,(1_ F_Complex )%>) . k1));
deffunc H1(
Nat)
-> Element of the
carrier of
F_Complex =
((Subst p,<%z0,(1_ F_Complex )%>) . (k1 + $1)) * ((power F_Complex ) . sq,(k1 + $1));
consider F2 being
FinSequence of the
carrier of
F_Complex such that A9:
len F2 = (len (Subst p,<%z0,(1_ F_Complex )%>)) -' (k1 + 1)
and A10:
for
n being
Nat st
n in dom F2 holds
F2 . n = H1(
n)
from FINSEQ_2:sch 1();
k1 < len (Subst p,<%z0,(1_ F_Complex )%>)
by A6, ALGSEQ_1:22;
then A11:
(k + 1) + 0 <= len (Subst p,<%z0,(1_ F_Complex )%>)
by NAT_1:13;
then
(len (Subst p,<%z0,(1_ F_Complex )%>)) - (k + 1) >= 0
by XREAL_1:21;
then A12:
len F2 = (len (Subst p,<%z0,(1_ F_Complex )%>)) - (k + 1)
by A9, XREAL_0:def 2;
A13:
eval p,
z0 =
eval p,
(z0 + (0. F_Complex ))
by RLVECT_1:def 7
.=
eval p,
(eval <%z0,(1_ F_Complex )%>,(0. F_Complex ))
by Th48
.=
eval (Subst p,<%z0,(1_ F_Complex )%>),
(0. F_Complex )
by Th54
;
A14:
now let z be
Element of
F_Complex ;
|.(eval (Subst p,<%z0,(1_ F_Complex )%>),z).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| eval (Subst p,<%z0,(1_ F_Complex )%>),
z =
eval p,
(eval <%z0,(1_ F_Complex )%>,z)
by Th54
.=
eval p,
(z0 + z)
by Th48
;
then
|.(eval (Subst p,<%z0,(1_ F_Complex )%>),z).| >= |.(eval p,z0).|
by A3;
hence
|.(eval (Subst p,<%z0,(1_ F_Complex )%>),z).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
by A13, Th32;
verum end; now let c be
Real;
( 0 < c & c < 1 implies c * (Sum |.F2.|) >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| )assume that A15:
0 < c
and A16:
c < 1
;
c * (Sum |.F2.|) >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|set z1 =
[**c,0 **] * sq;
consider F1 being
FinSequence of the
carrier of
F_Complex such that A17:
eval (Subst p,<%z0,(1_ F_Complex )%>),
([**c,0 **] * sq) = Sum F1
and A18:
len F1 = len (Subst p,<%z0,(1_ F_Complex )%>)
and A19:
for
n being
Element of
NAT st
n in dom F1 holds
F1 . n = ((Subst p,<%z0,(1_ F_Complex )%>) . (n -' 1)) * ((power F_Complex ) . ([**c,0 **] * sq),(n -' 1))
by POLYNOM4:def 2;
A20:
dom ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )) = dom (F1 /^ (k + 1))
by POLYNOM1:def 3;
A21:
k1 < len F1
by A6, A18, ALGSEQ_1:22;
1
in Seg k
by A6, FINSEQ_1:3;
then
1
in Seg (len (F1 | k))
by A21, FINSEQ_1:80;
then A22:
1
in dom (F1 | k)
by FINSEQ_1:def 3;
A23:
dom (F1 | k) c= dom F1
by FINSEQ_5:20;
now let i be
Element of
NAT ;
( i in dom (F1 | k) & i <> 1 implies (F1 | k1) /. i = 0. F_Complex )assume that A24:
i in dom (F1 | k)
and A25:
i <> 1
;
(F1 | k1) /. i = 0. F_Complex A26:
0 + 1
<= i
by A24, FINSEQ_3:27;
then
i > 1
by A25, XXREAL_0:1;
then
i >= 1
+ 1
by NAT_1:13;
then
i - 1
>= (1 + 1) - 1
by XREAL_1:11;
then A27:
i -' 1
>= 1
by XREAL_0:def 2;
i <= len (F1 | k)
by A24, FINSEQ_3:27;
then
i <= k
by A21, FINSEQ_1:80;
then
i < k + 1
by NAT_1:13;
then A28:
i - 1
< k
by XREAL_1:21;
i - 1
>= 0
by A26, XREAL_1:21;
then A29:
i -' 1
< k
by A28, XREAL_0:def 2;
thus (F1 | k1) /. i =
F1 /. i
by A24, FINSEQ_4:85
.=
F1 . i
by A23, A24, PARTFUN1:def 8
.=
((Subst p,<%z0,(1_ F_Complex )%>) . (i -' 1)) * ((power F_Complex ) . ([**c,0 **] * sq),(i -' 1))
by A19, A23, A24
.=
(0. F_Complex ) * ((power F_Complex ) . ([**c,0 **] * sq),(i -' 1))
by A7, A27, A29
.=
0. F_Complex
by VECTSP_1:39
;
verum end; then A30:
Sum (F1 | k) =
(F1 | k1) /. 1
by A22, POLYNOM2:5
.=
F1 /. 1
by A22, FINSEQ_4:85
.=
F1 . 1
by A22, A23, PARTFUN1:def 8
.=
((Subst p,<%z0,(1_ F_Complex )%>) . (1 -' 1)) * ((power F_Complex ) . ([**c,0 **] * sq),(1 -' 1))
by A19, A22, A23
.=
((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * ((power F_Complex ) . ([**c,0 **] * sq),(1 -' 1))
by XREAL_1:234
.=
((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * ((power F_Complex ) . ([**c,0 **] * sq),0 )
by XREAL_1:234
.=
((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * (1_ F_Complex )
by GROUP_1:def 8
.=
(Subst p,<%z0,(1_ F_Complex )%>) . 0
by GROUP_1:def 5
;
k + 1
in Seg (len F1)
by A8, A11, A18, FINSEQ_1:3;
then A31:
k + 1
in dom F1
by FINSEQ_1:def 3;
then A32:
F1 . (k + 1) = F1 /. (k + 1)
by PARTFUN1:def 8;
set gc =
(Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **];
A33:
c to_power (k + 1) > 0
by A15, POWER:39;
then A34:
Sum (F1 /^ (k + 1)) =
([**(c to_power (k + 1)),0 **] * (Sum (F1 /^ (k + 1)))) / [**(c to_power (k + 1)),0 **]
by COMPLFLD:9, COMPLFLD:66
.=
[**(c to_power (k + 1)),0 **] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **])
by A33, COMPLFLD:9, COMPLFLD:64
;
A35:
F1 /. (k + 1) =
F1 . (k + 1)
by A31, PARTFUN1:def 8
.=
((Subst p,<%z0,(1_ F_Complex )%>) . ((k + 1) -' 1)) * ((power F_Complex ) . ([**c,0 **] * sq),((k + 1) -' 1))
by A19, A31
.=
((Subst p,<%z0,(1_ F_Complex )%>) . k1) * ((power F_Complex ) . ([**c,0 **] * sq),((k + 1) -' 1))
by NAT_D:34
.=
((Subst p,<%z0,(1_ F_Complex )%>) . k1) * ((power F_Complex ) . ([**c,0 **] * sq),k1)
by NAT_D:34
.=
((Subst p,<%z0,(1_ F_Complex )%>) . k1) * (((power F_Complex ) . [**c,0 **],k1) * ((power F_Complex ) . sq,k1))
by GROUP_1:100
.=
((Subst p,<%z0,(1_ F_Complex )%>) . k1) * (((power F_Complex ) . [**c,0 **],k1) * (- (((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) / ((Subst p,<%z0,(1_ F_Complex )%>) . k1))))
by COMPLFLD:def 2
.=
(((Subst p,<%z0,(1_ F_Complex )%>) . k1) * (- (((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) / ((Subst p,<%z0,(1_ F_Complex )%>) . k1)))) * ((power F_Complex ) . [**c,0 **],k1)
.=
(((Subst p,<%z0,(1_ F_Complex )%>) . k1) * ((- ((Subst p,<%z0,(1_ F_Complex )%>) . 0 )) / ((Subst p,<%z0,(1_ F_Complex )%>) . k1))) * ((power F_Complex ) . [**c,0 **],k1)
by A6, COMPLFLD:78
.=
((((Subst p,<%z0,(1_ F_Complex )%>) . k1) * (- ((Subst p,<%z0,(1_ F_Complex )%>) . 0 ))) / ((Subst p,<%z0,(1_ F_Complex )%>) . k1)) * ((power F_Complex ) . [**c,0 **],k1)
by A6, COMPLFLD:64
.=
(- ((Subst p,<%z0,(1_ F_Complex )%>) . 0 )) * ((power F_Complex ) . [**c,0 **],k1)
by A6, COMPLFLD:66
.=
(- ((Subst p,<%z0,(1_ F_Complex )%>) . 0 )) * [**(c to_power k),0 **]
by A15, HAHNBAN1:37
;
A36:
|.((((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * ((1_ F_Complex ) - [**(c to_power k),0 **])) + ([**(c to_power (k + 1)),0 **] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]))).| <= |.(((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * ((1_ F_Complex ) - [**(c to_power k),0 **])).| + |.([**(c to_power (k + 1)),0 **] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **])).|
by COMPLFLD:100;
F1 = ((F1 | ((k + 1) -' 1)) ^ <*(F1 . (k + 1))*>) ^ (F1 /^ (k + 1))
by A8, A11, A18, POLYNOM4:3;
then Sum F1 =
(Sum ((F1 | ((k + 1) -' 1)) ^ <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1)))
by A32, RLVECT_1:58
.=
((Sum (F1 | ((k + 1) -' 1))) + (Sum <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1)))
by RLVECT_1:58
.=
((Sum (F1 | k)) + (Sum <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1)))
by NAT_D:34
.=
(((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) + ((- ((Subst p,<%z0,(1_ F_Complex )%>) . 0 )) * [**(c to_power k),0 **])) + (Sum (F1 /^ (k + 1)))
by A30, A35, RLVECT_1:61
.=
(((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) + (- (((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * [**(c to_power k),0 **]))) + (Sum (F1 /^ (k + 1)))
by VECTSP_1:41
.=
((((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * (1_ F_Complex )) - (((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * [**(c to_power k),0 **])) + (Sum (F1 /^ (k + 1)))
by VECTSP_1:def 13
.=
(((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * ((1_ F_Complex ) - [**(c to_power k),0 **])) + ([**(c to_power (k + 1)),0 **] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]))
by A34, VECTSP_1:43
;
then
|.((((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * ((1_ F_Complex ) - [**(c to_power k),0 **])) + ([**(c to_power (k + 1)),0 **] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]))).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
by A14, A17;
then
|.(((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * ((1_ F_Complex ) - [**(c to_power k),0 **])).| + |.([**(c to_power (k + 1)),0 **] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **])).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
by A36, XXREAL_0:2;
then
(|.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| * |.((1_ F_Complex ) - [**(c to_power k),0 **]).|) + |.([**(c to_power (k + 1)),0 **] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **])).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
by COMPLFLD:109;
then A37:
(|.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| * |.((1_ F_Complex ) - [**(c to_power k),0 **]).|) + (|.[**(c to_power (k + 1)),0 **].| * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).|) >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
by COMPLFLD:109;
0 + (c to_power k1) <= 1
by A15, A16, TBSP_1:2;
then A38:
1
- (c to_power k) >= 0
by XREAL_1:21;
A39:
c to_power k > 0
by A15, POWER:39;
A40:
len |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| =
len ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " ))
by Def1
.=
len (F1 /^ (k + 1))
by A20, FINSEQ_3:31
.=
(len F1) - (k + 1)
by A11, A18, RFINSEQ:def 2
.=
len |.F2.|
by A12, A18, Def1
;
now let i be
Element of
NAT ;
( i in dom |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| implies |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i <= |.F2.| . i )A41:
((k + 1) + i) -' 1 =
((k + i) + 1) - 1
by XREAL_0:def 2
.=
k + i
;
assume A42:
i in dom |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).|
;
|.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i <= |.F2.| . ithen A43:
i in Seg (len |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).|)
by FINSEQ_1:def 3;
then
i <= len |.F2.|
by A40, FINSEQ_1:3;
then
i <= (len F1) - (k + 1)
by A12, A18, Def1;
then
(
(k + i) + 1
>= 0 + 1 &
(k + 1) + i <= len F1 )
by XREAL_1:8, XREAL_1:21;
then A44:
(k + 1) + i in dom F1
by FINSEQ_3:27;
i >= 0 + 1
by A43, FINSEQ_1:3;
then A45:
i - 1
>= 0
by XREAL_1:21;
c to_power (i -' 1) <= 1
by A15, A16, TBSP_1:2;
then A46:
c to_power (i - 1) <= 1
by A45, XREAL_0:def 2;
A47:
c to_power (k + i) > 0
by A15, POWER:39;
A48:
(k + i) - (k + 1) = i - 1
;
i in Seg (len ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )))
by A43, Def1;
then A49:
i in dom ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " ))
by FINSEQ_1:def 3;
then A50:
(F1 /^ (k + 1)) /. i =
(F1 /^ (k + 1)) . i
by A20, PARTFUN1:def 8
.=
F1 . ((k + 1) + i)
by A11, A18, A20, A49, RFINSEQ:def 2
.=
((Subst p,<%z0,(1_ F_Complex )%>) . (((k + 1) + i) -' 1)) * ((power F_Complex ) . ([**c,0 **] * sq),(((k + 1) + i) -' 1))
by A19, A44
.=
((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * (((power F_Complex ) . sq,(k + i)) * ((power F_Complex ) . [**c,0 **],(k + i)))
by A41, GROUP_1:100
.=
(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))) * ((power F_Complex ) . [**c,0 **],(k + i))
;
A51:
len F2 = len |.F2.|
by Def1;
then A52:
dom F2 = dom |.F2.|
by FINSEQ_3:31;
A53:
|.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i =
|.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| /. i
by A42, PARTFUN1:def 8
.=
|.(((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )) /. i).|
by A49, Def1
.=
|.(((F1 /^ (k + 1)) /. i) * ([**(c to_power (k + 1)),0 **] " )).|
by A20, A49, POLYNOM1:def 3
.=
|.((F1 /^ (k + 1)) /. i).| * |.([**(c to_power (k + 1)),0 **] " ).|
by COMPLFLD:109
.=
|.((((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))) * ((power F_Complex ) . [**c,0 **],(k + i))).| * ((abs (c to_power (k + 1))) " )
by A33, A50, COMPLFLD:9, COMPLFLD:110
.=
(|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * |.((power F_Complex ) . [**c,0 **],(k + i)).|) * ((abs (c to_power (k + 1))) " )
by COMPLFLD:109
.=
(|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * |.[**(c to_power (k + i)),0 **].|) * ((abs (c to_power (k + 1))) " )
by A15, HAHNBAN1:37
.=
(|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * (c to_power (k + i))) * ((abs (c to_power (k + 1))) " )
by A47, ABSVALUE:def 1
.=
(|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * (c to_power (k + i))) * ((c to_power (k + 1)) " )
by A33, ABSVALUE:def 1
.=
|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * ((c to_power (k + i)) * ((c to_power (k + 1)) " ))
.=
|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * ((c to_power (k + i)) / (c to_power (k + 1)))
.=
|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * (c to_power (i - 1))
by A15, A48, POWER:34
;
A54:
i in dom F2
by A40, A43, A51, FINSEQ_1:def 3;
then ((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i)) =
F2 . i
by A10
.=
F2 /. i
by A54, PARTFUN1:def 8
;
then
|.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i <= |.(F2 /. i).|
by A46, A53, COMPLEX1:132, XREAL_1:155;
then
|.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i <= |.F2.| /. i
by A54, Def1;
hence
|.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i <= |.F2.| . i
by A52, A54, PARTFUN1:def 8;
verum end; then A55:
Sum |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| <= Sum |.F2.|
by A40, INTEGRA5:3;
|.((1_ F_Complex ) - [**(c to_power k),0 **]).| =
|.([**1,0 **] - [**(c to_power k),0 **]).|
by COMPLEX1:def 7, COMPLFLD:10
.=
|.[**(1 - (c to_power k1)),(0 - 0 )**].|
by Th6
.=
1
- (c to_power k)
by A38, ABSVALUE:def 1
;
then
|.[**(c to_power (k + 1)),0 **].| * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| >= (|.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| * 1) - (|.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| * (1 - (c to_power k)))
by A37, XREAL_1:22;
then
(c to_power (k + 1)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| * (c to_power k)
by A33, ABSVALUE:def 1;
then
((c to_power (k + 1)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).|) / (c to_power k) >= (|.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| * (c to_power k)) / (c to_power k)
by A39, XREAL_1:74;
then
((c to_power (k + 1)) / (c to_power k)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
by A39, XCMPLX_1:90;
then
(c to_power ((k + 1) - k)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
by A15, POWER:34;
then A56:
c * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
by POWER:30;
(Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **] =
(Sum (F1 /^ (k + 1))) * ([**(c to_power (k + 1)),0 **] " )
by VECTSP_1:def 23
.=
Sum ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " ))
by POLYNOM1:29
;
then
|.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| <= Sum |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).|
by Th15;
then
|.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| <= Sum |.F2.|
by A55, XXREAL_0:2;
then
c * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| <= c * (Sum |.F2.|)
by A15, XREAL_1:66;
hence
c * (Sum |.F2.|) >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
by A56, XXREAL_0:2;
verum end; then
|.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| <= 0
by Lm1;
then A57:
(Subst p,<%z0,(1_ F_Complex )%>) . 0 = 0. F_Complex
by COMPLFLD:96;
ex
x being
Element of
F_Complex st
x is_a_root_of p
hence
p is
with_roots
by Def7;
verum end;