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 S₁[ XFinSequence of NAT ] means ex z being Nat st a * ($1 . i1) = (b * ($1 . i2)) + ((z * c) * ($1 . i3));
defpred S₂[ 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 : S₁[p] } is diophantine Subset of (n -xtuples_of NAT) by Th10;
A2: { p where p is n -element XFinSequence of NAT : S₂[p] } is diophantine Subset of (n -xtuples_of NAT) by Th10;
A3: { p where p is n -element XFinSequence of NAT : ( S₁[p] or S₂[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 : ( S₁[p] or S₂[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 : ( S₁[p] or S₂[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 : ( S₁[p] or S₂[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 : ( S₁[p] or S₂[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 : ( S₁[p] or S₂[p] ) } by A5; :: thesis: verum

end;

suppose i < 0 ; :: thesis: x in { p where p is n -element XFinSequence of NAT : ( S₁[p] or S₂[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 : ( S₁[p] or S₂[p] ) } by A5; :: thesis: verum

end;

end;

end;

{ p where p is n -element XFinSequence of NAT : ( S₁[p] or S₂[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 : ( S₁[p] or S₂[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 : ( S₁[p] or S₂[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 & ( S₁[p] or S₂[p] ) ) ;

per cases ( S₁[p] or S₂[p] ) by A8;

suppose S₁[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 S₂[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