let n be Nat; :: thesis: for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT)
set n2 = n + 2;
defpred S1[ XFinSequence of NAT ] means ( $1 . i3 = Product ((($1 . i2) + 1) + (- (idseq ($1 . i1)))) & $1 . i2 > $1 . i1 );
set RR = { p where p is n -element XFinSequence of NAT : S1[p] } ;
per cases ( n = 0 or n <> 0 ) ;
suppose A1: n = 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT)
{ p where p is n -element XFinSequence of NAT : S1[p] } c= n -xtuples_of NAT
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 n -xtuples_of NAT )
assume x in { p where p is n -element XFinSequence of NAT : S1[p] } ; :: thesis: x in n -xtuples_of NAT
then ex p being n -element XFinSequence of NAT st
( x = p & S1[p] ) ;
hence x in n -xtuples_of NAT by HILB10_2:def 5; :: thesis: verum
end;
hence { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT) by A1; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT)
hence { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT) by Th37; :: thesis: verum
end;
end;