let p be prime odd Nat; :: thesis: for m being positive Nat
for k being non zero Nat st p <= k holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = (k !) * ((~ (Product (x. (m,p)))) . (k -' (p -' 1)))
let m be positive Nat; :: thesis: for k being non zero Nat st p <= k holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = (k !) * ((~ (Product (x. (m,p)))) . (k -' (p -' 1)))
let k be non zero Nat; :: thesis: ( p <= k implies eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = (k !) * ((~ (Product (x. (m,p)))) . (k -' (p -' 1))) )
set D = Der1 INT.Ring;
set t0 = tau 0;
assume A1: p <= k ; :: thesis: eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = (k !) * ((~ (Product (x. (m,p)))) . (k -' (p -' 1)))
set F0 = f_0 (m,p);
A2: 1 < p by INT_2:def 4;
1 + 1 < p + 1 by INT_2:def 4, XREAL_1:6;
then 2 <= p by NAT_1:13;
then A5: ( p -' 2 = p - 2 & p -' 1 = p - 1 ) by A2, XREAL_1:233;
reconsider f = Product (x. (m,p)) as Element of the carrier of (Polynom-Ring INT.Ring) ;
reconsider p1 = p -' 1 as non zero Element of NAT by A5;
A6: 1 = p - (p - 1)
.= p - (p -' 1) by XREAL_1:233, A2 ;
then 1 <= k - (p -' 1) by A1, XREAL_1:6;
then reconsider kp = k - (p -' 1) as Element of NAT by INT_1:3;
A7: p - 1 < p by XREAL_1:44;
A8: eta (k,k) = (k !) / (0 !) by XREAL_1:232
.= k ! by NEWTON:12 ;
A9: (~ (((tau 0) |^ (p -' 1)) * f)) . k = ((~ ((tau 0) |^ p1)) *' f) . (kp + p1) by POLYNOM3:def 10
.= f . kp by Lm6 ;
(((Der1 INT.Ring) |^ k) . (f_0 (m,p))) . 0 = (eta ((0 + k),k)) * ((f_0 (m,p)) . (0 + k)) by E_TRANS1:22
.= (eta (k,k)) * (f . kp) by A9, GROUP_4:6
.= (k !) * (f . (k -' (p -' 1))) by A8, XREAL_1:233, A7, A6, A1, XXREAL_0:2 ;
hence eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = (k !) * ((~ (Product (x. (m,p)))) . (k -' (p -' 1))) by POLYNOM5:31; :: thesis: verum