let n be Nat; :: thesis: for i1, i2, i3 being Element of n st n <> 0 holds
{ p where p is n -element XFinSequence of NAT : ( p . i1 >= p . i3 & p . i2 = (p . i1) choose (p . i3) ) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; :: thesis: ( n <> 0 implies { p where p is n -element XFinSequence of NAT : ( p . i1 >= p . i3 & p . i2 = (p . i1) choose (p . i3) ) } is diophantine Subset of (n -xtuples_of NAT) )
set n6 = n + 6;
defpred S1[ XFinSequence of NAT ] means ( $1 . i1 >= $1 . i3 & $1 . i2 = ($1 . i1) choose ($1 . i3) );
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 . i3 & p . i2 = (p . i1) choose (p . i3) ) } is diophantine Subset of (n -xtuples_of NAT)
n = n + 0 ;
then reconsider X = i1, Y = i2, Z = i3, U = n, V = n + 1, Y1 = n + 2, Y2 = n + 3, Y3 = n + 4, U1 = n + 5 as Element of n + 6 by HILB10_3:2, HILB10_3:3;
defpred S2[ XFinSequence of NAT ] means $1 . Y1 = ($1 . X) |^ ($1 . Z);
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 . U1) |^ ($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 . Y3 = ($1 . U) |^ ($1 . Z);
A4: { p where p is n + 6 -element XFinSequence of NAT : S4[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by HILB10_3:24;
defpred S5[ XFinSequence of NAT ] means 1 * ($1 . U) > (1 * ($1 . Y1)) + 0;
A5: { p where p is n + 6 -element XFinSequence of NAT : S5[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by HILB10_3:7;
defpred S6[ XFinSequence of NAT ] means ( 1 * ($1 . V) = [\((1 * ($1 . Y2)) / (1 * ($1 . Y3)))/] & 1 * ($1 . Y3) <> 0 );
A6: { p where p is n + 6 -element XFinSequence of NAT : S6[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by Th28;
defpred S7[ XFinSequence of NAT ] means 1 * ($1 . Y),1 * ($1 . V) are_congruent_mod 1 * ($1 . U);
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:21;
defpred S8[ XFinSequence of NAT ] means 1 * ($1 . U) > (1 * ($1 . Y)) + 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 1 * ($1 . X) >= (1 * ($1 . Z)) + 0;
A9: { p where p is n + 6 -element XFinSequence of NAT : S9[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by HILB10_3:8;
defpred S10[ XFinSequence of NAT ] means 1 * ($1 . U1) = (1 * ($1 . U)) + 1;
A10: { p where p is n + 6 -element XFinSequence of NAT : S10[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) by HILB10_3:6;
defpred S11[ XFinSequence of NAT ] means ( S2[$1] & S3[$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(A2, A3);
 defpred S12[ XFinSequence of NAT ] means ( S11[$1] & S4[$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, A4);
 defpred S13[ XFinSequence of NAT ] means ( S12[$1] & S5[$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, A5);
 defpred S14[ XFinSequence of NAT ] means ( S13[$1] & S6[$1] );
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, A6);
 defpred S15[ XFinSequence of NAT ] means ( S14[$1] & S7[$1] );
A15: { p where p is n + 6 -element XFinSequence of NAT : S15[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A14, A7);
 defpred S16[ XFinSequence of NAT ] means ( S15[$1] & S8[$1] );
A16: { p where p is n + 6 -element XFinSequence of NAT : S16[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A15, A8);
 defpred S17[ XFinSequence of NAT ] means ( S16[$1] & S9[$1] );
A17: { p where p is n + 6 -element XFinSequence of NAT : S17[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A16, A9);
 defpred S18[ XFinSequence of NAT ] means ( S17[$1] & S10[$1] );
set PP = { p where p is n + 6 -element XFinSequence of NAT : S18[p] } ;
A18: { p where p is n + 6 -element XFinSequence of NAT : S18[p] } is diophantine Subset of ((n + 6) -xtuples_of NAT) from HILB10_3:sch 3(A17, A10);
 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 : S18[p] } } as diophantine Subset of (n -xtuples_of NAT) by NAT_1:11, HILB10_3:5, A18;
A19: 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
A20: ( x = p | n & p in { p where p is n + 6 -element XFinSequence of NAT : S18[p] } ) ;
ex q being n + 6 -element XFinSequence of NAT st
( q = p & S18[q] ) by A20;
then A21: ( p . X >= p . Z & p . Y = (p . X) choose (p . Z) ) by Th16;
( (p | n) . X = p . i1 & (p | n) . Y = p . i2 & (p | n) . Z = p . i3 ) by A1, HILB10_3:4;
hence x in { p where p is n -element XFinSequence of NAT : S1[p] } by A21, A20; :: 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
A22: ( x = p & S1[p] ) ;
consider u, v, y1, y2, y3 being Nat such that
A23: ( y1 = (p . i1) |^ (p . i3) & y2 = (u + 1) |^ (p . i1) & y3 = u |^ (p . i3) & u > y1 & v = [\(y2 / y3)/] & p . i2,v are_congruent_mod u & p . i2 < u & p . i1 >= p . i3 ) by A22, Th16;
reconsider u1 = u + 1 as Element of NAT ;
reconsider u = u, v = v, y1 = y1, y2 = y2, y3 = y3 as Element of NAT by ORDINAL1:def 12;
set Y = ((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>;
set PY = p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>);
A24: ( len p = n & len (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) = 6 ) by CARD_1:def 7;
A25: (p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)) | n = p by A24, AFINSQ_1:57;
A26: (p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)) . i3 = ((p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)) | n) . i3 by A1, HILB10_3:4
.= p . i3 by A24, AFINSQ_1:57 ;
0 in dom (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) by AFINSQ_1:66;
then A27: (p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)) . (n + 0) = (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) . 0 by A24, AFINSQ_1:def 3
.= u by AFINSQ_1:47 ;
1 in dom (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) by A24, AFINSQ_1:66;
then A28: (p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)) . (n + 1) = (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) . 1 by A24, AFINSQ_1:def 3
.= v by AFINSQ_1:47 ;
2 in dom (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) by A24, AFINSQ_1:66;
then A29: (p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)) . (n + 2) = (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) . 2 by A24, AFINSQ_1:def 3
.= y1 by AFINSQ_1:47 ;
3 in dom (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) by A24, AFINSQ_1:66;
then A30: (p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)) . (n + 3) = (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) . 3 by A24, AFINSQ_1:def 3
.= y2 by AFINSQ_1:47 ;
4 in dom (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) by A24, AFINSQ_1:66;
then A31: (p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)) . (n + 4) = (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) . 4 by A24, AFINSQ_1:def 3
.= y3 by AFINSQ_1:47 ;
5 in dom (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) by A24, AFINSQ_1:66;
then A32: (p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)) . (n + 5) = (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) . 5 by A24, AFINSQ_1:def 3
.= u1 by AFINSQ_1:47 ;
S18[p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>)] by A23, A25, A1, HILB10_3:4, A26, A27, A28, A29, A30, A31, A32;
then p ^ (((((<%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>) in { p where p is n + 6 -element XFinSequence of NAT : S18[p] } ;
hence x in PPn by A25, A22; :: thesis: verum
end;
hence { p where p is n -element XFinSequence of NAT : ( p . i1 >= p . i3 & p . i2 = (p . i1) choose (p . i3) ) } is diophantine Subset of (n -xtuples_of NAT) by A19, XBOOLE_0:def 10; :: thesis: verum