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 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

per cases then ( len p = 2 or len p > 2 ) by XXREAL_0:1;

suppose 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

then A2: p = <%(p . 0),(p . 1)%> by Th38;
set N1 = |.(p . 1).|;
( p . ((len p) -' 1) <> 0. F_Complex & (len p) -' 1 = 2 - 1 ) by A1, UPROOTS:18, XREAL_1:233;
then A3: p . 1 <> 0 by COMPLFLD:def 1;
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
take e = ((|.(p . 1).| ") * |.r.|) + (|.(- (p . 0)).| * (|.(p . 1).| ")); :: 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 A4: e < |.z.| ; :: thesis: |.(eval (p,z)).| > r
A5: (((|.(p . 1).| ") * |.r.|) + (|.(- (p . 0)).| * (|.(p . 1).| "))) * |.(p . 1).| < |.z.| * |.(p . 1).| by A4, A3, XREAL_1:68;
A6: ((|.(p . 1).| ") * |.r.|) * |.(p . 1).| = |.r.| * ((|.(p . 1).| ") * |.(p . 1).|)
.= |.r.| * 1 by A3, XCMPLX_0:def 7 ;
A7: (|.(- (p . 0)).| * (|.(p . 1).| ")) * |.(p . 1).| = |.(- (p . 0)).| * ((|.(p . 1).| ") * |.(p . 1).|)
.= |.(- (p . 0)).| * 1 by A3, XCMPLX_0:def 7 ;
(((|.(p . 1).| ") * |.r.|) + (|.(- (p . 0)).| * (|.(p . 1).| "))) * |.(p . 1).| = |.r.| + |.(- (p . 0)).| by A6, A7;
then A8: |.r.| < (|.z.| * |.(p . 1).|) - |.(- (p . 0)).| by A5, XREAL_1:20;
reconsider z1 = z * (p . 1), z2 = - (p . 0) as Complex ;
A9: |.(z * (p . 1)).| - |.(- (p . 0)).| <= |.((z * (p . 1)) - (- (p . 0))).| by COMPLEX1:59;
A10: (z * (p . 1)) - (- (p . 0)) = (z * (p . 1)) + (- (- (p . 0)))
.= (z * (p . 1)) + (p . 0) ;
|.z.| * |.(p . 1).| = |.(z * (p . 1)).| by COMPLEX1:65;
then |.r.| < |.((z * (p . 1)) - (- (p . 0))).| by A8, A9, XXREAL_0:2;
then A11: |.r.| < |.(eval (p,z)).| by A2, POLYNOM5:44, A10;
r <= |.r.| by COMPLEX1:76;
hence |.(eval (p,z)).| > r by A11, XXREAL_0:2; :: thesis: verum

end;

suppose 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

hence for r being Real ex e being Real st
for z being Element of F_Complex st e < |.z.| holds
|.(eval (p,z)).| > r by Lm3; :: thesis: verum

end;

end;