let n be Nat; :: thesis: 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; :: thesis: 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; :: 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)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } 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)) / (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; :: thesis: 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; :: thesis: 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; :: thesis: { 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; :: thesis: 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] )
proof
let p be n -element XFinSequence of NAT ; :: thesis: ( S8[p] iff S7[p] )
thus ( S8[p] implies S7[p] ) :: thesis: ( S7[p] implies S8[p] )
proof
assume A17: S8[p] ; :: thesis: S7[p]
then A18: (a * (p . i1)) * (c * (p . i3)) <= b * (p . i2) by XREAL_1:83, INT_1:def 6;
((b * (p . i2)) / (c * (p . i3))) * (c * (p . i3)) = ((c * (p . i3)) / (c * (p . i3))) * (b * (p . i2)) by XCMPLX_1:75
.= 1 * (b * (p . i2)) by A17, XCMPLX_1:60 ;
then A19: (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) = (b * (p . i2)) - (c * (p . i3)) ;
((b * (p . i2)) / (c * (p . i3))) - 1 < a * (p . i1) by A17, INT_1:def 6;
then (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) < (a * (p . i1)) * (c * (p . i3)) by A17, XREAL_1:68;
hence S7[p] by A18, A19, XREAL_1:19; :: thesis: verum
end;
assume A20: S7[p] ; :: thesis: S8[p]
then A21: (a * (p . i1)) * (c * (p . i3)) > (b * (p . i2)) - (c * (p . i3)) by XREAL_1:19;
((b * (p . i2)) / (c * (p . i3))) * (c * (p . i3)) = ((c * (p . i3)) / (c * (p . i3))) * (b * (p . i2)) by XCMPLX_1:75
.= 1 * (b * (p . i2)) by A20, XCMPLX_1:60 ;
then (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) = (b * (p . i2)) - (c * (p . i3)) ;
then A22: a * (p . i1) > ((b * (p . i2)) / (c * (p . i3))) - 1 by A21, XREAL_1:64;
(a * (p . i1)) * (c * (p . i3)) <= b * (p . i2) by A20;
then a * (p . i1) <= (b * (p . i2)) / (c * (p . i3)) by A20, XREAL_1:77;
hence S8[p] by A20, A22, INT_1:def 6; :: thesis: verum
end;
{ 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; :: thesis: verum