let n be Nat; :: thesis: for i1, i2 being Element of n st n <> 0 holds
{ p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2 be Element of n; :: thesis: ( n <> 0 implies { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT) )
set n6 = n + 6;
defpred S1[ XFinSequence of NAT ] means $1 . i1 = ($1 . i2) ! ;
set RR = { p where p is n -element XFinSequence of NAT : S1[p] } ;
assume A1: n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)
n = n + 0 ;
then reconsider Y = i1, X = i2, N = n, Y1 = n + 1, Y2 = n + 2, Y3 = n + 3, X1 = n + 4, X2 = n + 5 as Element of n + 6 by HILB10_3:2, HILB10_3:3;
defpred S2[ XFinSequence of NAT ] means $1 . Y1 = ($1 . X2) |^ ($1 . X1);
A2: { p where p is n + 6 -element XFinSequence of NAT : S2[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by HILB10_3:24;
defpred S3[ XFinSequence of NAT ] means $1 . Y2 = ($1 . N) |^ ($1 . X);
A3: { p where p is n + 6 -element XFinSequence of NAT : S3[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by HILB10_3:24;
defpred S4[ XFinSequence of NAT ] means ( $1 . N >= $1 . X & $1 . Y3 = ($1 . N) choose ($1 . X) );
A4: { p where p is n + 6 -element XFinSequence of NAT : S4[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by Th30;
defpred S5[ XFinSequence of NAT ] means ( 1 * ($1 . Y) = [\((1 * ($1 . Y2)) / (1 * ($1 . Y3)))/] & 1 * ($1 . Y3) <> 0 );
A5: { p where p is n + 6 -element XFinSequence of NAT : S5[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by Th28;
defpred S6[ XFinSequence of NAT ] means 1 * ($1 . X2) = (2 * ($1 . X)) + 0;
A6: { p where p is n + 6 -element XFinSequence of NAT : S6[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by HILB10_3:6;
defpred S7[ XFinSequence of NAT ] means 1 * ($1 . X1) = (1 * ($1 . X)) + 1;
A7: { p where p is n + 6 -element XFinSequence of NAT : S7[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by HILB10_3:6;
defpred S8[ XFinSequence of NAT ] means 1 * ($1 . N) > (1 * ($1 . Y1)) + 0;
A8: { p where p is n + 6 -element XFinSequence of NAT : S8[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by HILB10_3:7;
defpred S9[ XFinSequence of NAT ] means ( S2[$1] & S3[$1] );
A9: { p where p is n + 6 -element XFinSequence of NAT : S9[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A2, A3);
 defpred S10[ XFinSequence of NAT ] means ( S9[$1] & S4[$1] );
A10: { p where p is n + 6 -element XFinSequence of NAT : S10[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A9, A4);
 defpred S11[ XFinSequence of NAT ] means ( S10[$1] & S5[$1] );
A11: { p where p is n + 6 -element XFinSequence of NAT : S11[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A10, A5);
 defpred S12[ XFinSequence of NAT ] means ( S11[$1] & S6[$1] );
A12: { p where p is n + 6 -element XFinSequence of NAT : S12[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A11, A6);
 defpred S13[ XFinSequence of NAT ] means ( S12[$1] & S7[$1] );
A13: { p where p is n + 6 -element XFinSequence of NAT : S13[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A12, A7);
 defpred S14[ XFinSequence of NAT ] means ( S13[$1] & S8[$1] );
set PP = { p where p is n + 6 -element XFinSequence of NAT : S14[p] } ;
A14: { p where p is n + 6 -element XFinSequence of NAT : S14[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A13, A8);
 reconsider PPn = { (p | n) where p is n + 6 -element XFinSequence of NAT : p in { p where p is n + 6 -element XFinSequence of NAT : S14[p] } } as diophantine Subset of (n -xtuples_of NAT) by NAT_1:11, HILB10_3:5, A14;
A15: PPn c= { p where p is n -element XFinSequence of NAT : S1[p] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PPn or x in { p where p is n -element XFinSequence of NAT : S1[p] } )
assume x in PPn ; :: thesis: x in { p where p is n -element XFinSequence of NAT : S1[p] }
then consider p being n + 6 -element XFinSequence of NAT such that
A16: ( x = p | n & p in { p where p is n + 6 -element XFinSequence of NAT : S14[p] } ) ;
ex q being n + 6 -element XFinSequence of NAT st
( q = p & S14[q] ) by A16;
then A17: p . Y = (p . X) ! by Th18;
( (p | n) . X = p . i2 & (p | n) . Y = p . i1 ) by A1, HILB10_3:4;
hence x in { p where p is n -element XFinSequence of NAT : S1[p] } by A17, A16; :: thesis: verum
end;
{ p where p is n -element XFinSequence of NAT : S1[p] } c= PPn
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is n -element XFinSequence of NAT : S1[p] } or x in PPn )
assume x in { p where p is n -element XFinSequence of NAT : S1[p] } ; :: thesis: x in PPn
then consider p being n -element XFinSequence of NAT such that
A18: ( x = p & S1[p] ) ;
consider N, y1, y2, y3 being Nat such that
A19: ( y1 = (2 * (p . i2)) |^ ((p . i2) + 1) & y2 = N |^ (p . i2) & y3 = N choose (p . i2) & N > y1 & p . i1 = [\(y2 / y3)/] ) by Th18, A18;
A20: ( p . i2 <> 0 implies N >= p . i2 )
proof
assume p . i2 <> 0 ; :: thesis: N >= p . i2
then A21: 2 * (p . i2) >= 1 by NAT_1:14;
(p . i2) + 1 >= 1 by NAT_1:11;
then A22: (2 * (p . i2)) |^ ((p . i2) + 1) >= (2 * (p . i2)) |^ 1 by A21, PREPOWER:93;
( N > 2 * (p . i2) & (p . i2) + (p . i2) >= p . i2 ) by A22, A19, XXREAL_0:2, NAT_1:11;
hence N >= p . i2 by XXREAL_0:2; :: thesis: verum
end;
reconsider x1 = (p . i2) + 1, x2 = 2 * (p . i2) as Element of NAT ;
reconsider N = N, y1 = y1, y2 = y2, y3 = y3 as Element of NAT by ORDINAL1:def 12;
set Y = ((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>;
set PY = p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>);
A23: ( len p = n & len (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) = 6 ) by CARD_1:def 7;
A24: (p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>)) | n = p by A23, AFINSQ_1:57;
0 in dom (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) by AFINSQ_1:66;
then A25: (p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>)) . (n + 0) = (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) . 0 by A23, AFINSQ_1:def 3
.= N by AFINSQ_1:47 ;
1 in dom (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) by A23, AFINSQ_1:66;
then A26: (p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>)) . (n + 1) = (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) . 1 by A23, AFINSQ_1:def 3
.= y1 by AFINSQ_1:47 ;
2 in dom (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) by A23, AFINSQ_1:66;
then A27: (p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>)) . (n + 2) = (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) . 2 by A23, AFINSQ_1:def 3
.= y2 by AFINSQ_1:47 ;
3 in dom (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) by A23, AFINSQ_1:66;
then A28: (p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>)) . (n + 3) = (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) . 3 by A23, AFINSQ_1:def 3
.= y3 by AFINSQ_1:47 ;
4 in dom (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) by A23, AFINSQ_1:66;
then A29: (p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>)) . (n + 4) = (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) . 4 by A23, AFINSQ_1:def 3
.= x1 by AFINSQ_1:47 ;
5 in dom (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) by A23, AFINSQ_1:66;
then A30: (p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>)) . (n + 5) = (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) . 5 by A23, AFINSQ_1:def 3
.= x2 by AFINSQ_1:47 ;
S14[p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>)] by A20, A19, CATALAN2:26, A24, A1, HILB10_3:4, A25, A26, A27, A28, A29, A30;
then p ^ (((((<%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>) in { p where p is n + 6 -element XFinSequence of NAT : S14[p] } ;
hence x in PPn by A24, A18; :: thesis: verum
end;
hence { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT) by A15, XBOOLE_0:def 10; :: thesis: verum