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 = In (|.(eval ((NormPolynomial p),$1)).|,REAL);
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 ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not b in D or 0 <= b )
assume b in D ; :: thesis: 0 <= b
then consider z being Element of F_Complex such that
A2: b = In (|.(eval ((NormPolynomial p),z)).|,REAL) ;
b = |.(eval ((NormPolynomial p),z)).| by A2;
hence 0 <= b by COMPLEX1:46; :: thesis: verum
end;
defpred S2[ Nat, object ] means ex g1 being Element of F_Complex st
( g1 = $2 & |.(eval ((NormPolynomial p),g1)).| < (lower_bound D) + (1 / ($1 + 1)) );
In (|.(eval ((NormPolynomial p),(0. F_Complex))).|,REAL) = |.(eval ((NormPolynomial p),(0. F_Complex))).| ;
then A3: |.(eval ((NormPolynomial p),(0. F_Complex))).| in D ;
A4: for n being Nat ex g being Complex st S2[n,g]
proof
let n be Nat; :: thesis: ex g being Complex st S2[n,g]
consider r being Real such that
A5: r in D and
A6: r < (lower_bound D) + (1 / (n + 1)) by A3, A1, SEQ_4:def 2;
consider g1 being Element of F_Complex such that
A7: r = In (|.(eval ((NormPolynomial p),g1)).|,REAL) by A5;
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 A6, A7; :: thesis: verum
end;
consider G being Complex_Sequence such that
A8: for n being Nat holds S2[n,G . n] from CFCONT_1:sch 1(A4);
 deffunc H2( Nat) -> Element of REAL = In (|.((NormPolynomial p) . ($1 -' 1)).|,REAL);
consider F being FinSequence of REAL such that
A9: len F = len (NormPolynomial p) and
A10: for n being Nat st n in dom F holds
F . n = H2(n) from FINSEQ_2:sch 1();
 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;
G is bounded
proof
take r = (Sum F) + 1; :: according to COMSEQ_2:def 4 :: thesis: for b1 being set holds not r <= |.(G . b1).|
let n be Nat; :: thesis: not r <= |.(G . n).|
consider Gn being Element of F_Complex such that
A14: Gn = G . n and
A15: |.(eval ((NormPolynomial p),Gn)).| < (lower_bound D) + (1 / (n + 1)) by A8;
n + 1 >= 0 + 1 by XREAL_1:6;
then A16: 1 / (n + 1) <= 1 by XREAL_1:211;
A17: len (NormPolynomial p) = len p by A11, Th57;
then A18: (NormPolynomial p) . ((len (NormPolynomial p)) -' 1) = 1_ F_Complex by A11, Th56;
|.(G . n).| <= Sum F
proof
A19: eval ((NormPolynomial p),(0. F_Complex)) = (NormPolynomial p) . 0 by Th31;
In (|.((NormPolynomial p) . 0).|,REAL) = |.((NormPolynomial p) . 0).| ;
then |.((NormPolynomial p) . 0).| in D by A19;
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 A16, XREAL_1:7;
A21: for n being Element of NAT st n in dom F holds
F . n = |.((NormPolynomial p) . (n -' 1)).|
proof
let n be Element of NAT ; :: thesis: ( n in dom F implies F . n = |.((NormPolynomial p) . (n -' 1)).| )
assume n in dom F ; :: thesis: F . n = |.((NormPolynomial p) . (n -' 1)).|
then F . n = H2(n) by A10;
hence F . n = |.((NormPolynomial p) . (n -' 1)).| ; :: thesis: verum
end;
assume |.(G . n).| > Sum F ; :: thesis: contradiction
then |.(eval ((NormPolynomial p),Gn)).| > |.((NormPolynomial p) . 0).| + 1 by A11, A9, A14, A17, A18, A21, COMPLFLD:60, Th72;
hence contradiction by A15, A20, XXREAL_0:2; :: thesis: verum
end;
then |.(G . n).| + 0 < r by XREAL_1:8;
hence not r <= |.(G . n).| ; :: thesis: verum
end;
then consider G1 being Complex_Sequence such that
A22: G1 is subsequence of G and
A23: G1 is convergent by COMSEQ_3:50;
defpred S3[ Nat, object ] means ex G1n being Element of F_Complex st
( G1n = G1 . $1 & $2 = eval ((NormPolynomial p),G1n) );
lim G1 in COMPLEX by XCMPLX_0:def 2;
then reconsider z0 = lim G1 as Element of F_Complex by COMPLFLD:def 1;
A24: for n being Nat ex g being Complex st S3[n,g]
proof
let n be Nat; :: thesis: ex g being Complex st S3[n,g]
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider G1n = G1 . nn 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
A25: for n being Nat holds S3[n,H . n] from CFCONT_1:sch 1(A24);
 reconsider enp0 = eval ((NormPolynomial p),z0) as Element of COMPLEX by COMPLFLD:def 1;
consider g being Complex such that
A26: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((G1 . m) - g).| < p by A23;
A27: g in COMPLEX by XCMPLX_0:def 2;
then 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 :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((H . m) - eg).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((H . m) - eg).| < p )
consider fPF being Function of COMPLEX,COMPLEX such that
A28: fPF = Polynomial-Function (F_Complex,(NormPolynomial p)) and
A29: fPF is_continuous_on COMPLEX by Th71;
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((H . m) - eg).| < p
then consider p1 being Real such that
A30: 0 < p1 and
A31: for x1 being Complex st x1 in COMPLEX & |.(x1 - g).| < p1 holds
|.((fPF /. x1) - (fPF /. g)).| < p by A29, CFCONT_1:39, A27;
consider n being Nat such that
A32: for m being Nat st n <= m holds
|.((G1 . m) - g).| < p1 by A26, A30;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((H . m) - eg).| < p
let m be Nat; :: thesis: ( n <= m implies |.((H . m) - eg).| < p )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: |.((H . m) - eg).| < p
then A33: |.((G1 . m) - g).| < p1 by A32;
ex G1m being Element of F_Complex st
( G1m = G1 . m & H . m = eval ((NormPolynomial p),G1m) ) by A25;
then A34: H . m = fPF /. (G1 . mm) by A28, Def13;
eg = fPF /. g by A28, Def13;
hence |.((H . m) - eg).| < p by A31, A33, A34; :: thesis: verum
end;
then A35: H is convergent ;
consider PF being Function of COMPLEX,COMPLEX such that
A36: PF = Polynomial-Function (F_Complex,(NormPolynomial p)) and
A37: PF is_continuous_on COMPLEX by Th71;
now :: thesis: for a being Real st 0 < a holds
ex n being Nat st
for m being Nat st n <= m holds
|.((H . m) - enp0).| < a
let a be Real; :: thesis: ( 0 < a implies ex n being Nat st
for m being Nat st n <= m holds
|.((H . m) - enp0).| < a )
A38: lim G1 in COMPLEX by XCMPLX_0:def 2;
assume 0 < a ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((H . m) - enp0).| < a
then consider s being Real such that
A39: 0 < s and
A40: for x1 being Complex st x1 in COMPLEX & |.(x1 - (lim G1)).| < s holds
|.((PF /. x1) - (PF /. (lim G1))).| < a by A37, CFCONT_1:39, A38;
consider n being Nat such that
A41: for m being Nat st n <= m holds
|.((G1 . m) - (lim G1)).| < s by A23, A39, COMSEQ_2:def 6;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((H . m) - enp0).| < a
let m be Nat; :: thesis: ( n <= m implies |.((H . m) - enp0).| < a )
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: |.((H . m) - enp0).| < a
then A42: |.((G1 . m) - (lim G1)).| < s by A41;
ex G1m being Element of F_Complex st
( G1m = G1 . m & H . m = eval ((NormPolynomial p),G1m) ) by A25;
then A43: PF /. (G1 . mm) = H . m by A36, Def13;
PF /. (lim G1) = eval ((NormPolynomial p),z0) by A36, Def13;
hence |.((H . m) - enp0).| < a by A40, A42, A43; :: thesis: verum
end;
then A44: enp0 = lim H by A35, COMSEQ_2:def 6;
deffunc H3( Nat) -> set = 1 / ($1 + 1);
consider R being Real_Sequence such that
A45: for n being 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 v = |.(eval ((NormPolynomial p),z)).| as Element of REAL by XREAL_0:def 1;
set Rcons = seq_const |.(eval ((NormPolynomial p),z)).|;
consider Nseq being increasing sequence of NAT such that
A46: G1 = G * Nseq by A22, VALUED_0:def 17;
In (|.(eval ((NormPolynomial p),z)).|,REAL) = |.(eval ((NormPolynomial p),z)).| ;
then |.(eval ((NormPolynomial p),z)).| in D ;
then A47: |.(eval ((NormPolynomial p),z)).| >= lower_bound D by A1, SEQ_4:def 2;
A48: now :: thesis: for n being Nat holds (seq_const |.(eval ((NormPolynomial p),z)).|) . n >= (|.H.| - R) . n
let n be Nat; :: thesis: (seq_const |.(eval ((NormPolynomial p),z)).|) . n >= (|.H.| - R) . n
A49: n in NAT by ORDINAL1:def 12;
consider G1n being Element of F_Complex such that
A50: G1n = G1 . n and
A51: H . n = eval ((NormPolynomial p),G1n) by A25;
consider gNn being Element of F_Complex such that
A52: gNn = G . (Nseq . n) and
A53: |.(eval ((NormPolynomial p),gNn)).| < (lower_bound D) + (1 / ((Nseq . n) + 1)) by A8;
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 A53, XXREAL_0:2;
then lower_bound D > |.(eval ((NormPolynomial p),gNn)).| - (1 / (n + 1)) by XREAL_1:19;
then A54: ( (seq_const |.(eval ((NormPolynomial p),z)).|) . n = |.(eval ((NormPolynomial p),z)).| & |.(eval ((NormPolynomial p),z)).| > |.(eval ((NormPolynomial p),gNn)).| - (1 / (n + 1)) ) by A47, SEQ_1:57, XXREAL_0:2;
dom (|.H.| - R) = NAT by FUNCT_2:def 1;
then (|.H.| - R) . n = (|.H.| . n) - (R . n) by VALUED_1:13, A49
.= (|.H.| . n) - (1 / (n + 1)) by A45
.= |.(eval ((NormPolynomial p),G1n)).| - (1 / (n + 1)) by A51, VALUED_1:18 ;
hence (seq_const |.(eval ((NormPolynomial p),z)).|) . n >= (|.H.| - R) . n by A46, A50, A52, A54, FUNCT_2:15, A49; :: thesis: verum
end;
A55: R is convergent by A45, SEQ_4:31;
then |.H.| - R is convergent by A35;
then ( (seq_const |.(eval ((NormPolynomial p),z)).|) . 0 = |.(eval ((NormPolynomial p),z)).| & lim (|.H.| - R) <= lim (seq_const |.(eval ((NormPolynomial p),z)).|) ) by A48, SEQ_1:57, SEQ_2:18;
then A56: lim (|.H.| - R) <= |.(eval ((NormPolynomial p),z)).| by SEQ_4:25;
lim (|.H.| - R) = (lim |.H.|) - (lim R) by A35, A55, SEQ_2:12
.= |.(lim H).| - (lim R) by A35, SEQ_2:27
.= |.(lim H).| - 0 by A45, SEQ_4:31 ;
then |.((eval (p,z)) / (p . ((len p) -' 1))).| >= |.(eval ((NormPolynomial p),z0)).| by A11, A56, A44, Th58;
then |.((eval (p,z)) / (p . ((len p) -' 1))).| >= |.((eval (p,z0)) / (p . ((len p) -' 1))).| by A11, Th58;
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