let n be Nat; for a, b being Integer
for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
let a, b be Integer; for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; { p where p is n -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
defpred S1[ Nat, Nat, Integer] means a * $1 > $3 + 0;
deffunc H1( Nat, Nat, Nat) -> set = (b * $2) * $3;
defpred S2[ XFinSequence of NAT ] means a * ($1 . i1) > ((b * ($1 . i2)) * ($1 . i3)) + 0;
defpred S3[ XFinSequence of NAT ] means a * ($1 . i1) > (b * ($1 . i2)) * ($1 . i3);
A1:
for n being Nat
for i1, i2, i3 being Element of n
for c being Integer holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,c * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT)
by Th7;
A2:
for n being Nat
for i1, i2, i3, i4 being Element of n
for c being Integer holds { p where p is b1 -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = c * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
by Th9;
A3:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,H1(p . i3,p . i4,p . i5)] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 5(A1, A2);
A4:
for p being n -element XFinSequence of NAT holds
( S2[p] iff S3[p] )
;
{ p where p is n -element XFinSequence of NAT : S2[p] } = { q where q is n -element XFinSequence of NAT : S3[q] }
from HILB10_3:sch 2(A4);
hence
{ p where p is n -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
by A3; verum