theorem Th39: :: E_TRANS2:36

for p being prime odd Nat
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