let p be prime odd Nat; :: thesis: for m being positive Nat
for k being Nat st 0 <= k & k <= p -' 2 holds
(((Der1 INT.Ring) |^ k) . (f_0 (m,p))) . 0 = 0. INT.Ring
let m be positive Nat; :: thesis: for k being Nat st 0 <= k & k <= p -' 2 holds
(((Der1 INT.Ring) |^ k) . (f_0 (m,p))) . 0 = 0. INT.Ring
let k be Nat; :: thesis: ( 0 <= k & k <= p -' 2 implies (((Der1 INT.Ring) |^ k) . (f_0 (m,p))) . 0 = 0. INT.Ring )
set D = Der1 INT.Ring;
set t0 = tau 0;
assume A1: ( 0 <= k & k <= p -' 2 ) ; :: thesis: (((Der1 INT.Ring) |^ k) . (f_0 (m,p))) . 0 = 0. INT.Ring
set F0 = f_0 (m,p);
A2: 1 < p by INT_2:def 4;
1 + 1 < p + 1 by INT_2:def 4, XREAL_1:6;
then 2 <= p by NAT_1:13;
then A3: ( p -' 2 = p - 2 & p -' 1 = p - 1 ) by A2, XREAL_1:233;
then reconsider p1 = p -' 1 as non zero Element of NAT ;
(p - 1) - 1 < p - 1 by XREAL_1:44;
then A5: k < p -' 1 by A3, A1, XXREAL_0:2;
set f = Product (x. (m,p));
A6: (~ (((tau 0) |^ (p -' 1)) * (Product (x. (m,p))))) . k = ((~ ((tau 0) |^ (p -' 1))) *' (~ (Product (x. (m,p))))) . k by POLYNOM3:def 10
.= (((~ ((tau 0) |^ (p -' 1))) *' (~ (Product (x. (m,p))))) | (Segm p1)) . k by A5, NAT_1:44, FUNCT_1:49
.= ((Segm p1) --> (0. INT.Ring)) . k by Lm6
.= 0. INT.Ring by A5, NAT_1:44, FUNCOP_1:7 ;
(((Der1 INT.Ring) |^ k) . (f_0 (m,p))) . 0 = (eta ((0 + k),k)) * ((f_0 (m,p)) . (0 + k)) by E_TRANS1:22
.= (eta ((0 + k),k)) * (0. INT.Ring) by A6, GROUP_4:6
.= 0. INT.Ring ;
hence (((Der1 INT.Ring) |^ k) . (f_0 (m,p))) . 0 = 0. INT.Ring ; :: thesis: verum