let n be Nat; :: thesis: for a being Integer
for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of (n -xtuples_of NAT)
let a be Integer; :: thesis: for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of (n -xtuples_of NAT)
defpred S1[ XFinSequence of NAT ] means $1 . i1 = a * ($1 . i2);
defpred S2[ XFinSequence of NAT ] means 1 * ($1 . i1) = (a * ($1 . i2)) + 0;
A1: { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } c= { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } or y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } )
assume y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } ; :: thesis: y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 }
then consider p being n -element XFinSequence of NAT such that
A2: ( y = p & p . i1 = a * (p . i2) ) ;
1 * (p . i1) = (a * (p . i2)) + 0 by A2;
hence y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } by A2; :: thesis: verum
end;
{ q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } c= { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } or y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } )
assume y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } ; :: thesis: y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) }
then ex q being n -element XFinSequence of NAT st
( y = q & 1 * (q . i1) = (a * (q . i2)) + 0 ) ;
hence y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } ; :: thesis: verum
end;
then { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } = { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } by A1, XBOOLE_0:def 10;
hence { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of (n -xtuples_of NAT) by Th6; :: thesis: verum