let p be prime odd Nat; for m being positive Nat
for k, j being Nat st k < p & j in Seg m holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) = 0. INT.Ring
let m be positive Nat; for k, j being Nat st k < p & j in Seg m holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) = 0. INT.Ring
let k, j be Nat; ( k < p & j in Seg m implies eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) = 0. INT.Ring )
assume A1:
( k < p & j in Seg m )
; eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) = 0. INT.Ring
then
k < (p - 1) + 1
;
then A3:
( 0 <= k & k <= p - 1 )
by NAT_1:13;
set D = Der1 INT.Ring;
set tj = tau j;
set yj = Product (Del ((ff_0 (m,p)),j));
A4:
1 < p
by INT_2:def 4;
1 + 1 < p + 1
by XREAL_1:6, INT_2:def 4;
then
2 <= p
by NAT_1:13;
then
( p -' 2 = p - 2 & p -' 1 = p - 1 )
by A4, XREAL_1:233;
then reconsider p1 = p -' 1 as non zero Element of NAT ;
set f = Product (Del ((ff_0 (m,p)),j));
A6:
len (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) = k + 1
by RINGDER1:def 4;
then A7:
dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) = Seg (k + 1)
by FINSEQ_1:def 3;
reconsider lbz = LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p)) as non empty FinSequence of the carrier of (Polynom-Ring INT.Ring) by A6;
A8:
for i being Nat st i in Seg (k + 1) holds
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i
by A3, Th18;
Sum lbz =
((Der1 INT.Ring) |^ k) . ((Product (Del ((ff_0 (m,p)),j))) * ((tau j) |^ p))
by RINGDER1:25
.=
((Der1 INT.Ring) |^ k) . (f_0 (m,p))
by A1, Lm9
;
then
ex u being Element of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) = (tau j) * u
by GCD_1:def 1, A8, A7, E_TRANS1:4;
hence
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) = 0. INT.Ring
by Th25; verum