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_{1}[ XFinSequence of NAT ] means a * ($1 . i1) > (b * ($1 . i2)) + c;

defpred S_{2}[ XFinSequence of NAT ] means a * ($1 . i1) = (b * ($1 . i2)) + c;

defpred S_{3}[ XFinSequence of NAT ] means ( S_{1}[$1] or S_{2}[$1] );

defpred S_{4}[ XFinSequence of NAT ] means a * ($1 . i1) >= (b * ($1 . i2)) + c;

A1: { p where p is n -element XFinSequence of NAT : S_{1}[p] } is diophantine Subset of (n -xtuples_of NAT)
by Th7;

A2: { p where p is n -element XFinSequence of NAT : S_{2}[p] } is diophantine Subset of (n -xtuples_of NAT)
by Th6;

A3: { p where p is n -element XFinSequence of NAT : ( S_{1}[p] or S_{2}[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_{3}[p] iff S_{4}[p] )
by XXREAL_0:1;

{ p where p is n -element XFinSequence of NAT : S_{3}[p] } = { q where q is n -element XFinSequence of NAT : S_{4}[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

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

defpred S

defpred S

defpred S

A1: { p where p is n -element XFinSequence of NAT : S

A2: { p where p is n -element XFinSequence of NAT : S

A3: { p where p is n -element XFinSequence of NAT : ( S

A4: for p being n -element XFinSequence of NAT holds

( S

{ p where p is n -element XFinSequence of NAT : S

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