let p be prime odd Nat; :: thesis: for m being positive Nat
for x being Element of F_Real st 0 < x & x <= m holds
for i being Nat st i in Seg m holds
|.(eval ((~ (^ ((x. (m,p)) /. i))),x)).| <= m |^ p
let m be positive Nat; :: thesis: for x being Element of F_Real st 0 < x & x <= m holds
for i being Nat st i in Seg m holds
|.(eval ((~ (^ ((x. (m,p)) /. i))),x)).| <= m |^ p
let x be Element of F_Real; :: thesis: ( 0 < x & x <= m implies for i being Nat st i in Seg m holds
|.(eval ((~ (^ ((x. (m,p)) /. i))),x)).| <= m |^ p )
set PRI = Polynom-Ring INT.Ring;
set PRF = Polynom-Ring F_Real;
set FR = F_Real ;
assume A1: ( 0 < x & x <= m ) ; :: thesis: for i being Nat st i in Seg m holds
|.(eval ((~ (^ ((x. (m,p)) /. i))),x)).| <= m |^ p
let i be Nat; :: thesis: ( i in Seg m implies |.(eval ((~ (^ ((x. (m,p)) /. i))),x)).| <= m |^ p )
assume A2: i in Seg m ; :: thesis: |.(eval ((~ (^ ((x. (m,p)) /. i))),x)).| <= m |^ p
A3: dom (x. (m,p)) = Seg (len (x. (m,p))) by FINSEQ_1:def 3
.= Seg m by Def2 ;
then A4: (x. (m,p)) /. i = (x. (m,p)) . i by A2, PARTFUN1:def 6
.= (tau i) |^ p by A2, A3, Def2 ;
A5: Polynom-Ring INT.Ring is Subring of Polynom-Ring F_Real by FIELD_4:def 1;
p in NAT by ORDINAL1:def 12;
then A6: ^ ((tau i) |^ p) = (^ (tau i)) |^ p by A5, FIELD_6:19;
reconsider ui = tau i as Polynomial of F_Real by FIELD_4:8;
A7: (^ (tau i)) |^ p = ui `^ p by RINGDER1:37;
reconsider z0 = - i as Element of F_Real by XREAL_0:def 1;
A8: eval (ui,x) = eval (<%(In ((- i),F_Real)),(1. F_Real)%>,x)
.= z0 + ((1. F_Real) * x) by POLYNOM5:44
.= z0 + x ;
A9: eval ((~ (^ ((x. (m,p)) /. i))),x) = (power F_Real) . ((eval (ui,x)),p) by A6, A4, A7, POLYNOM5:22
.= (z0 + x) |^ p by A8, BINOM:def 2 ;
|.(i - x).| = |.(- (i - x)).| by COMPLEX1:52
.= |.(z0 + x).| ;
then A10: |.(z0 + x).| <= m by Lm15, A1, A2;
|.((z0 + x) |^ p).| <= m |^ p

proof

per cases ( |.(z0 + x).| <> 0 or |.(z0 + x).| = 0 ) ;

suppose A11: |.(z0 + x).| <> 0 ; :: thesis: |.((z0 + x) |^ p).| <= m |^ p

then A12: z0 + x <> 0. F_Real ;
|.((z0 + x) |^ p).| = |.(power ((z0 + x),p)).| by BINOM:def 2
.= |.(z0 + x).| to_power p by A12, Lm14 ;
hence |.((z0 + x) |^ p).| <= m |^ p by A11, PREPOWER:9, A10; :: thesis: verum

end;

suppose |.(z0 + x).| = 0 ; :: thesis: |.((z0 + x) |^ p).| <= m |^ p

then z0 + x = 0. F_Real ;
hence |.((z0 + x) |^ p).| <= m |^ p ; :: thesis: verum

end;

end;

end;

hence |.(eval ((~ (^ ((x. (m,p)) /. i))),x)).| <= m |^ p by A9; :: thesis: verum