let p be prime odd Nat; :: thesis: for m being positive Nat
for k, j being Nat st j in Seg m & p <= k holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) in {(In ((p !),INT.Ring))} -Ideal
let m be positive Nat; :: thesis: for k, j being Nat st j in Seg m & p <= k holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) in {(In ((p !),INT.Ring))} -Ideal
let k, j be Nat; :: thesis: ( j in Seg m & p <= k implies eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) in {(In ((p !),INT.Ring))} -Ideal )
assume that
A1: j in Seg m and
AA: p <= k ; :: thesis: eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) in {(In ((p !),INT.Ring))} -Ideal
consider u, v being Element of the carrier of (Polynom-Ring INT.Ring) such that
A2: ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) = ((tau j) * u) + ((p !) * v) by AA, Th30, A1;
reconsider z = p ! as Element of INT.Ring by INT_1:def 2;
set tu = (tau j) * u;
set pv = (p !) * v;
set r = In ((p !),INT.Ring);
set j1 = In (j,INT.Ring);
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) = eval (((~ ((tau j) * u)) + (~ ((p !) * v))),(In (j,INT.Ring))) by A2, POLYNOM3:def 10
.= (eval ((~ ((tau j) * u)),(In (j,INT.Ring)))) + (eval ((~ ((p !) * v)),(In (j,INT.Ring)))) by POLYNOM4:19
.= (0. INT.Ring) + (eval ((~ ((p !) * v)),(In (j,INT.Ring)))) by Th25
.= eval (((In ((p !),INT.Ring)) * (~ v)),(In (j,INT.Ring))) by Th6 ;
hence eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) in {(In ((p !),INT.Ring))} -Ideal by Th31; :: thesis: verum