let p be Polynomial of F_Complex ; :: thesis: ( len p > 2 & |.(p . ((len p) -' 1)).| = 1 implies for F being FinSequence of REAL st len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ) holds
for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval p,z).| > |.(p . 0 ).| + 1 )
assume that
A1: len p > 2 and
A2: |.(p . ((len p) -' 1)).| = 1 ; :: thesis: for F being FinSequence of REAL st len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ) holds
for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval p,z).| > |.(p . 0 ).| + 1
let F be FinSequence of REAL ; :: thesis: ( len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ) implies for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval p,z).| > |.(p . 0 ).| + 1 )
assume that
A3: len F = len p and
A4: for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ; :: thesis: for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval p,z).| > |.(p . 0 ).| + 1
set lF1 = (len F) -' 1;
A5: ((len F) -' 1) + 1 = len F by A1, A3, XREAL_1:237, XXREAL_0:2;
then A6: F = F | (((len F) -' 1) + 1) by FINSEQ_1:79
.= (F | ((len F) -' 1)) ^ <*(F /. (((len F) -' 1) + 1))*> by A5, FINSEQ_5:85 ;
A7: len p > 1 by A1, XXREAL_0:2;
then A8: 1 in dom F by A3, FINSEQ_3:27;
A9: now
let n be Element of NAT ; :: thesis: ( n in dom (F | ((len F) -' 1)) implies (F | ((len F) -' 1)) . n >= 0 )
A10: dom (F | ((len F) -' 1)) c= dom F by FINSEQ_5:20;
assume A11: n in dom (F | ((len F) -' 1)) ; :: thesis: (F | ((len F) -' 1)) . n >= 0
then (F | ((len F) -' 1)) . n = (F | ((len F) -' 1)) /. n by PARTFUN1:def 8
.= F /. n by A11, FINSEQ_4:85
.= F . n by A11, A10, PARTFUN1:def 8
.= |.(p . (n -' 1)).| by A4, A11, A10 ;
hence (F | ((len F) -' 1)) . n >= 0 by COMPLEX1:132; :: thesis: verum
end;
A12: len (F | ((len F) -' 1)) = (len F) -' 1 by A5, FINSEQ_1:80, NAT_1:11;
|.(p . 0 ).| >= 0 by COMPLEX1:132;
then A13: |.(p . 0 ).| + 1 >= 0 + 1 by XREAL_1:8;
let z be Element of F_Complex ; :: thesis: ( |.z.| > Sum F implies |.(eval p,z).| > |.(p . 0 ).| + 1 )
consider G being FinSequence of the carrier of F_Complex such that
A14: eval p,z = Sum G and
A15: len G = len p and
A16: for n being Element of NAT st n in dom G holds
G . n = (p . (n -' 1)) * ((power F_Complex ) . z,(n -' 1)) by POLYNOM4:def 2;
set lF2 = (len F) -' 2;
assume A17: |.z.| > Sum F ; :: thesis: |.(eval p,z).| > |.(p . 0 ).| + 1
A18: len F in dom F by A7, A3, FINSEQ_3:27;
then F /. (((len F) -' 1) + 1) = F . (((len F) -' 1) + 1) by A5, PARTFUN1:def 8
.= 1 by A2, A3, A4, A5, A18 ;
then A19: Sum F = (Sum (F | ((len F) -' 1))) + 1 by A6, RVSUM_1:104;
A20: len F >= (1 + 1) + 0 by A1, A3;
then (len F) -' 1 >= 1 by A5, XREAL_1:8;
then A21: 1 in dom (F | ((len F) -' 1)) by A12, FINSEQ_3:27;
then (F | ((len F) -' 1)) . 1 = (F | ((len F) -' 1)) /. 1 by PARTFUN1:def 8
.= F /. 1 by A21, FINSEQ_4:85
.= F . 1 by A8, PARTFUN1:def 8
.= |.(p . (1 -' 1)).| by A4, A8
.= |.(p . 0 ).| by XREAL_1:234 ;
then Sum (F | ((len F) -' 1)) >= |.(p . 0 ).| by A21, A9, Th4;
then A22: Sum F >= |.(p . 0 ).| + 1 by A19, XREAL_1:8;
then A23: z <> 0. F_Complex by A17, A13, COMPLFLD:96;
G = G | (((len F) -' 1) + 1) by A3, A15, A5, FINSEQ_1:79
.= (G | ((len F) -' 1)) ^ <*(G /. (((len F) -' 1) + 1))*> by A3, A15, A5, FINSEQ_5:85 ;
then A24: Sum G = (Sum (G | ((len F) -' 1))) + (G /. (((len F) -' 1) + 1)) by FVSUM_1:87;
A25: dom F = dom G by A3, A15, FINSEQ_3:31;
then G /. (((len F) -' 1) + 1) = G . (((len F) -' 1) + 1) by A5, A18, PARTFUN1:def 8
.= (p . ((len F) -' 1)) * ((power F_Complex ) . z,((len F) -' 1)) by A16, A5, A18, A25 ;
then |.(G /. (((len F) -' 1) + 1)).| = 1 * |.((power F_Complex ) . z,((len F) -' 1)).| by A2, A3, COMPLFLD:109;
then A26: |.(eval p,z).| >= |.((power F_Complex ) . z,((len F) -' 1)).| - |.(Sum (G | ((len F) -' 1))).| by A14, A24, COMPLFLD:102;
1 = 1 + 0 ;
then A27: (len F) - 1 >= 0 by A7, A3, XREAL_1:21;
A28: len (F | ((len F) -' 1)) = (len F) -' 1 by A5, FINSEQ_1:80, NAT_1:11
.= len (G | ((len F) -' 1)) by A3, A15, A5, FINSEQ_1:80, NAT_1:11 ;
then A29: ( (F | ((len F) -' 1)) | (len (F | ((len F) -' 1))) = F | ((len F) -' 1) & (G | ((len F) -' 1)) | (len (F | ((len F) -' 1))) = G | ((len F) -' 1) ) by FINSEQ_1:79;
defpred S1[ Element of NAT ] means |.(Sum ((G | ((len F) -' 1)) | $1)).| <= (Sum ((F | ((len F) -' 1)) | $1)) * |.((power F_Complex ) . z,((len F) -' 2)).|;
(len F) - 2 >= 0 by A20, XREAL_1:21;
then A30: ((len F) -' 2) + 1 = ((len F) - 2) + 1 by XREAL_0:def 2
.= (len F) -' 1 by A27, XREAL_0:def 2 ;
then (power F_Complex ) . z,((len F) -' 1) = ((power F_Complex ) . z,((len F) -' 2)) * z by GROUP_1:def 8;
then A31: |.((power F_Complex ) . z,((len F) -' 1)).| - (|.((power F_Complex ) . z,((len F) -' 2)).| * (Sum (F | ((len F) -' 1)))) = (|.((power F_Complex ) . z,((len F) -' 2)).| * |.z.|) - (|.((power F_Complex ) . z,((len F) -' 2)).| * (Sum (F | ((len F) -' 1)))) by COMPLFLD:109
.= |.((power F_Complex ) . z,((len F) -' 2)).| * (|.z.| - (Sum (F | ((len F) -' 1)))) ;
A32: |.z.| > |.(p . 0 ).| + 1 by A17, A22, XXREAL_0:2;
then A33: |.z.| > 1 by A13, XXREAL_0:2;
A34: dom (F | ((len F) -' 1)) = dom (G | ((len F) -' 1)) by A28, FINSEQ_3:31;
A35: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A36: |.(Sum ((G | ((len F) -' 1)) | n)).| <= (Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex ) . z,((len F) -' 2)).| ; :: thesis: S1[n + 1]
then A37: |.(Sum ((G | ((len F) -' 1)) | n)).| + |.((G | ((len F) -' 1)) /. (n + 1)).| <= ((Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex ) . z,((len F) -' 2)).|) + |.((G | ((len F) -' 1)) /. (n + 1)).| by XREAL_1:8;
per cases ( n + 1 <= len (G | ((len F) -' 1)) or n + 1 > len (G | ((len F) -' 1)) ) ;
suppose A38: n + 1 <= len (G | ((len F) -' 1)) ; :: thesis: S1[n + 1]
then n + 1 <= ((len F) -' 2) + 1 by A3, A15, A5, A30, FINSEQ_1:80, NAT_1:11;
then n <= (len F) -' 2 by XREAL_1:8;
then |.z.| to_power n <= |.z.| to_power ((len F) -' 2) by A33, PRE_FF:10;
then |.z.| to_power n <= |.((power F_Complex ) . z,((len F) -' 2)).| by A23, Th8;
then A39: ( |.(p . n).| >= 0 & |.((power F_Complex ) . z,n).| <= |.((power F_Complex ) . z,((len F) -' 2)).| ) by A23, Th8, COMPLEX1:132;
(G | ((len F) -' 1)) | (n + 1) = ((G | ((len F) -' 1)) | n) ^ <*((G | ((len F) -' 1)) /. (n + 1))*> by A38, FINSEQ_5:85;
then Sum ((G | ((len F) -' 1)) | (n + 1)) = (Sum ((G | ((len F) -' 1)) | n)) + ((G | ((len F) -' 1)) /. (n + 1)) by FVSUM_1:87;
then |.(Sum ((G | ((len F) -' 1)) | (n + 1))).| <= |.(Sum ((G | ((len F) -' 1)) | n)).| + |.((G | ((len F) -' 1)) /. (n + 1)).| by COMPLFLD:100;
then A40: |.(Sum ((G | ((len F) -' 1)) | (n + 1))).| <= ((Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex ) . z,((len F) -' 2)).|) + |.((G | ((len F) -' 1)) /. (n + 1)).| by A37, XXREAL_0:2;
A41: dom (G | ((len F) -' 1)) c= dom G by FINSEQ_5:20;
n + 1 >= 1 by NAT_1:11;
then A42: n + 1 in dom (G | ((len F) -' 1)) by A38, FINSEQ_3:27;
then A43: (F | ((len F) -' 1)) /. (n + 1) = F /. (n + 1) by A34, FINSEQ_4:85
.= F . (n + 1) by A25, A42, A41, PARTFUN1:def 8
.= |.(p . ((n + 1) -' 1)).| by A4, A25, A42, A41
.= |.(p . n).| by NAT_D:34 ;
(G | ((len F) -' 1)) /. (n + 1) = G /. (n + 1) by A42, FINSEQ_4:85
.= G . (n + 1) by A42, A41, PARTFUN1:def 8
.= (p . ((n + 1) -' 1)) * ((power F_Complex ) . z,((n + 1) -' 1)) by A16, A42, A41
.= (p . n) * ((power F_Complex ) . z,((n + 1) -' 1)) by NAT_D:34
.= (p . n) * ((power F_Complex ) . z,n) by NAT_D:34 ;
then |.((G | ((len F) -' 1)) /. (n + 1)).| = ((F | ((len F) -' 1)) /. (n + 1)) * |.((power F_Complex ) . z,n).| by A43, COMPLFLD:109;
then |.((G | ((len F) -' 1)) /. (n + 1)).| <= ((F | ((len F) -' 1)) /. (n + 1)) * |.((power F_Complex ) . z,((len F) -' 2)).| by A43, A39, XREAL_1:66;
then A44: ((Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex ) . z,((len F) -' 2)).|) + |.((G | ((len F) -' 1)) /. (n + 1)).| <= ((Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex ) . z,((len F) -' 2)).|) + (((F | ((len F) -' 1)) /. (n + 1)) * |.((power F_Complex ) . z,((len F) -' 2)).|) by XREAL_1:8;
(F | ((len F) -' 1)) | (n + 1) = ((F | ((len F) -' 1)) | n) ^ <*((F | ((len F) -' 1)) /. (n + 1))*> by A28, A38, FINSEQ_5:85;
then Sum ((F | ((len F) -' 1)) | (n + 1)) = (Sum ((F | ((len F) -' 1)) | n)) + ((F | ((len F) -' 1)) /. (n + 1)) by RVSUM_1:104;
hence S1[n + 1] by A40, A44, XXREAL_0:2; :: thesis: verum
end;
suppose A45: n + 1 > len (G | ((len F) -' 1)) ; :: thesis: S1[n + 1]
then n >= len (G | ((len F) -' 1)) by NAT_1:13;
then A46: ( (G | ((len F) -' 1)) | n = G | ((len F) -' 1) & (F | ((len F) -' 1)) | n = F | ((len F) -' 1) ) by A28, FINSEQ_1:79;
(G | ((len F) -' 1)) | (n + 1) = G | ((len F) -' 1) by A45, FINSEQ_1:79;
hence S1[n + 1] by A28, A36, A45, A46, FINSEQ_1:79; :: thesis: verum
end;
end;
end;
(G | ((len F) -' 1)) | 0 = <*> the carrier of F_Complex ;
then A47: S1[ 0 ] by COMPLFLD:93, RLVECT_1:60, RVSUM_1:102;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A47, A35);
 then |.(Sum (G | ((len F) -' 1))).| <= (Sum (F | ((len F) -' 1))) * |.((power F_Complex ) . z,((len F) -' 2)).| by A29;
then |.((power F_Complex ) . z,((len F) -' 1)).| - |.(Sum (G | ((len F) -' 1))).| >= |.((power F_Complex ) . z,((len F) -' 1)).| - ((Sum (F | ((len F) -' 1))) * |.((power F_Complex ) . z,((len F) -' 2)).|) by XREAL_1:15;
then A48: |.(eval p,z).| >= |.((power F_Complex ) . z,((len F) -' 1)).| - (|.((power F_Complex ) . z,((len F) -' 2)).| * (Sum (F | ((len F) -' 1)))) by A26, XXREAL_0:2;
len F >= 2 + 1 by A1, A3, NAT_1:13;
then (len F) - 2 >= 1 by XREAL_1:21;
then (len F) -' 2 >= 1 by XREAL_0:def 2;
then |.z.| to_power ((len F) -' 2) >= |.z.| to_power 1 by A33, PRE_FF:10;
then |.((power F_Complex ) . z,((len F) -' 2)).| >= |.z.| to_power 1 by A23, Th8;
then |.((power F_Complex ) . z,((len F) -' 2)).| >= |.((power F_Complex ) . z,1).| by A23, Th8;
then A49: |.((power F_Complex ) . z,((len F) -' 2)).| >= |.z.| by GROUP_1:98;
( |.((power F_Complex ) . z,((len F) -' 2)).| >= 0 & |.z.| - (Sum (F | ((len F) -' 1))) > 1 ) by A17, A19, COMPLEX1:132, XREAL_1:22;
then |.((power F_Complex ) . z,((len F) -' 2)).| * (|.z.| - (Sum (F | ((len F) -' 1)))) >= |.((power F_Complex ) . z,((len F) -' 2)).| * 1 by XREAL_1:66;
then |.(eval p,z).| >= |.((power F_Complex ) . z,((len F) -' 2)).| by A48, A31, XXREAL_0:2;
then |.(eval p,z).| >= |.z.| by A49, XXREAL_0:2;
hence |.(eval p,z).| > |.(p . 0 ).| + 1 by A32, XXREAL_0:2; :: thesis: verum