let n be Nat; :: thesis: for a, b, c 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) are_congruent_mod c * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
let a, b, c 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) are_congruent_mod c * (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) are_congruent_mod c * (p . i3) } is diophantine Subset of (n -xtuples_of NAT)
defpred S1[ XFinSequence of NAT ] means ex z being Nat st a * ($1 . i1) = (b * ($1 . i2)) + ((z * c) * ($1 . i3));
defpred S2[ XFinSequence of NAT ] means ex z being Nat st b * ($1 . i2) = (a * ($1 . i1)) + ((z * c) * ($1 . i3));
A1: { p where p is n -element XFinSequence of NAT : S1[p] } is diophantine Subset of (n -xtuples_of NAT) by Th10;
A2: { p where p is n -element XFinSequence of NAT : S2[p] } is diophantine Subset of (n -xtuples_of NAT) by Th10;
A3: { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } is diophantine Subset of (n -xtuples_of NAT) from HILB10_3:sch 1(A1, A2);
 set PP = { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } ;
A4: { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } c= { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } or x in { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } )
assume x in { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } ; :: thesis: x in { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) }
then consider p being n -element XFinSequence of NAT such that
A5: ( x = p & a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) ) ;
consider i being Integer such that
A6: (c * (p . i3)) * i = (a * (p . i1)) - (b * (p . i2)) by A5, INT_1:def 5;
per cases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; :: thesis: x in { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) }
then reconsider i = i as Element of NAT by INT_1:3;
a * (p . i1) = (b * (p . i2)) + ((i * c) * (p . i3)) by A6;
hence x in { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } by A5; :: thesis: verum
end;
suppose i < 0 ; :: thesis: x in { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) }
then reconsider I = - i as Element of NAT by INT_1:3;
A7: a * (p . i1) = (b * (p . i2)) + ((i * c) * (p . i3)) by A6;
a * (p . i1) = (b * (p . i2)) + (((- I) * c) * (p . i3)) by A7;
then b * (p . i2) = (a * (p . i1)) + ((I * c) * (p . i3)) ;
hence x in { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } by A5; :: thesis: verum
end;
end;
end;
{ p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } c= { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } or x in { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } )
assume x in { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } ; :: thesis: x in { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) }
then consider p being n -element XFinSequence of NAT such that
A8: ( x = p & ( S1[p] or S2[p] ) ) ;
per cases ( S1[p] or S2[p] ) by A8;
suppose S1[p] ; :: thesis: x in { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) }
then consider z being Nat such that
A9: a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) ;
z * (c * (p . i3)) = (a * (p . i1)) - (b * (p . i2)) by A9;
then a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) by INT_1:def 5;
hence x in { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } by A8; :: thesis: verum
end;
suppose S2[p] ; :: thesis: x in { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) }
then consider z being Nat such that
A10: b * (p . i2) = (a * (p . i1)) + ((z * c) * (p . i3)) ;
(- z) * (c * (p . i3)) = (a * (p . i1)) - (b * (p . i2)) by A10;
then a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) by INT_1:def 5;
hence x in { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } by A8; :: thesis: verum
end;
end;
end;
hence { p where p is n -element XFinSequence of NAT : a * (p . i1),b * (p . i2) are_congruent_mod c * (p . i3) } is diophantine Subset of (n -xtuples_of NAT) by A3, A4, XBOOLE_0:def 10; :: thesis: verum