let p be prime odd Nat; for m being positive Nat
for j, k being Nat st j in Seg m & p <= k holds
for i being Nat st i in Seg p 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; for j, k being Nat st j in Seg m & p <= k holds
for i being Nat st i in Seg p holds
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i
let j, k be Nat; ( j in Seg m & p <= k implies for i being Nat st i in Seg p holds
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i )
assume A1:
( j in Seg m & p <= k )
; for i being Nat st i in Seg p 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;
A2:
p -' 1 = p - 1
by XREAL_1:233, NAT_1:14;
1 < p
by INT_2:def 4;
then
1 + 1 <= p
by INT_1:7;
then
2 - 2 <= p - 2
by XREAL_1:6;
then
p - 2 in NAT
by INT_1:3;
then reconsider p2 = p - 2 as Nat ;
reconsider p1 = p -' 1 as non zero Nat by A2;
for i being Nat st i in Seg p holds
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i
proof
let i be
Nat;
( i in Seg p implies 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;
set f =
Product (ff_0 (m,p));
set xj =
tau j;
set yj =
Product (Del ((ff_0 (m,p)),j));
reconsider n0 =
j as
Nat ;
assume A4:
i in Seg p
;
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i
then A5:
( 1
<= i &
i <= p )
by FINSEQ_1:1;
set f =
Product (ff_0 (m,p));
set xj =
tau j;
set yj =
Product (Del ((ff_0 (m,p)),j));
A6:
1. (Polynom-Ring INT.Ring) =
(Der1 INT.Ring) . (tau j)
by Th27
.=
((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 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;
p < k + 1
by A1, NAT_1:13;
then A8:
Seg p c= Seg (k + 1)
by FINSEQ_1:5;
reconsider i1 =
i - 1 as
Nat by A5;
A9:
i -' 1
= i - 1
by A5, XREAL_1:233;
A10:
tau j divides ((Der1 INT.Ring) |^ (i -' 1)) . ((tau j) |^ p)
proof
per cases
( i -' 1 = 0 or i -' 1 <> 0 )
;
suppose A13:
i -' 1
<> 0
;
tau j divides ((Der1 INT.Ring) |^ (i -' 1)) . ((tau j) |^ p)A14:
i -' 1
< i
by A9, XREAL_1:44;
then A15:
( 1
<= i -' 1 &
i -' 1
< p )
by A13, NAT_1:14, A5, XXREAL_0:2;
then A16:
p - (i -' 1) > (i -' 1) - (i -' 1)
by XREAL_1:6;
A17:
p - (i -' 1) =
p - (i - 1)
by A5, XREAL_1:233
.=
(p - i) + 1
;
then A18:
p -' (i -' 1) = (p - i) + 1
by A14, A5, XXREAL_0:2, XREAL_1:233;
reconsider p9 =
(p - i) + 1 as non
zero Nat by A17, A16, INT_1:3, ORDINAL1:def 12;
reconsider s =
eta (
p,
(i -' 1)) as
Element of
NAT ;
A19:
tau j divides s * ((tau j) |^ p9)
by Lm8, E_TRANS1:7;
((Der1 INT.Ring) |^ (i -' 1)) . ((tau j) |^ p) = s * ((tau j) |^ p9)
by A18, A15, A6, E_TRANS1:19;
hence
tau j divides ((Der1 INT.Ring) |^ (i -' 1)) . ((tau j) |^ p)
by A19;
verum end;
end;
reconsider u =
(k choose (i -' 1)) * (((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j)))) as
Element of the
carrier of
(Polynom-Ring INT.Ring) ;
A20:
tau j divides (((Der1 INT.Ring) |^ (i -' 1)) . ((tau j) |^ p)) * u
by A10, GCD_1:7;
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) . i = (((Der1 INT.Ring) |^ (i -' 1)) . ((tau j) |^ p)) * u
by A7, A4, A8, RINGDER1:def 4;
hence
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i
by A20, A7, A4, A8, PARTFUN1:def 6;
verum
end;
hence
for i being Nat st i in Seg p holds
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i
; verum