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:235, XXREAL_0:2;
then A6: F = F | (((len F) -' 1) + 1) by FINSEQ_1:58
.= (F | ((len F) -' 1)) ^ <*(F /. (((len F) -' 1) + 1))*> by A5, FINSEQ_5:82 ;
A7: len p > 1 by A1, XXREAL_0:2;
then A8: 1 in dom F by A3, FINSEQ_3:25;
A9: now :: thesis: for n being Element of NAT st n in dom (F | ((len F) -' 1)) holds
(F | ((len F) -' 1)) . n >= 0
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:18;
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 6
.= F /. n by A11, FINSEQ_4:70
.= F . n by A11, A10, PARTFUN1:def 6
.= |.(p . (n -' 1)).| by A4, A11, A10 ;
hence (F | ((len F) -' 1)) . n >= 0 by COMPLEX1:46; :: thesis: verum
end;
A12: len (F | ((len F) -' 1)) = (len F) -' 1 by A5, FINSEQ_1:59, NAT_1:11;
|.(p . 0).| >= 0 by COMPLEX1:46;
then A13: |.(p . 0).| + 1 >= 0 + 1 by XREAL_1:6;
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:25;
then F /. (((len F) -' 1) + 1) = F . (((len F) -' 1) + 1) by A5, PARTFUN1:def 6
.= 1 by A2, A3, A4, A5, A18 ;
then A19: Sum F = (Sum (F | ((len F) -' 1))) + 1 by A6, RVSUM_1:74;
A20: len F >= (1 + 1) + 0 by A1, A3;
then (len F) -' 1 >= 1 by A5, XREAL_1:6;
then A21: 1 in dom (F | ((len F) -' 1)) by A12, FINSEQ_3:25;
then (F | ((len F) -' 1)) . 1 = (F | ((len F) -' 1)) /. 1 by PARTFUN1:def 6
.= F /. 1 by A21, FINSEQ_4:70
.= F . 1 by A8, PARTFUN1:def 6
.= |.(p . (1 -' 1)).| by A4, A8
.= |.(p . 0).| by XREAL_1:232 ;
then Sum (F | ((len F) -' 1)) >= |.(p . 0).| by A21, A9, Th4;
then A22: Sum F >= |.(p . 0).| + 1 by A19, XREAL_1:6;
then A23: z <> 0. F_Complex by A17, A13, COMPLFLD:59;
G = G | (((len F) -' 1) + 1) by A3, A15, A5, FINSEQ_1:58
.= (G | ((len F) -' 1)) ^ <*(G /. (((len F) -' 1) + 1))*> by A3, A15, A5, FINSEQ_5:82 ;
then A24: Sum G = (Sum (G | ((len F) -' 1))) + (G /. (((len F) -' 1) + 1)) by FVSUM_1:71;
A25: dom F = dom G by A3, A15, FINSEQ_3:29;
then G /. (((len F) -' 1) + 1) = G . (((len F) -' 1) + 1) by A5, A18, PARTFUN1:def 6
.= (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:71;
then A26: |.(eval (p,z)).| >= |.((power F_Complex) . (z,((len F) -' 1))).| - |.(Sum (G | ((len F) -' 1))).| by A14, A24, COMPLFLD:64;
A27: (len F) - 1 >= 0 by A7, A3;
A28: len (F | ((len F) -' 1)) = (len F) -' 1 by A5, FINSEQ_1:59, NAT_1:11
.= len (G | ((len F) -' 1)) by A3, A15, A5, FINSEQ_1:59, 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:58;
defpred S1[ 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:19;
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 7;
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:71
.= |.((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:29;
reconsider GG = G | ((len F) -' 1) as FinSequence of the carrier of F_Complex ;
reconsider FF = F | ((len F) -' 1) as FinSequence of REAL ;
A35: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
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 (GG | n)).| + |.(GG /. (n + 1)).| <= ((Sum (FF | n)) * |.((power F_Complex) . (z,((len F) -' 2))).|) + |.(GG /. (n + 1)).| by XREAL_1:6;
per cases ( n + 1 <= len (G | ((len F) -' 1)) or n + 1 > len GG ) ;
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:59, NAT_1:11;
then n <= (len F) -' 2 by XREAL_1:6;
then |.z.| to_power n <= |.z.| to_power ((len F) -' 2) by A33, PRE_FF:8;
then |.z.| to_power n <= |.(power (z,((len F) -' 2))).| by A23, Th7;
then A39: ( |.(p . nn).| >= 0 & |.(power (z,n)).| <= |.(power (z,((len F) -' 2))).| ) by A23, Th7, COMPLEX1:46;
GG | (n + 1) = (GG | n) ^ <*(GG /. (n + 1))*> by A38, FINSEQ_5:82;
then Sum (GG | (n + 1)) = (Sum (GG | n)) + (GG /. (n + 1)) by FVSUM_1:71;
then |.(Sum (GG | (n + 1))).| <= |.(Sum (GG | n)).| + |.(GG /. (n + 1)).| by COMPLFLD:62;
then A40: |.(Sum (GG | (n + 1))).| <= ((Sum (FF | n)) * |.((power F_Complex) . (z,((len F) -' 2))).|) + |.(GG /. (n + 1)).| by A37, XXREAL_0:2;
A41: dom GG c= dom G by FINSEQ_5:18;
n + 1 >= 1 by NAT_1:11;
then A42: n + 1 in dom GG by A38, FINSEQ_3:25;
then A43: (F | ((len F) -' 1)) /. (n + 1) = F /. (n + 1) by A34, FINSEQ_4:70
.= F . (n + 1) by A25, A42, A41, PARTFUN1:def 6
.= |.(p . ((n + 1) -' 1)).| by A4, A25, A42, A41
.= |.(p . nn).| by NAT_D:34 ;
GG /. (n + 1) = G /. (n + 1) by A42, FINSEQ_4:70
.= G . (n + 1) by A42, A41, PARTFUN1:def 6
.= (p . ((n + 1) -' 1)) * ((power F_Complex) . (z,((n + 1) -' 1))) by A16, A42, A41
.= (p . nn) * ((power F_Complex) . (z,((n + 1) -' 1))) by NAT_D:34
.= (p . nn) * ((power F_Complex) . (z,n)) by NAT_D:34 ;
then |.(GG /. (n + 1)).| = ((F | ((len F) -' 1)) /. (n + 1)) * |.((power F_Complex) . (z,n)).| by A43, COMPLFLD:71;
then |.(GG /. (n + 1)).| <= ((F | ((len F) -' 1)) /. (n + 1)) * |.((power F_Complex) . (z,((len F) -' 2))).| by A43, A39, XREAL_1:64;
then A44: ((Sum ((F | ((len F) -' 1)) | n)) * |.((power F_Complex) . (z,((len F) -' 2))).|) + |.(GG /. (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:6;
(F | ((len F) -' 1)) | (n + 1) = ((F | ((len F) -' 1)) | n) ^ <*((F | ((len F) -' 1)) /. (n + 1))*> by A28, A38, FINSEQ_5:82;
then Sum ((F | ((len F) -' 1)) | (n + 1)) = (Sum ((F | ((len F) -' 1)) | n)) + ((F | ((len F) -' 1)) /. (n + 1)) by RVSUM_1:74;
hence S1[n + 1] by A40, A44, XXREAL_0:2; :: thesis: verum
end;
suppose A45: n + 1 > len GG ; :: thesis: S1[n + 1]
then n >= len GG by NAT_1:13;
then A46: ( GG | n = GG & (F | ((len F) -' 1)) | n = F | ((len F) -' 1) ) by A28, FINSEQ_1:58;
GG | (n + 1) = GG by A45, FINSEQ_1:58;
hence S1[n + 1] by A28, A36, A45, A46, FINSEQ_1:58; :: thesis: verum
end;
end;
end;
(G | ((len F) -' 1)) | 0 = <*> the carrier of F_Complex ;
then A47: S1[ 0 ] by COMPLFLD:57, RLVECT_1:43, RVSUM_1:72;
for n being Nat holds S1[n] from NAT_1:sch 2(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:13;
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:19;
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:8;
then |.(power (z,((len F) -' 2))).| >= |.z.| to_power 1 by A23, Th7;
then |.((power F_Complex) . (z,((len F) -' 2))).| >= |.(power (z,1)).| by A23, Th7;
then A49: |.((power F_Complex) . (z,((len F) -' 2))).| >= |.z.| by GROUP_1:50;
( |.((power F_Complex) . (z,((len F) -' 2))).| >= 0 & |.z.| - (Sum (F | ((len F) -' 1))) > 1 ) by A17, A19, COMPLEX1:46, XREAL_1:20;
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:64;
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