let p be prime odd Nat; for m being positive Nat holds eval ((~ (((Der1 INT.Ring) |^ (p -' 1)) . (f_0 (m,p)))),(0. INT.Ring)) = ((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))
let m be positive Nat; eval ((~ (((Der1 INT.Ring) |^ (p -' 1)) . (f_0 (m,p)))),(0. INT.Ring)) = ((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))
set D = Der1 INT.Ring;
set ProdX = Product (x. (m,p));
set t0 = tau 0;
set F0 = f_0 (m,p);
A1:
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
( p -' 2 = p - 2 & p -' 1 = p - 1 )
by A1, XREAL_1:233;
then reconsider p1 = p -' 1 as non zero Element of NAT ;
reconsider f = Product (x. (m,p)) as Element of the carrier of (Polynom-Ring INT.Ring) ;
A3: eta (p1,p1) =
(p1 !) / (0 !)
by XREAL_1:232
.=
p1 !
by NEWTON:12
;
A4: (~ (((tau 0) |^ p1) * f)) . p1 =
((~ ((tau 0) |^ (p -' 1))) *' f) . (0 + p1)
by POLYNOM3:def 10
.=
(~ f) . 0
by Lm6
.=
In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring)
by Th20
;
(((Der1 INT.Ring) |^ p1) . (f_0 (m,p))) . 0 =
(eta ((0 + p1),p1)) * ((f_0 (m,p)) . (0 + p1))
by E_TRANS1:22
.=
((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))
by A3, A4, GROUP_4:6
;
hence
eval ((~ (((Der1 INT.Ring) |^ (p -' 1)) . (f_0 (m,p)))),(0. INT.Ring)) = ((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))
by POLYNOM5:31; verum