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 ()

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 ()

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 ()
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 ()
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 ()
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 ()

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 ()
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 ()
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 () 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 () 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 () from 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 hence { p where p is n -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of () 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 () 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 () from 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 () 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 () 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 () from 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 () by A7;
A12: { p where p is n -element XFinSequence of NAT : S4[p] } is diophantine Subset of () by A10;
{ p where p is n -element XFinSequence of NAT : ( S3[p] & S4[p] ) } is diophantine Subset of () from then A13: { p where p is n -element XFinSequence of NAT : S5[p] } is diophantine Subset of () ;
A14: { p where p is n -element XFinSequence of NAT : S6[p] } is diophantine Subset of () by HILB10_3:16;
A15: { p where p is n -element XFinSequence of NAT : ( S5[p] & S6[p] ) } is diophantine Subset of () from 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 ;
((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 ;
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 ;
then (((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3)) < (a * (p . i1)) * (c * (p . i3)) by ;
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 ;
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 ;
(a * (p . i1)) * (c * (p . i3)) <= b * (p . i2) by A20;
then a * (p . i1) <= (b * (p . i2)) / (c * (p . i3)) by ;
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 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 () by A15; :: thesis: verum