let p be Polynomial of F_Complex; :: thesis: ( len p > 2 implies for r being Real ex e being Real st
for z being Element of F_Complex st e < |.z.| holds
|.(eval (p,z)).| > r )
assume A1: len p > 2 ; :: thesis: for r being Real ex e being Real st
for z being Element of F_Complex st e < |.z.| holds
|.(eval (p,z)).| > r
let r be Real; :: thesis: ex e being Real st
for z being Element of F_Complex st e < |.z.| holds
|.(eval (p,z)).| > r
set N = NormPolynomial p;
A2: len (NormPolynomial p) = len p by A1, POLYNOM5:57;
then (NormPolynomial p) . ((len (NormPolynomial p)) -' 1) = 1. F_Complex by A1, POLYNOM5:56;
then (NormPolynomial p) . ((len (NormPolynomial p)) -' 1) = 1 by COMPLFLD:def 1;
then A3: |.((NormPolynomial p) . ((len (NormPolynomial p)) -' 1)).| = 1 ;
deffunc H₁( Nat) -> Element of REAL = In (|.((NormPolynomial p) . ($1 -' 1)).|,REAL);
consider F being FinSequence of REAL such that
A4: len F = len (NormPolynomial p) and
A5: for n being Nat st n in dom F holds
F . n = H₁(n) from FINSEQ_2:sch 1();
take e = ((|.(p . ((len p) -' 1)).| ") * |.(r + 1).|) + |.(Sum F).|; :: thesis: for z being Element of F_Complex st e < |.z.| holds
|.(eval (p,z)).| > r
let z be Element of F_Complex; :: thesis: ( e < |.z.| implies |.(eval (p,z)).| > r )
assume A6: e < |.z.| ; :: thesis: |.(eval (p,z)).| > r
A7: 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)).|
hence F . n = H₁(n) by A5
.= |.((NormPolynomial p) . (n -' 1)).| ;
:: thesis: verum

end;

for n being Nat st n in dom F holds
F . n >= 0

proof

let n be Nat; :: thesis: ( n in dom F implies F . n >= 0 )
assume n in dom F ; :: thesis: F . n >= 0
then F . n = |.((NormPolynomial p) . (n -' 1)).| by A7;
hence F . n >= 0 ; :: thesis: verum

end;

then A8: |.(Sum F).| = Sum F by RVSUM_1:84, COMPLEX1:43;
e >= |.(Sum F).| + 0 by XREAL_1:6;
then |.z.| > |.(Sum F).| by A6, XXREAL_0:2;
then |.(eval ((NormPolynomial p),z)).| >= |.z.| by A8, A7, A1, A2, A3, A4, POLYNOM5:72;
then ( |.(eval ((NormPolynomial p),z)).| >= ((|.(p . ((len p) -' 1)).| ") * |.(r + 1).|) + |.(Sum F).| & ((|.(p . ((len p) -' 1)).| ") * |.(r + 1).|) + |.(Sum F).| >= ((|.(p . ((len p) -' 1)).| ") * |.(r + 1).|) + 0 ) by A6, XXREAL_0:2, XREAL_1:6;
then A9: |.(eval ((NormPolynomial p),z)).| >= (|.(p . ((len p) -' 1)).| ") * |.(r + 1).| by XXREAL_0:2;
A10: p . ((len p) -' 1) <> 0. F_Complex by A1, UPROOTS:18;
then A11: p . ((len p) -' 1) <> 0 by COMPLFLD:def 1;
A12: ((|.(p . ((len p) -' 1)).| ") * |.(r + 1).|) * |.(p . ((len p) -' 1)).| = |.(r + 1).| * ((|.(p . ((len p) -' 1)).| ") * |.(p . ((len p) -' 1)).|)
.= |.(r + 1).| * 1 by A11, XCMPLX_0:def 7 ;
(eval ((NormPolynomial p),z)) * (p . ((len p) -' 1)) = ((eval (p,z)) / (p . ((len p) -' 1))) * (p . ((len p) -' 1)) by A1, POLYNOM5:58;
then (eval ((NormPolynomial p),z)) * (p . ((len p) -' 1)) = eval (p,z) by A10, VECTSP_2:22;
then |.(eval ((NormPolynomial p),z)).| * |.(p . ((len p) -' 1)).| = |.(eval (p,z)).| by COMPLEX1:65;
then ( |.(eval (p,z)).| >= |.(r + 1).| & |.(r + 1).| >= r + 1 ) by A12, A9, XREAL_1:64, ABSVALUE:4;
then ( |.(eval (p,z)).| >= r + 1 & r + 1 > r + 0 ) by XXREAL_0:2, XREAL_1:6;
hence |.(eval (p,z)).| > r by XXREAL_0:2; :: thesis: verum