let n be Nat; for a, b, c 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) are_congruent_mod c * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
let a, b, c 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) are_congruent_mod c * (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) are_congruent_mod c * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
defpred S1[ XFinSequence of NAT ] means ex z being Nat st a * ($1 . i1) = (b * ($1 . i2)) + ((z * c) * ($1 . i3));
defpred S2[ XFinSequence of NAT ] means ex z being Nat st b * ($1 . i2) = (a * ($1 . i1)) + ((z * c) * ($1 . i3));
A1:
{ p where p is n -element XFinSequence of NAT : S1[p] } is diophantine Subset of (n -xtuples_of NAT)
by Th10;
A2:
{ p where p is n -element XFinSequence of NAT : S2[p] } is diophantine Subset of (n -xtuples_of NAT)
by Th10;
A3:
{ p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 1(A1, A2);
set PP = { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } ;
A4:
{ p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } c= { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) }
{ p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } c= { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) }
hence
{ p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
by A3, A4, XBOOLE_0:def 10; verum