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 SEQ_4:def 2 :: thesis: for b1 being set holds
( not b1 in D or 0 <= b1 )
let b be real number ; :: 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:132; :: 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 5;
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:237, XXREAL_0:2;
then p . ((len p) -' 1) <> 0. F_Complex by ALGSEQ_1:25;
then A13: |.(p . ((len p) -' 1)).| > 0 by COMPLFLD:96;
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:8;
then A17: 1 / (n + 1) <= 1 by XREAL_1:213;
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 5;
then A20: |.((NormPolynomial p) . 0 ).| + 1 >= (lower_bound D) + (1 / (n + 1)) by A17, XREAL_1:9;
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:97;
hence contradiction by A16, A20, XXREAL_0:2; :: thesis: verum
end;
then |.(G . n).| + 0 < r by XREAL_1:10;
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:51;
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:61;
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:61;
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 V65() 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 5;
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:33;
then (Nseq . n) + 1 >= n + 1 by XREAL_1:8;
then 1 / ((Nseq . n) + 1) <= 1 / (n + 1) by XREAL_1:87;
then (lower_bound D) + (1 / ((Nseq . n) + 1)) <= (lower_bound D) + (1 / (n + 1)) by XREAL_1:8;
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:21;
then A50: ( Rcons . n = |.(eval (NormPolynomial p),z).| & |.(eval (NormPolynomial p),z).| > |.(eval (NormPolynomial p),gNn).| - (1 / (n + 1)) ) by A44, FUNCOP_1:13, 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:21; :: thesis: verum
end;
A51: R is convergent by A42, SEQ_4:43;
then |.H.| - R is convergent by A33, SEQ_2:25;
then ( Rcons . 0 = |.(eval (NormPolynomial p),z).| & lim (|.H.| - R) <= lim Rcons ) by A45, FUNCOP_1:13, SEQ_2:32;
then A52: lim (|.H.| - R) <= |.(eval (NormPolynomial p),z).| by SEQ_4:40;
lim (|.H.| - R) = (lim |.H.|) - (lim R) by A33, A51, SEQ_2:26
.= |.(lim H).| - (lim R) by A33, COMSEQ_2:11
.= |.(lim H).| - 0 by A42, SEQ_4:44 ;
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:25, COMPLFLD:111;
then |.(eval p,z).| / |.(p . ((len p) -' 1)).| >= |.(eval p,z0).| / |.(p . ((len p) -' 1)).| by A12, ALGSEQ_1:25, COMPLFLD:111;
hence |.(eval p,z).| >= |.(eval p,z0).| by A13, XREAL_1:76; :: thesis: verum