let x1, w, u be Nat; :: thesis: ( x1 * w,1 are_congruent_mod u implies for x being Nat holds Product (1 + (x1 * (idseq x))),((x1 |^ x) * (x !)) * ((w + x) choose x) are_congruent_mod u )
assume A1: x1 * w,1 are_congruent_mod u ; :: thesis: for x being Nat holds Product (1 + (x1 * (idseq x))),((x1 |^ x) * (x !)) * ((w + x) choose x) are_congruent_mod u
consider b being Integer such that
A2: u * b = (x1 * w) - 1 by A1, INT_1:def 5;
defpred S₁[ Nat] means Product (1 + (x1 * (idseq $1))),((x1 |^ $1) * ($1 !)) * ((w + $1) choose $1) are_congruent_mod u;
( x1 |^ 0 = 1 & 0 ! = 1 & (w + 0) choose 0 = 1 ) by NEWTON:4, NEWTON:12, NEWTON:19;
then A3: S₁[ 0 ] by RVSUM_1:94, INT_1:11;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
set P = Product (1 + (x1 * (idseq n)));
set L = ((x1 |^ n) * (n !)) * ((w + n) choose n);
assume S₁[n] ; :: thesis: S₁[n + 1]
then consider a being Integer such that
A5: u * a = (Product (1 + (x1 * (idseq n)))) - (((x1 |^ n) * (n !)) * ((w + n) choose n)) by INT_1:def 5;
A6: 1 + (x1 * <*(n + 1)*>) = 1 + <*(x1 * (n + 1))*> by RVSUM_1:47
.= <*(1 + (x1 * (n + 1)))*> by BASEL_1:2 ;
idseq (n + 1) = (idseq n) ^ <*(n + 1)*> by FINSEQ_2:51;
then x1 * (idseq (n + 1)) = (x1 * (idseq n)) ^ (x1 * <*(n + 1)*>) by NEWTON04:43;
then A7: 1 + (x1 * (idseq (n + 1))) = (1 + (x1 * (idseq n))) ^ (1 + (x1 * <*(n + 1)*>)) by BASEL_1:3;
( w + n >= n & (w + n) - n = w ) by NAT_1:11;
then (w + n) choose n = ((w + n) !) / ((n !) * (w !)) by NEWTON:def 3;
then A8: (n !) * ((w + n) choose n) = ((n !) * ((w + n) !)) / ((n !) * (w !)) by XCMPLX_1:74
.= ((w + n) !) / (w !) by XCMPLX_1:91 ;
( w + (n + 1) >= n + 1 & (w + (n + 1)) - (n + 1) = w ) by NAT_1:11;
then (w + (n + 1)) choose (n + 1) = ((w + (n + 1)) !) / (((n + 1) !) * (w !)) by NEWTON:def 3;
then A9: ((n + 1) !) * ((w + (n + 1)) choose (n + 1)) = (((n + 1) !) * ((w + (n + 1)) !)) / (((n + 1) !) * (w !)) by XCMPLX_1:74
.= (((w + n) + 1) !) / (w !) by XCMPLX_1:91
.= (((w + n) !) * ((w + n) + 1)) / (w !) by NEWTON:15
.= ((w + n) + 1) * (((w + n) !) / (w !)) by XCMPLX_1:74
.= ((w + (n + 1)) * (n !)) * ((w + n) choose n) by A8 ;
x1 |^ (n + 1) = (x1 |^ n) * x1 by NEWTON:6;
then ((x1 |^ (n + 1)) * ((n + 1) !)) * ((w + (n + 1)) choose (n + 1)) = ((x1 |^ n) * x1) * (((n + 1) !) * ((w + (n + 1)) choose (n + 1)))
.= ((x1 |^ n) * x1) * ((((w + n) + 1) * (n !)) * ((w + n) choose n)) by A9
.= ((w + (n + 1)) * x1) * (((x1 |^ n) * (n !)) * ((w + n) choose n)) ;
then (Product (1 + (x1 * (idseq (n + 1))))) - (((x1 |^ (n + 1)) * ((n + 1) !)) * ((w + (n + 1)) choose (n + 1))) = ((Product (1 + (x1 * (idseq n)))) * (1 + (x1 * (n + 1)))) - ((x1 * (w + (n + 1))) * (((x1 |^ n) * (n !)) * ((w + n) choose n))) by A7, A6, RVSUM_1:96
.= (((Product (1 + (x1 * (idseq n)))) * (1 + (x1 * (n + 1)))) - ((x1 * w) * (((x1 |^ n) * (n !)) * ((w + n) choose n)))) - ((x1 * (n + 1)) * (((x1 |^ n) * (n !)) * ((w + n) choose n)))
.= (((Product (1 + (x1 * (idseq n)))) * (1 + (x1 * (n + 1)))) - (((u * b) + 1) * (((x1 |^ n) * (n !)) * ((w + n) choose n)))) - ((x1 * (n + 1)) * (((x1 |^ n) * (n !)) * ((w + n) choose n))) by A2
.= (((Product (1 + (x1 * (idseq n)))) - (((x1 |^ n) * (n !)) * ((w + n) choose n))) * (1 + (x1 * (n + 1)))) - (((u * b) * 1) * (((x1 |^ n) * (n !)) * ((w + n) choose n)))
.= ((u * a) * (1 + (x1 * (n + 1)))) - ((u * b) * (((x1 |^ n) * (n !)) * ((w + n) choose n))) by A5
.= u * ((a * (1 + (x1 * (n + 1)))) - (b * (((x1 |^ n) * (n !)) * ((w + n) choose n)))) ;
hence S₁[n + 1] by INT_1:def 5; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence for x being Nat holds Product (1 + (x1 * (idseq x))),((x1 |^ x) * (x !)) * ((w + x) choose x) are_congruent_mod u ; :: thesis: verum