let p be prime odd Nat; for m being positive Nat
for j being Element of F_Real st 0 < j & j <= m holds
eval ((~ (^ ((tau 0) |^ (p -' 1)))),j) <= m |^ (p -' 1)
let m be positive Nat; for j being Element of F_Real st 0 < j & j <= m holds
eval ((~ (^ ((tau 0) |^ (p -' 1)))),j) <= m |^ (p -' 1)
let j be Element of F_Real; ( 0 < j & j <= m implies eval ((~ (^ ((tau 0) |^ (p -' 1)))),j) <= m |^ (p -' 1) )
assume A1:
( 0 < j & j <= m )
; eval ((~ (^ ((tau 0) |^ (p -' 1)))),j) <= m |^ (p -' 1)
1 < p
by INT_2:def 4;
then A3:
p -' 1 = p - 1
by XREAL_1:233;
set p1 = p - 1;
reconsider m0 = m as Element of F_Real by NUMBERS:15, INT_1:def 2;
A4: m to_power (p - 1) =
(power F_Real) . (m0,(p - 1))
by Lm19
.=
m0 |^ (p - 1)
by BINOM:def 2
.=
m |^ (p -' 1)
by A3, Lm16
;
eval ((~ (^ ((tau 0) |^ (p -' 1)))),j) =
j |^ (p -' 1)
by Th40
.=
(power F_Real) . (j,(p - 1))
by A3, BINOM:def 2
.=
j to_power (p - 1)
by A1, Lm19
;
hence
eval ((~ (^ ((tau 0) |^ (p -' 1)))),j) <= m |^ (p -' 1)
by A4, A1, ASYMPT_1:64; verum