let p be prime odd Nat; :: thesis: for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) holds
for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1))))
let m be positive Nat; :: thesis: for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) holds
for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1))))
let g be non zero Polynomial of INT.Ring; :: thesis: for z0 being non zero Element of F_Real
for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) holds
for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1))))
let z0 be non zero Element of F_Real; :: thesis: for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) holds
for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1))))
let M be Nat; :: thesis: ( z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) implies for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1)))) )
assume A1: ( z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) ) ; :: thesis: for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1))))
for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1))))

proof

let k be Nat; :: thesis: ( k in Seg m implies |.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1)))) )
assume A2: k in Seg m ; :: thesis: |.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1))))
then A4: ( 1 <= k & k <= m ) by FINSEQ_1:1;
A3: p > 1 by INT_2:def 4;
A5: len (delta_1 (m,p,g)) = m by Def5;
len (delta_2 (m,p,g,z0)) = m by Def6;
then A7: ( k in dom (delta_1 (m,p,g)) & k in dom (delta_2 (m,p,g,z0)) ) by A2, A5, FINSEQ_1:def 3;
set kr = In (k,F_Real);
(delta_2 (m,p,g,z0)) . k = - ((g . k) * (((power F_Real) . (z0,k)) * (('F' (f_0 (m,p))) . 0))) by A7, Def6;
then A9: ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) = ((g . k) * (('F' (f_0 (m,p))) . (In (k,F_Real)))) - ((g . k) * (((power F_Real) . (z0,k)) * (('F' (f_0 (m,p))) . 0))) by A7, Def5
.= (g . k) * ((('F' (f_0 (m,p))) . (In (k,F_Real))) - (((power F_Real) . (z0,k)) * (('F' (f_0 (m,p))) . 0))) ;
A10: (('F' (f_0 (m,p))) . (In (k,F_Real))) - (((power F_Real) . (z0,k)) * (('F' (f_0 (m,p))) . 0)) = (('F' (f_0 (m,p))) . (In (k,F_Real))) - ((exp_R . (In (k,F_Real))) * (('F' (f_0 (m,p))) . 0)) by A1, Lm13;
reconsider k0 = In (k,F_Real) as positive Real by A2, FINSEQ_1:1;
len (f_0 (m,p)) = len (~ (f_0 (m,p)))
.= (m * p) + p by Th12 ;
then consider s being Real such that
A12: ( 0 < s & s < 1 & (('F' (f_0 (m,p))) . k0) - ((exp_R . k0) * (('F' (f_0 (m,p))) . 0)) = - ((k0 * (exp_R . (k0 * (1 - s)))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0))) ) by E_TRANS1:34;
set t = |.(- ((k0 * (exp_R . (k0 * (1 - s)))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0)))).|;
A13: |.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| = |.(g . k).| * |.(- ((k0 * (exp_R . (k0 * (1 - s)))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0)))).| by A12, A10, A9, COMPLEX1:65;
A14: |.(g . k).| * |.(- ((k0 * (exp_R . (k0 * (1 - s)))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0)))).| <= M * |.(- ((k0 * (exp_R . (k0 * (1 - s)))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0)))).| by A1, XREAL_1:64;
set u = |.(- (k0 * (z0 to_power (k0 * (1 - s))))).|;
set v = |.((Eval (~ (^ (f_0 (m,p))))) . (s * k0)).|;
1 < z0 by A1, XXREAL_0:2, TAYLOR_1:11;
then A16: |.(- (k0 * (z0 to_power (k0 * (1 - s))))).| <= m * (z0 to_power m) by A4, A12, Lm22;
exp_R . (k0 * (1 - s)) = z0 to_power (k0 * (1 - s)) by A1, TAYLOR_1:10;
then |.(- ((k0 * (exp_R . (k0 * (1 - s)))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0)))).| = |.((- (k0 * (z0 to_power (k0 * (1 - s))))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0))).|
.= |.(- (k0 * (z0 to_power (k0 * (1 - s))))).| * |.((Eval (~ (^ (f_0 (m,p))))) . (s * k0)).| by COMPLEX1:65 ;
then A17: |.(- ((k0 * (exp_R . (k0 * (1 - s)))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0)))).| <= (m * (z0 to_power m)) * |.((Eval (~ (^ (f_0 (m,p))))) . (s * k0)).| by A16, XREAL_1:64;
reconsider sk = s * k0 as Element of F_Real by XREAL_0:def 1;
( 0 < s & 0 < k0 & s < 1 & k0 <= m & s < 1 ) by A2, FINSEQ_1:1, A12;
then A18: s * k0 < m * 1 by XREAL_1:98;
A20: ((p * m) + (p -' 1)) + 1 = ((p * m) + (p - 1)) + 1 by A3, XREAL_1:233
.= p * (m + 1) ;
( 0 < sk & sk <= m ) by A12, A18;
then |.((Eval (~ (^ (f_0 (m,p))))) . (s * k0)).| <= m |^ ((p * m) + (p -' 1)) by Lm21;
then A21: (m * (z0 to_power m)) * |.((Eval (~ (^ (f_0 (m,p))))) . (s * k0)).| <= (m * (z0 to_power m)) * (m |^ ((p * m) + (p -' 1))) by A1, TAYLOR_1:11, XREAL_1:64;
(m * (z0 to_power m)) * (m |^ ((p * m) + (p -' 1))) = (z0 to_power m) * (m * (m |^ ((p * m) + (p -' 1))))
.= (z0 to_power m) * (m |^ (p * (m + 1))) by A20, NEWTON:6 ;
then |.(- ((k0 * (exp_R . (k0 * (1 - s)))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0)))).| <= (z0 to_power m) * (m |^ (p * (m + 1))) by A21, XXREAL_0:2, A17;
then M * |.(- ((k0 * (exp_R . (k0 * (1 - s)))) * ((Eval (~ (^ (f_0 (m,p))))) . (s * k0)))).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1)))) by XREAL_1:64;
hence |.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1)))) by A13, A14, XXREAL_0:2; :: thesis: verum

end;

hence for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1)))) ; :: thesis: verum