let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: { 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 S_{1}[ Nat, Nat, Integer] means a * $1 > $3 + 0;

deffunc H_{1}( Nat, Nat, Nat) -> set = (b * $2) * $3;

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

defpred S_{3}[ 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 b_{1} -element XFinSequence of NAT : S_{1}[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 b_{1} -element XFinSequence of NAT : H_{1}(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 b_{1} -element XFinSequence of NAT : S_{1}[p . i1,p . i2,H_{1}(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

( S_{2}[p] iff S_{3}[p] )
;

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

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; :: thesis: 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; :: thesis: { 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 S

deffunc H

defpred S

defpred S

A1: for n being Nat

for i1, i2, i3 being Element of n

for c being Integer holds { p where p is b

A2: for n being Nat

for i1, i2, i3, i4 being Element of n

for c being Integer holds { p where p is b

A3: for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b

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)) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT) by A3; :: thesis: verum