let n be Nat; 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; ( 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
; { 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] }
{ p where p is n -element XFinSequence of NAT : S1[p] } c= PPn
proof
let x be
object ;
TARSKI:def 3 ( 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] }
;
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;
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; verum