let n be Nat; :: thesis: for a, b, c being Integer
for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) <> (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)
let a, b, c be Integer; :: thesis: for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) <> (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : a * (p . i1) <> (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)
defpred S1[ XFinSequence of NAT ] means a * ($1 . i1) > (b * ($1 . i2)) + c;
defpred S2[ XFinSequence of NAT ] means (a * ($1 . i1)) + (- c) < b * ($1 . i2);
defpred S3[ XFinSequence of NAT ] means ( S1[$1] or S2[$1] );
defpred S4[ XFinSequence of NAT ] means a * ($1 . i1) <> (b * ($1 . i2)) + c;
A1: { p where p is n -element XFinSequence of NAT : S1[p] } is diophantine Subset of (n -xtuples_of NAT) by Th7;
A2: { p where p is n -element XFinSequence of NAT : S2[p] } is diophantine Subset of (n -xtuples_of NAT) by Th7;
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);
 A4: for p being n -element XFinSequence of NAT holds
( S3[p] iff S4[p] )
proof
let p be n -element XFinSequence of NAT ; :: thesis: ( S3[p] iff S4[p] )
thus ( S3[p] implies S4[p] ) ; :: thesis: ( S4[p] implies S3[p] )
assume S4[p] ; :: thesis: S3[p]
then ( a * (p . i1) > (b * (p . i2)) + c or a * (p . i1) < (b * (p . i2)) + c ) by XXREAL_0:1;
then ( a * (p . i1) > (b * (p . i2)) + c or (a * (p . i1)) - c < b * (p . i2) ) by XREAL_1:19;
hence S3[p] ; :: thesis: verum
end;
{ p where p is n -element XFinSequence of NAT : S3[p] } = { q where q is n -element XFinSequence of NAT : S4[q] } from HILB10_3:sch 2(A4);
 hence { p where p is n -element XFinSequence of NAT : a * (p . i1) <> (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT) by A3; :: thesis: verum