let p be prime odd Nat; :: thesis: for m being positive Nat
for k being Nat st 0 <= k & k <= p - 1 holds
for i, j 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
let m be positive Nat; :: thesis: for k being Nat st 0 <= k & k <= p - 1 holds
for i, j 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
let k be Nat; :: thesis: ( 0 <= k & k <= p - 1 implies for i, j 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 )
assume A1: ( 0 <= k & k <= p - 1 ) ; :: thesis: for i, j 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
set D = Der1 INT.Ring;
set PR = Polynom-Ring INT.Ring;
for i, j 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

proof

let i, j be Nat; :: thesis: ( i in Seg (k + 1) implies tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i )
set f = Product (ff_0 (m,p));
set xj = tau j;
set yj = Product (Del ((ff_0 (m,p)),j));
assume A2: i in Seg (k + 1) ; :: thesis: tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i
A3: 1. (Polynom-Ring INT.Ring) = (Der1 INT.Ring) . (tau j) by Th13
.= ((Der1 INT.Ring) |^ 1) . (tau j) by VECTSP11:19
.= ((Der1 INT.Ring) |^ 1) . ((tau j) |^ 1) by BINOM:8 ;
len (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) = k + 1 by RINGDER1:def 4;
then A4: i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) by A2, FINSEQ_1:def 3;
set p1 = p - 1;
A5: k + 1 <= (p - 1) + 1 by A1, XREAL_1:6;
A7: (p - 1) + 0 <= (p - 1) + 1 by XREAL_1:7;
A6: ( 1 <= i & i <= k + 1 ) by A2, FINSEQ_1:1;
then A8: ( 1 <= i & i <= p ) by A5, XXREAL_0:2;
then A9: i - 1 <= p - 1 by XREAL_1:6;
set i1 = i -' 1;
set s = k choose (i -' 1);
set t = eta (p,(i -' 1));
A10: ( 0 <= i -' 1 & i -' 1 <= p - 1 ) by A6, XREAL_1:233, A9;

per cases ( i -' 1 <> 0 or i -' 1 = 0 ) ;

suppose i -' 1 <> 0 ; :: thesis: tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i

then ( 1 <= i -' 1 & i -' 1 <= p ) by NAT_1:14, A7, A10, XXREAL_0:2;
then A13: ((Der1 INT.Ring) |^ (i -' 1)) . ((tau j) |^ p) = (eta (p,(i -' 1))) * ((tau j) |^ (p -' (i -' 1))) by A3, E_TRANS1:19;
set tDx = (eta (p,(i -' 1))) * ((tau j) |^ (p -' (i -' 1)));
set Dy = ((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j)));
A14: (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) . i = ((eta (p,(i -' 1))) * ((tau j) |^ (p -' (i -' 1)))) * ((k choose (i -' 1)) * (((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j))))) by A13, A4, RINGDER1:def 4
.= ((tau j) |^ (p -' (i -' 1))) * ((eta (p,(i -' 1))) * ((k choose (i -' 1)) * (((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j)))))) by RINGDER1:2 ;
set u = (tau j) |^ (p -' (i -' 1));
set v = (eta (p,(i -' 1))) * ((k choose (i -' 1)) * (((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j)))));
reconsider w = (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) . i as Element of the carrier of (Polynom-Ring INT.Ring) by A4, FINSEQ_2:11;
A15: i - i <= p - i by A8, XREAL_1:6;
p -' (i -' 1) = p - (i -' 1) by XREAL_1:233, A7, A10, XXREAL_0:2
.= p - (i - 1) by A6, XREAL_1:233
.= (p - i) + 1 ;
then A17: tau j divides (tau j) |^ (p -' (i -' 1)) by A15, Lm8;
(tau j) |^ (p -' (i -' 1)) divides w by A14, GCD_1:def 1;
then tau j divides w by A17, GCD_1:2;
hence tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i by A4, PARTFUN1:def 6; :: thesis: verum

end;

suppose i -' 1 = 0 ; :: thesis: tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i

then ((Der1 INT.Ring) |^ (i -' 1)) . ((tau j) |^ p) = (id (Polynom-Ring INT.Ring)) . ((tau j) |^ p) by VECTSP11:18
.= (tau j) |^ p ;
then A20: (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) . i = ((tau j) |^ p) * ((k choose (i -' 1)) * (((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j))))) by A4, RINGDER1:def 4;
tau j divides ((tau j) |^ p) * ((k choose (i -' 1)) * (((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j))))) by GCD_1:7, Lm8;
hence tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i by A20, A4, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

hence for i, j 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 ; :: thesis: verum