let n be Nat; for a, b being Integer
for c being Nat
for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)
let a, b be Integer; for c being Nat
for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)
let c be Nat; for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; { p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)
deffunc H1( Nat, Nat, Nat) -> set = (c * $3) + (((a * c) * $1) * $3);
A1:
for n being Nat
for i1, i2, i3, i4 being Element of n
for d being Integer holds { p where p is b1 -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
proof
let n be
Nat;
for i1, i2, i3, i4 being Element of n
for d being Integer holds { p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)let i1,
i2,
i3,
i4 be
Element of
n;
for d being Integer holds { p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)let d be
Integer;
{ p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
defpred S1[
Nat,
Nat,
Integer]
means d * $1
= ((c * $2) + $3) + 0;
A2:
for
n being
Nat for
i1,
i2,
i3 being
Element of
n for
f being
Integer holds
{ p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,f * (p . i3)] } is
diophantine Subset of
(n -xtuples_of NAT)
by HILB10_3:11;
deffunc H2(
Nat,
Nat,
Nat)
-> set =
((a * c) * $1) * $3;
A3:
for
n being
Nat for
i1,
i2,
i3,
i4 being
Element of
n for
f being
Integer holds
{ p where p is b1 -element XFinSequence of NAT : H2(p . i1,p . i2,p . i3) = f * (p . i4) } is
diophantine Subset of
(n -xtuples_of NAT)
by HILB10_3:9;
A4:
for
n being
Nat for
i1,
i2,
i3,
i4,
i5 being
Element of
n holds
{ p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,H2(p . i3,p . i4,p . i5)] } is
diophantine Subset of
(n -xtuples_of NAT)
from HILB10_3:sch 5(A2, A3);
defpred S2[
XFinSequence of
NAT ]
means H1($1
. i1,$1
. i2,$1
. i3)
= d * ($1 . i4);
defpred S3[
XFinSequence of
NAT ]
means S1[$1
. i4,$1
. i3,
H2($1
. i1,$1
. i2,$1
. i3)];
A5:
for
p being
n -element XFinSequence of
NAT holds
(
S2[
p] iff
S3[
p] )
;
{ p where p is n -element XFinSequence of NAT : S2[p] } = { q where q is n -element XFinSequence of NAT : S3[q] }
from HILB10_3:sch 2(A5);
hence
{ p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = d * (p . i4) } is
diophantine Subset of
(n -xtuples_of NAT)
by A4;
verum
end;
defpred S1[ Nat, Nat, Integer] means (b * $1) + 0 < $3;
A6:
for n being Nat
for i1, i2, i3 being Element of n
for d being Integer holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,d * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:7;
A7:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,H1(p . i3,p . i4,p . i5)] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 5(A6, A1);
defpred S2[ Nat, Nat, Integer] means b * $1 >= $3 + 0;
A8:
for n being Nat
for i1, i2, i3 being Element of n
for d being Integer holds { p where p is b1 -element XFinSequence of NAT : S2[p . i1,p . i2,d * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:8;
deffunc H2( Nat, Nat, Nat) -> set = ((a * c) * $1) * $3;
A9:
for n being Nat
for i1, i2, i3, i4 being Element of n
for d being Integer holds { p where p is b1 -element XFinSequence of NAT : H2(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:9;
A10:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S2[p . i1,p . i2,H2(p . i3,p . i4,p . i5)] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 5(A8, A9);
defpred S3[ XFinSequence of NAT ] means S1[$1 . i2,$1 . i2,H1($1 . i1,$1 . i1,$1 . i3)];
defpred S4[ XFinSequence of NAT ] means S2[$1 . i2,$1 . i2,H2($1 . i1,$1 . i1,$1 . i3)];
defpred S5[ XFinSequence of NAT ] means ( S3[$1] & S4[$1] );
defpred S6[ XFinSequence of NAT ] means c * ($1 . i3) <> (0 * ($1 . i3)) + 0;
defpred S7[ XFinSequence of NAT ] means ( S5[$1] & S6[$1] );
defpred S8[ XFinSequence of NAT ] means ( a * ($1 . i1) = [\((b * ($1 . i2)) / (c * ($1 . i3)))/] & c * ($1 . i3) <> 0 );
A11:
{ p where p is n -element XFinSequence of NAT : S3[p] } is diophantine Subset of (n -xtuples_of NAT)
by A7;
A12:
{ p where p is n -element XFinSequence of NAT : S4[p] } is diophantine Subset of (n -xtuples_of NAT)
by A10;
{ p where p is n -element XFinSequence of NAT : ( S3[p] & S4[p] ) } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 3(A11, A12);
then A13:
{ p where p is n -element XFinSequence of NAT : S5[p] } is diophantine Subset of (n -xtuples_of NAT)
;
A14:
{ p where p is n -element XFinSequence of NAT : S6[p] } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:16;
A15:
{ p where p is n -element XFinSequence of NAT : ( S5[p] & S6[p] ) } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 3(A13, A14);
A16:
for p being n -element XFinSequence of NAT holds
( S8[p] iff S7[p] )
{ p where p is n -element XFinSequence of NAT : S8[p] } = { q where q is n -element XFinSequence of NAT : S7[q] }
from HILB10_3:sch 2(A16);
hence
{ p where p is n -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)
by A15; verum