let p be prime odd Nat; for m being positive Nat
for k, j, i being Nat st p + 1 < i & i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) holds
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring)
let m be positive Nat; for k, j, i being Nat st p + 1 < i & i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) holds
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring)
let k, j be Nat; for i being Nat st p + 1 < i & i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) holds
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring)
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 n0 = j as Nat ;
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 u = (k choose p) * (((Der1 INT.Ring) |^ (k -' p)) . (Product (Del ((ff_0 (m,p)),j)))) as Element of the carrier of (Polynom-Ring INT.Ring) ;
A2: 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 A3:
dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) = Seg (k + 1)
by FINSEQ_1:def 3;
for i being Nat st p + 1 < i & i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) holds
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring)
proof
let i be
Nat;
( p + 1 < i & i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) implies (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring) )
assume A4:
(
p + 1
< i &
i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) )
;
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring)
set u =
(k choose (i -' 1)) * (((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j))));
A5:
( 1
<= i &
i <= k + 1 )
by A3, A4, FINSEQ_1:1;
(p + 1) - 1
< i - 1
by A4, XREAL_1:6;
then A7:
p < i -' 1
by A5, XREAL_1:233;
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) . i =
((k choose (i -' 1)) * (((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j))))) * (((Der1 INT.Ring) |^ (i -' 1)) . ((tau j) |^ p))
by A4, RINGDER1:def 4
.=
((k choose (i -' 1)) * (((Der1 INT.Ring) |^ ((k + 1) -' i)) . (Product (Del ((ff_0 (m,p)),j))))) * (0. (Polynom-Ring INT.Ring))
by A7, A2, E_TRANS1:21
.=
0. (Polynom-Ring INT.Ring)
;
hence
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring)
by A4, PARTFUN1:def 6;
verum
end;
hence
for i being Nat st p + 1 < i & i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) holds
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring)
; verum