defpred S1[ set ] means verum;
let p be Polynomial of F_Complex; :: thesis: ( len p > 2 implies ex z0 being Element of F_Complex st
for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).| )
set np = NormPolynomial p;
deffunc H1( Element of F_Complex) -> Element of REAL = |.(eval ((NormPolynomial p),$1)).|;
reconsider D = { H1(z) where z is Element of F_Complex : S1[z] } as Subset of REAL from DOMAIN_1:sch 8();
 set q = lower_bound D;
A1: D is bounded_below
proof
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of D
let b be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not b in D or 0 <= b )
assume b in D ; :: thesis: 0 <= b
then ex z being Element of F_Complex st b = |.(eval ((NormPolynomial p),z)).| ;
hence 0 <= b by COMPLEX1:46; :: thesis: verum
end;
defpred S2[ Element of NAT , set ] means ex g1 being Element of F_Complex st
( g1 = $2 & |.(eval ((NormPolynomial p),g1)).| < (lower_bound D) + (1 / ($1 + 1)) );
A2: |.(eval ((NormPolynomial p),(0. F_Complex))).| in D ;
A3: for n being Element of NAT ex g being Element of COMPLEX st S2[n,g]
proof
let n be Element of NAT ; :: thesis: ex g being Element of COMPLEX st S2[n,g]
consider r being real number such that
A4: r in D and
A5: r < (lower_bound D) + (1 / (n + 1)) by A2, A1, SEQ_4:def 2;
consider g1 being Element of F_Complex such that
A6: r = |.(eval ((NormPolynomial p),g1)).| by A4;
reconsider g = g1 as Element of COMPLEX by COMPLFLD:def 1;
take g ; :: thesis: S2[n,g]
take g1 ; :: thesis: ( g1 = g & |.(eval ((NormPolynomial p),g1)).| < (lower_bound D) + (1 / (n + 1)) )
thus g1 = g ; :: thesis: |.(eval ((NormPolynomial p),g1)).| < (lower_bound D) + (1 / (n + 1))
thus |.(eval ((NormPolynomial p),g1)).| < (lower_bound D) + (1 / (n + 1)) by A5, A6; :: thesis: verum
end;
consider G being Complex_Sequence such that
A7: for n being Element of NAT holds S2[n,G . n] from CFCONT_1:sch 1(A3);
 deffunc H2( Nat) -> Element of REAL = |.((NormPolynomial p) . ($1 -' 1)).|;
consider F being FinSequence of REAL such that
A8: len F = len (NormPolynomial p) and
A9: for n being Nat st n in dom F holds
F . n = H2(n) from FINSEQ_2:sch 1();
 dom F = Seg (len (NormPolynomial p)) by A8, FINSEQ_1:def 3;
then A10: for n being Element of NAT st n in Seg (len (NormPolynomial p)) holds
F . n = H2(n) by A9;
assume A11: len p > 2 ; :: thesis: ex z0 being Element of F_Complex st
for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).|
then A12: len p = ((len p) -' 1) + 1 by XREAL_1:235, XXREAL_0:2;
then p . ((len p) -' 1) <> 0. F_Complex by ALGSEQ_1:10;
then A13: |.(p . ((len p) -' 1)).| > 0 by COMPLFLD:59;
A14: Seg (len (NormPolynomial p)) = dom F by A8, FINSEQ_1:def 3;
ex r being Real st
for n being Element of NAT holds |.(G . n).| < r
proof
take r = (Sum F) + 1; :: thesis: for n being Element of NAT holds |.(G . n).| < r
let n be Element of NAT ; :: thesis: |.(G . n).| < r
consider Gn being Element of F_Complex such that
A15: Gn = G . n and
A16: |.(eval ((NormPolynomial p),Gn)).| < (lower_bound D) + (1 / (n + 1)) by A7;
n + 1 >= 0 + 1 by XREAL_1:6;
then A17: 1 / (n + 1) <= 1 by XREAL_1:211;
A18: len (NormPolynomial p) = len p by A11, Th58;
then A19: (NormPolynomial p) . ((len (NormPolynomial p)) -' 1) = 1_ F_Complex by A11, Th57;
|.(G . n).| <= Sum F
proof
eval ((NormPolynomial p),(0. F_Complex)) = (NormPolynomial p) . 0 by Th32;
then |.((NormPolynomial p) . 0).| in D ;
then |.((NormPolynomial p) . 0).| >= lower_bound D by A1, SEQ_4:def 2;
then A20: |.((NormPolynomial p) . 0).| + 1 >= (lower_bound D) + (1 / (n + 1)) by A17, XREAL_1:7;
assume |.(G . n).| > Sum F ; :: thesis: contradiction
then |.(eval ((NormPolynomial p),Gn)).| > |.((NormPolynomial p) . 0).| + 1 by A11, A8, A10, A14, A15, A18, A19, Th73, COMPLFLD:60;
hence contradiction by A16, A20, XXREAL_0:2; :: thesis: verum
end;
then |.(G . n).| + 0 < r by XREAL_1:8;
hence |.(G . n).| < r ; :: thesis: verum
end;
then G is bounded by COMSEQ_2:def 3;
then consider G1 being Complex_Sequence such that
A21: G1 is subsequence of G and
A22: G1 is convergent by COMSEQ_3:50;
defpred S3[ Element of NAT , set ] means ex G1n being Element of F_Complex st
( G1n = G1 . $1 & $2 = eval ((NormPolynomial p),G1n) );
reconsider z0 = lim G1 as Element of F_Complex by COMPLFLD:def 1;
A23: for n being Element of NAT ex g being Element of COMPLEX st S3[n,g]
proof
let n be Element of NAT ; :: thesis: ex g being Element of COMPLEX st S3[n,g]
reconsider G1n = G1 . n as Element of F_Complex by COMPLFLD:def 1;
reconsider g = eval ((NormPolynomial p),G1n) as Element of COMPLEX by COMPLFLD:def 1;
take g ; :: thesis: S3[n,g]
take G1n ; :: thesis: ( G1n = G1 . n & g = eval ((NormPolynomial p),G1n) )
thus G1n = G1 . n ; :: thesis: g = eval ((NormPolynomial p),G1n)
thus g = eval ((NormPolynomial p),G1n) ; :: thesis: verum
end;
consider H being Complex_Sequence such that
A24: for n being Element of NAT holds S3[n,H . n] from CFCONT_1:sch 1(A23);
 reconsider enp0 = eval ((NormPolynomial p),z0) as Element of COMPLEX by COMPLFLD:def 1;
consider g being Element of COMPLEX such that
A25: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((G1 . m) - g).| < p by A22, COMSEQ_2:def 4;
reconsider g1 = g as Element of F_Complex by COMPLFLD:def 1;
reconsider eg = eval ((NormPolynomial p),g1) as Element of COMPLEX by COMPLFLD:def 1;
now
let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((H . m) - eg).| < p )
consider fPF being Function of COMPLEX,COMPLEX such that
A26: fPF = Polynomial-Function (F_Complex,(NormPolynomial p)) and
A27: fPF is_continuous_on COMPLEX by Th72;
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((H . m) - eg).| < p
then consider p1 being Real such that
A28: 0 < p1 and
A29: for x1 being Element of COMPLEX st x1 in COMPLEX & |.(x1 - g).| < p1 holds
|.((fPF /. x1) - (fPF /. g)).| < p by A27, CFCONT_1:39;
consider n being Element of NAT such that
A30: for m being Element of NAT st n <= m holds
|.((G1 . m) - g).| < p1 by A25, A28;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
|.((H . m) - eg).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.((H . m) - eg).| < p )
assume n <= m ; :: thesis: |.((H . m) - eg).| < p
then A31: |.((G1 . m) - g).| < p1 by A30;
ex G1m being Element of F_Complex st
( G1m = G1 . m & H . m = eval ((NormPolynomial p),G1m) ) by A24;
then A32: H . m = fPF /. (G1 . m) by A26, Def12;
eg = fPF /. g by A26, Def12;
hence |.((H . m) - eg).| < p by A29, A31, A32; :: thesis: verum
end;
then A33: H is convergent by COMSEQ_2:def 4;
consider PF being Function of COMPLEX,COMPLEX such that
A34: PF = Polynomial-Function (F_Complex,(NormPolynomial p)) and
A35: PF is_continuous_on COMPLEX by Th72;
now
let a be Real; :: thesis: ( 0 < a implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((H . m) - enp0).| < a )
assume 0 < a ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((H . m) - enp0).| < a
then consider s being Real such that
A36: 0 < s and
A37: for x1 being Element of COMPLEX st x1 in COMPLEX & |.(x1 - (lim G1)).| < s holds
|.((PF /. x1) - (PF /. (lim G1))).| < a by A35, CFCONT_1:39;
consider n being Element of NAT such that
A38: for m being Element of NAT st n <= m holds
|.((G1 . m) - (lim G1)).| < s by A22, A36, COMSEQ_2:def 5;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
|.((H . m) - enp0).| < a
let m be Element of NAT ; :: thesis: ( n <= m implies |.((H . m) - enp0).| < a )
assume n <= m ; :: thesis: |.((H . m) - enp0).| < a
then A39: |.((G1 . m) - (lim G1)).| < s by A38;
ex G1m being Element of F_Complex st
( G1m = G1 . m & H . m = eval ((NormPolynomial p),G1m) ) by A24;
then A40: PF /. (G1 . m) = H . m by A34, Def12;
PF /. (lim G1) = eval ((NormPolynomial p),z0) by A34, Def12;
hence |.((H . m) - enp0).| < a by A37, A39, A40; :: thesis: verum
end;
then A41: enp0 = lim H by A33, COMSEQ_2:def 5;
deffunc H3( Element of NAT ) -> Element of REAL = 1 / ($1 + 1);
consider R being Real_Sequence such that
A42: for n being Element of NAT holds R . n = H3(n) from SEQ_1:sch 1();
 take z0 ; :: thesis: for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).|
let z be Element of F_Complex; :: thesis: |.(eval (p,z)).| >= |.(eval (p,z0)).|
reconsider Rcons = NAT --> |.(eval ((NormPolynomial p),z)).| as Real_Sequence ;
consider Nseq being V43() sequence of NAT such that
A43: G1 = G * Nseq by A21, VALUED_0:def 17;
|.(eval ((NormPolynomial p),z)).| in D ;
then A44: |.(eval ((NormPolynomial p),z)).| >= lower_bound D by A1, SEQ_4:def 2;
A45: now
let n be Element of NAT ; :: thesis: Rcons . n >= (|.H.| - R) . n
consider G1n being Element of F_Complex such that
A46: G1n = G1 . n and
A47: H . n = eval ((NormPolynomial p),G1n) by A24;
consider gNn being Element of F_Complex such that
A48: gNn = G . (Nseq . n) and
A49: |.(eval ((NormPolynomial p),gNn)).| < (lower_bound D) + (1 / ((Nseq . n) + 1)) by A7;
Nseq . n >= n by SEQM_3:14;
then (Nseq . n) + 1 >= n + 1 by XREAL_1:6;
then 1 / ((Nseq . n) + 1) <= 1 / (n + 1) by XREAL_1:85;
then (lower_bound D) + (1 / ((Nseq . n) + 1)) <= (lower_bound D) + (1 / (n + 1)) by XREAL_1:6;
then |.(eval ((NormPolynomial p),gNn)).| < (lower_bound D) + (1 / (n + 1)) by A49, XXREAL_0:2;
then lower_bound D > |.(eval ((NormPolynomial p),gNn)).| - (1 / (n + 1)) by XREAL_1:19;
then A50: ( Rcons . n = |.(eval ((NormPolynomial p),z)).| & |.(eval ((NormPolynomial p),z)).| > |.(eval ((NormPolynomial p),gNn)).| - (1 / (n + 1)) ) by A44, FUNCOP_1:7, XXREAL_0:2;
dom (|.H.| - R) = NAT by FUNCT_2:def 1;
then (|.H.| - R) . n = (|.H.| . n) - (R . n) by VALUED_1:13
.= (|.H.| . n) - (1 / (n + 1)) by A42
.= |.(eval ((NormPolynomial p),G1n)).| - (1 / (n + 1)) by A47, VALUED_1:18 ;
hence Rcons . n >= (|.H.| - R) . n by A43, A46, A48, A50, FUNCT_2:15; :: thesis: verum
end;
A51: R is convergent by A42, SEQ_4:28;
then |.H.| - R is convergent by A33, SEQ_2:11;
then ( Rcons . 0 = |.(eval ((NormPolynomial p),z)).| & lim (|.H.| - R) <= lim Rcons ) by A45, FUNCOP_1:7, SEQ_2:18;
then A52: lim (|.H.| - R) <= |.(eval ((NormPolynomial p),z)).| by SEQ_4:25;
lim (|.H.| - R) = (lim |.H.|) - (lim R) by A33, A51, SEQ_2:12
.= |.(lim H).| - (lim R) by A33, COMSEQ_2:11
.= |.(lim H).| - 0 by A42, SEQ_4:29 ;
then |.((eval (p,z)) / (p . ((len p) -' 1))).| >= |.(eval ((NormPolynomial p),z0)).| by A11, A52, A41, Th59;
then |.((eval (p,z)) / (p . ((len p) -' 1))).| >= |.((eval (p,z0)) / (p . ((len p) -' 1))).| by A11, Th59;
then |.(eval (p,z)).| / |.(p . ((len p) -' 1)).| >= |.((eval (p,z0)) / (p . ((len p) -' 1))).| by A12, ALGSEQ_1:10, COMPLFLD:73;
then |.(eval (p,z)).| / |.(p . ((len p) -' 1)).| >= |.(eval (p,z0)).| / |.(p . ((len p) -' 1)).| by A12, ALGSEQ_1:10, COMPLFLD:73;
hence |.(eval (p,z)).| >= |.(eval (p,z0)).| by A13, XREAL_1:74; :: thesis: verum