let x, y, x1 be Nat; :: thesis: ( x1 >= 1 implies ( y = Product (1 + (x1 * (idseq x))) iff ex u, w, y1, y2, y3, y4, y5 being Nat st
( u > y & x1 * w,1 are_congruent_mod u & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod u & y4 = 1 + (x1 * x) & y5 = y4 |^ x & u > y5 ) ) )
assume A1: x1 >= 1 ; :: thesis: ( y = Product (1 + (x1 * (idseq x))) iff ex u, w, y1, y2, y3, y4, y5 being Nat st
( u > y & x1 * w,1 are_congruent_mod u & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod u & y4 = 1 + (x1 * x) & y5 = y4 |^ x & u > y5 ) )
defpred S1[ Nat] means (1 + (x1 * $1)) |^ $1 >= Product (1 + (x1 * (idseq $1)));
A2: S1[ 0 ] by RVSUM_1:94;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[n + 1]
set n1 = n + 1;
A5: 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 1 + (x1 * (idseq (n + 1))) = (1 + (x1 * (idseq n))) ^ (1 + (x1 * <*(n + 1)*>)) by BASEL_1:3;
then A6: Product (1 + (x1 * (idseq (n + 1)))) = (Product (1 + (x1 * (idseq n)))) * (1 + (x1 * (n + 1))) by A5, RVSUM_1:96;
x1 * n <= x1 * (n + 1) by NAT_1:11, XREAL_1:64;
then 1 + (x1 * n) <= 1 + (x1 * (n + 1)) by XREAL_1:7;
then (1 + (x1 * n)) |^ n <= (1 + (x1 * (n + 1))) |^ n by PREPOWER:9;
then ((1 + (x1 * n)) |^ n) * (1 + (x1 * (n + 1))) <= ((1 + (x1 * (n + 1))) |^ n) * (1 + (x1 * (n + 1))) by XREAL_1:64;
then A7: ((1 + (x1 * n)) |^ n) * (1 + (x1 * (n + 1))) <= (1 + (x1 * (n + 1))) |^ (n + 1) by NEWTON:6;
(Product (1 + (x1 * (idseq n)))) * (1 + (x1 * (n + 1))) <= ((1 + (x1 * n)) |^ n) * (1 + (x1 * (n + 1))) by A4, XREAL_1:64;
hence S1[n + 1] by A7, A6, XXREAL_0:2; :: thesis: verum
end;
A8: for n being Nat holds S1[n] from NAT_1:sch 2(A2, A3);
 thus ( y = Product (1 + (x1 * (idseq x))) implies ex u, w, y1, y2, y3, y4, y5 being Nat st
( u > y & x1 * w,1 are_congruent_mod u & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod u & y4 = 1 + (x1 * x) & y5 = y4 |^ x & u > y5 ) ) :: thesis: ( ex u, w, y1, y2, y3, y4, y5 being Nat st
( u > y & x1 * w,1 are_congruent_mod u & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod u & y4 = 1 + (x1 * x) & y5 = y4 |^ x & u > y5 ) implies y = Product (1 + (x1 * (idseq x))) )
proof
assume A9: y = Product (1 + (x1 * (idseq x))) ; :: thesis: ex u, w, y1, y2, y3, y4, y5 being Nat st
( u > y & x1 * w,1 are_congruent_mod u & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod u & y4 = 1 + (x1 * x) & y5 = y4 |^ x & u > y5 )
set u = (x1 * ((1 + (x1 * x)) |^ x)) + 1;
((x1 * ((1 + (x1 * x)) |^ x)) + 1) gcd x1 = 1 gcd x1 by EULER_1:16
.= 1 by WSIERP_1:8 ;
then consider w being Nat such that
A10: ((x1 * w) - 1) mod ((x1 * ((1 + (x1 * x)) |^ x)) + 1) = 0 by INT_4:16, INT_2:def 3;
take (x1 * ((1 + (x1 * x)) |^ x)) + 1 ; :: thesis: ex w, y1, y2, y3, y4, y5 being Nat st
( (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y & x1 * w,1 are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 )
take w ; :: thesis: ex y1, y2, y3, y4, y5 being Nat st
( (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y & x1 * w,1 are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 )
take y1 = x1 |^ x; :: thesis: ex y2, y3, y4, y5 being Nat st
( (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y & x1 * w,1 are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 )
take y2 = x ! ; :: thesis: ex y3, y4, y5 being Nat st
( (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y & x1 * w,1 are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 )
take y3 = (w + x) choose x; :: thesis: ex y4, y5 being Nat st
( (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y & x1 * w,1 are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 )
take y4 = 1 + (x1 * x); :: thesis: ex y5 being Nat st
( (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y & x1 * w,1 are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 )
take y5 = y4 |^ x; :: thesis: ( (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y & x1 * w,1 are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 )
A11: (x1 * w) - 1 = ((((x1 * w) - 1) div ((x1 * ((1 + (x1 * x)) |^ x)) + 1)) * ((x1 * ((1 + (x1 * x)) |^ x)) + 1)) + 0 by A10, INT_1:59;
then y,((x1 |^ x) * (x !)) * ((w + x) choose x) are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 by A9, Th19, INT_1:def 5;
then consider e being Integer such that
A12: (((x1 |^ x) * (x !)) * ((w + x) choose x)) - y = ((x1 * ((1 + (x1 * x)) |^ x)) + 1) * e by INT_1:def 5, INT_1:14;
(1 + (x1 * x)) |^ x >= Product (1 + (x1 * (idseq x))) by A8;
then x1 * ((1 + (x1 * x)) |^ x) >= 1 * (Product (1 + (x1 * (idseq x)))) by A1, XREAL_1:66;
hence (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y by A9, NAT_1:13; :: thesis: ( x1 * w,1 are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 )
thus x1 * w,1 are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 by A11, INT_1:def 5; :: thesis: ( y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 )
A13: (x1 * ((1 + (x1 * x)) |^ x)) + 1 > (x1 * ((1 + (x1 * x)) |^ x)) + 0 by XREAL_1:6;
x1 * ((1 + (x1 * x)) |^ x) >= 1 * ((1 + (x1 * x)) |^ x) by A1, XREAL_1:66;
hence ( y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x & (y1 * y2) * y3,y are_congruent_mod (x1 * ((1 + (x1 * x)) |^ x)) + 1 & y4 = 1 + (x1 * x) & y5 = y4 |^ x & (x1 * ((1 + (x1 * x)) |^ x)) + 1 > y5 ) by A12, INT_1:def 5, A13, XXREAL_0:2; :: thesis: verum
end;
given u, w, y1, y2, y3, y4, y5 being Nat such that A14: ( u > y & x1 * w,1 are_congruent_mod u ) and
A15: ( y1 = x1 |^ x & y2 = x ! & y3 = (w + x) choose x ) and
A16: (y1 * y2) * y3,y are_congruent_mod u and
A17: ( y4 = 1 + (x1 * x) & y5 = y4 |^ x & u > y5 ) ; :: thesis: y = Product (1 + (x1 * (idseq x)))
set U = ((x1 |^ x) * (x !)) * ((w + x) choose x);
Product (1 + (x1 * (idseq x))),((x1 |^ x) * (x !)) * ((w + x) choose x) are_congruent_mod u by A14, Th19;
then A18: ((x1 |^ x) * (x !)) * ((w + x) choose x), Product (1 + (x1 * (idseq x))) are_congruent_mod u by INT_1:14;
A19: Product (1 + (x1 * (idseq x))) is Nat by TARSKI:1;
Product (1 + (x1 * (idseq x))) <= (1 + (x1 * x)) |^ x by A8;
then Product (1 + (x1 * (idseq x))) < u by A17, XXREAL_0:2;
hence y = Product (1 + (x1 * (idseq x))) by A19, A18, A15, A16, A14, NAT_6:14; :: thesis: verum