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 S₁[ XFinSequence of NAT ] means a * ($1 . i1) > (b * ($1 . i2)) + c;
defpred S₂[ XFinSequence of NAT ] means a * ($1 . i1) = (b * ($1 . i2)) + c;
defpred S₃[ XFinSequence of NAT ] means ( S₁[$1] or S₂[$1] );
defpred S₄[ XFinSequence of NAT ] means a * ($1 . i1) >= (b * ($1 . i2)) + c;
A1: { p where p is n -element XFinSequence of NAT : S₁[p] } is diophantine Subset of (n -xtuples_of NAT) by Th7;
A2: { p where p is n -element XFinSequence of NAT : S₂[p] } is diophantine Subset of (n -xtuples_of NAT) by Th6;
A3: { p where p is n -element XFinSequence of NAT : ( S₁[p] or S₂[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
( S₃[p] iff S₄[p] ) by XXREAL_0:1;
{ p where p is n -element XFinSequence of NAT : S₃[p] } = { q where q is n -element XFinSequence of NAT : S₄[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