let n be Nat; :: thesis: for a, b being Nat
for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = ((a * (p . i2)) + b) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
let a, b be Nat; :: thesis: for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = ((a * (p . i2)) + b) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
deffunc H₁( Nat, Nat, Nat) -> set = (a * $1) + b;
A1: for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : H₁(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT) by HILB10_3:15;
defpred S₁[ Nat, Nat, natural object , Nat, Nat, Nat] means 1 * $1 = (1 * $3) * $2;
A2: for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT) by HILB10_3:9;
A3: for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : S₁[p . i1,p . i2,H₁(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT) from HILB10_3:sch 4(A2, A1);
let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = ((a * (p . i2)) + b) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
defpred S₂[ XFinSequence of NAT ] means S₁[$1 . i1,$1 . i3,(a * ($1 . i2)) + b,$1 . i3,$1 . i3,$1 . i3];
defpred S₃[ XFinSequence of NAT ] means $1 . i1 = ((a * ($1 . i2)) + b) * ($1 . i3);
A4: for p being n -element XFinSequence of NAT holds
( S₂[p] iff S₃[p] ) ;
{ 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 : p . i1 = ((a * (p . i2)) + b) * (p . i3) } is diophantine Subset of (n -xtuples_of NAT) by A3; :: thesis: verum