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 ) & ( 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)))) ) holds
- (((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= Sum (delta (m,p,g,z0))
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 ) & ( 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)))) ) holds
- (((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= Sum (delta (m,p,g,z0))
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 ) & ( 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)))) ) holds
- (((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= Sum (delta (m,p,g,z0))
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 ) & ( 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)))) ) holds
- (((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= Sum (delta (m,p,g,z0))
let M be Nat; :: thesis: ( z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) & ( 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)))) ) implies - (((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= Sum (delta (m,p,g,z0)) )
assume A1: ( z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) & ( 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: - (((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= Sum (delta (m,p,g,z0))
set r = (M * (z0 to_power m)) * (m |^ (p * (m + 1)));
- (m * ((M * (z0 to_power m)) * (m |^ (p * (m + 1))))) <= Sum (delta (m,p,g,z0))

proof

A3: for i being Nat st i in Seg m holds
- ((M * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= (delta (m,p,g,z0)) . i

proof

let i be Nat; :: thesis: ( i in Seg m implies - ((M * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= (delta (m,p,g,z0)) . i )
assume A4: i in Seg m ; :: thesis: - ((M * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= (delta (m,p,g,z0)) . i
then (delta (m,p,g,z0)) . i = ((delta_1 (m,p,g)) . i) + ((delta_2 (m,p,g,z0)) . i) by Lm24;
then A5: - |.(((delta_1 (m,p,g)) . i) + ((delta_2 (m,p,g,z0)) . i)).| <= (delta (m,p,g,z0)) . i by ABSVALUE:4;
- ((M * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= - |.(((delta_1 (m,p,g)) . i) + ((delta_2 (m,p,g,z0)) . i)).| by A1, A4, XREAL_1:24;
hence - ((M * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= (delta (m,p,g,z0)) . i by A5, XXREAL_0:2; :: thesis: verum

end;

Seg (len (delta (m,p,g,z0))) = dom (delta (m,p,g,z0)) by FINSEQ_1:def 3
.= dom (delta_1 (m,p,g)) by BINOM:def 1
.= Seg (len (delta_1 (m,p,g))) by FINSEQ_1:def 3 ;
then A7: len (delta (m,p,g,z0)) = len (delta_1 (m,p,g)) by FINSEQ_1:6
.= m by Def5 ;
reconsider r0 = - ((M * (z0 to_power m)) * (m |^ (p * (m + 1)))) as Element of F_Real by XREAL_0:def 1;
A8: m * (- ((M * (z0 to_power m)) * (m |^ (p * (m + 1))))) = m * (In ((- ((M * (z0 to_power m)) * (m |^ (p * (m + 1))))),F_Real)) by Lm26
.= m * r0 ;
set h = m |-> r0;
A9: for i being Nat st i in Seg m holds
(m |-> r0) . i <= (delta (m,p,g,z0)) . i

proof

let i be Nat; :: thesis: ( i in Seg m implies (m |-> r0) . i <= (delta (m,p,g,z0)) . i )
assume A10: i in Seg m ; :: thesis: (m |-> r0) . i <= (delta (m,p,g,z0)) . i
then (m |-> r0) . i = - ((M * (z0 to_power m)) * (m |^ (p * (m + 1)))) by FUNCOP_1:7;
hence (m |-> r0) . i <= (delta (m,p,g,z0)) . i by A10, A3; :: thesis: verum

end;

A12: dom (m |-> r0) = Seg m ;
len (delta (m,p,g,z0)) = len (m |-> r0) by A7;
then Sum (m |-> r0) <= Sum (delta (m,p,g,z0)) by A9, A12, E_TRANS1:2;
hence - (m * ((M * (z0 to_power m)) * (m |^ (p * (m + 1))))) <= Sum (delta (m,p,g,z0)) by A8, Th3; :: thesis: verum

end;

hence - (((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= Sum (delta (m,p,g,z0)) ; :: thesis: verum