let p be prime odd Nat; :: thesis: for m being positive Nat
for k being Element of F_Real st 0 < k & k <= m holds
|.((Eval (~ (^ (f_0 (m,p))))) . k).| <= m |^ ((p * m) + (p -' 1))
let m be positive Nat; :: thesis: for k being Element of F_Real st 0 < k & k <= m holds
|.((Eval (~ (^ (f_0 (m,p))))) . k).| <= m |^ ((p * m) + (p -' 1))
let k be Element of F_Real; :: thesis: ( 0 < k & k <= m implies |.((Eval (~ (^ (f_0 (m,p))))) . k).| <= m |^ ((p * m) + (p -' 1)) )
set t1 = eval ((~ (^ (Product (x. (m,p))))),k);
set t2 = eval ((~ (^ ((tau 0) |^ (p -' 1)))),k);
assume A1: ( 0 < k & k <= m ) ; :: thesis: |.((Eval (~ (^ (f_0 (m,p))))) . k).| <= m |^ ((p * m) + (p -' 1))
A2: 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;
eval ((~ (^ ((tau 0) |^ (p -' 1)))),k) = k |^ (p -' 1) by Th40
.= (power F_Real) . (k,(p - 1)) by A3, BINOM:def 2
.= k to_power (p - 1) by A1, Lm19 ;
then A5: |.(eval ((~ (^ ((tau 0) |^ (p -' 1)))),k)).| = eval ((~ (^ ((tau 0) |^ (p -' 1)))),k) by A1, ABSVALUE:def 1;
A6: eval ((~ (^ ((tau 0) |^ (p -' 1)))),k) <= m |^ (p -' 1) by A1, Lm20;
A7: |.((Eval (~ (^ (f_0 (m,p))))) . k).| = |.((eval ((~ (^ (Product (x. (m,p))))),k)) * (eval ((~ (^ ((tau 0) |^ (p -' 1)))),k))).| by Th35
.= |.(eval ((~ (^ (Product (x. (m,p))))),k)).| * |.(eval ((~ (^ ((tau 0) |^ (p -' 1)))),k)).| by COMPLEX1:65 ;
|.(eval ((~ (^ (Product (x. (m,p))))),k)).| <= m |^ (p * m) by A1, Lm17;
then A8: |.(eval ((~ (^ (Product (x. (m,p))))),k)).| * |.(eval ((~ (^ ((tau 0) |^ (p -' 1)))),k)).| <= (m |^ (p * m)) * |.(eval ((~ (^ ((tau 0) |^ (p -' 1)))),k)).| by XREAL_1:64;
A9: (m |^ (p * m)) * |.(eval ((~ (^ ((tau 0) |^ (p -' 1)))),k)).| <= (m |^ (p * m)) * (m |^ (p -' 1)) by XREAL_1:66, A6, A5;
set pm = p * m;
(m |^ (p * m)) * (m |^ (p -' 1)) = (m to_power (p * m)) * (m to_power (p - 1)) by A2, XREAL_1:233
.= m to_power ((p * m) + (p - 1)) by POWER:27
.= m |^ ((p * m) + (p -' 1)) by A2, XREAL_1:233 ;
hence |.((Eval (~ (^ (f_0 (m,p))))) . k).| <= m |^ ((p * m) + (p -' 1)) by A7, A8, A9, XXREAL_0:2; :: thesis: verum