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
Sum (delta (m,p,g,z0)) <= ((m * 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 ) & ( 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
Sum (delta (m,p,g,z0)) <= ((m * 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 ) & ( 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
Sum (delta (m,p,g,z0)) <= ((m * 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 ) & ( 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
Sum (delta (m,p,g,z0)) <= ((m * 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 ) & ( 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 Sum (delta (m,p,g,z0)) <= ((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1))) )
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: Sum (delta (m,p,g,z0)) <= ((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))
set r = (M * (z0 to_power m)) * (m |^ (p * (m + 1)));
Sum (delta (m,p,g,z0)) <= m * ((M * (z0 to_power m)) * (m |^ (p * (m + 1))))

proof

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

proof

let i be Nat; :: thesis: ( i in Seg m implies (delta (m,p,g,z0)) . i <= (M * (z0 to_power m)) * (m |^ (p * (m + 1))) )
assume A4: i in Seg m ; :: thesis: (delta (m,p,g,z0)) . i <= (M * (z0 to_power m)) * (m |^ (p * (m + 1)))
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 (m,p,g,z0)) . i <= |.(((delta_1 (m,p,g)) . i) + ((delta_2 (m,p,g,z0)) . i)).| by ABSVALUE:4;
|.(((delta_1 (m,p,g)) . i) + ((delta_2 (m,p,g,z0)) . i)).| <= (M * (z0 to_power m)) * (m |^ (p * (m + 1))) by A4, A1;
hence (delta (m,p,g,z0)) . i <= (M * (z0 to_power m)) * (m |^ (p * (m + 1))) 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 A6: 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;
A7: 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;
A8: for i being Nat st i in Seg m holds
(delta (m,p,g,z0)) . i <= (m |-> r0) . i

proof

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

end;

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

end;

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