let p be prime odd Nat; :: thesis: for m being positive Nat holds (~ (Product (x. (m,p)))) . 0 = (((- 1) |^ m) * (m !)) |^ p
let m be positive Nat; :: thesis: (~ (Product (x. (m,p)))) . 0 = (((- 1) |^ m) * (m !)) |^ p
defpred S₁[ Nat] means (~ (Product (x. ($1,p)))) . 0 = (((- 1) |^ $1) * ($1 !)) |^ p;
A1: S₁[1]

proof

A2: len (x. (1,p)) = 1 by Def2;
A3: x. (1,p) = <*((x. (1,p)) . 1)*> by Def2, FINSEQ_1:40;
dom (x. (1,p)) = Seg 1 by A2, FINSEQ_1:def 3;
then 1 in dom (x. (1,p)) ;
then A4: (x. (1,p)) . 1 = (tau 1) |^ p by Def2;
(~ (Product (x. (1,p)))) . 0 = (~ ((tau 1) |^ p)) . 0 by A3, A4, FINSOP_1:11
.= (In ((- 1),INT.Ring)) |^ p by Lm10
.= (- 1) |^ p by Lm2 ;
hence S₁[1] by NEWTON:13; :: thesis: verum

end;

A6: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: (- (k + 1)) |^ p = (In ((- (k + 1)),INT.Ring)) |^ p by Lm2;
Product (x. ((k + 1),p)) = (Product (x. (k,p))) * ((tau (k + 1)) |^ p) by Th10;
then (~ (Product (x. ((k + 1),p)))) . 0 = ((~ (Product (x. (k,p)))) *' (~ ((tau (k + 1)) |^ p))) . 0 by POLYNOM3:def 10
.= ((~ (Product (x. (k,p)))) . 0) * ((~ ((tau (k + 1)) |^ p)) . 0) by Th14
.= ((((- 1) |^ k) * (k !)) |^ p) * ((- (k + 1)) |^ p) by A8, A7, Lm10
.= ((((- 1) |^ k) * (k !)) * ((- 1) * (k + 1))) |^ p by NEWTON:7
.= (((((- 1) |^ k) * (- 1)) * (k !)) * (k + 1)) |^ p
.= ((((- 1) |^ (k + 1)) * (k !)) * (k + 1)) |^ p by NEWTON:6
.= (((- 1) |^ (k + 1)) * ((k !) * (k + 1))) |^ p
.= (((- 1) |^ (k + 1)) * ((k + 1) !)) |^ p by NEWTON:15 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A1, A6);
hence (~ (Product (x. (m,p)))) . 0 = (((- 1) |^ m) * (m !)) |^ p ; :: thesis: verum