let n be Nat; :: thesis: for a, b, c, d 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)) + (c * (p . i3))) + d } is diophantine Subset of (n -xtuples_of NAT)
let a, b, c, d 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)) + (c * (p . i3))) + d } 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))) + d } is diophantine Subset of (n -xtuples_of NAT)
set F = F_Real ;
reconsider ar = a, br = b, cr = c, dr = d as integer Element of F_Real by XREAL_0:def 1;
set D = { p where p is n -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } ;
{ p where p is n -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } c= n -xtuples_of NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is n -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } or y in n -xtuples_of NAT )
assume y in { p where p is n -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } ; :: thesis: y in n -xtuples_of NAT
then ex p being n -element XFinSequence of NAT st
( y = p & a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d ) ;
hence y in n -xtuples_of NAT by HILB10_2:def 5; :: thesis: verum

end;

then reconsider D = { p where p is n -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } as Subset of (n -xtuples_of NAT) ;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } is diophantine Subset of (n -xtuples_of NAT)

then D is diophantine Subset of (n -xtuples_of NAT) ;
hence { p where p is n -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } is diophantine Subset of (n -xtuples_of NAT) ; :: thesis: verum

end;

suppose A1: n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } is diophantine Subset of (n -xtuples_of NAT)

set Q = (((ar * (1_1 (i1,F_Real))) - (br * (1_1 (i2,F_Real)))) - (cr * (1_1 (i3,F_Real)))) - (dr * (1_ (n,F_Real)));
reconsider Q = (((ar * (1_1 (i1,F_Real))) - (br * (1_1 (i2,F_Real)))) - (cr * (1_1 (i3,F_Real)))) - (dr * (1_ (n,F_Real))) as INT -valued Polynomial of (n + 0),F_Real ;
for s being object holds
( s in D iff ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 ) )

proof

let s be object ; :: thesis: ( s in D iff ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 ) )
thus ( s in D implies ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 ) ) :: thesis: ( ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 ) implies s in D )

proof

assume s in D ; :: thesis: ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 )
then consider p being n -element XFinSequence of NAT such that
A2: ( s = p & a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d ) ;
reconsider Z = <%> NAT as 0 -element XFinSequence of NAT ;
take pZ = p; :: thesis: ex y being 0 -element XFinSequence of NAT st
( s = pZ & eval (Q,(@ (pZ ^ y))) = 0 )
take Z ; :: thesis: ( s = pZ & eval (Q,(@ (pZ ^ Z))) = 0 )
A3: eval ((dr * (1_ (n,F_Real))),(@ p)) = dr * (eval ((1_ (n,F_Real)),(@ p))) by POLYNOM7:29
.= dr * (1. F_Real) by POLYNOM2:21
.= d ;
A4: eval ((ar * (1_1 (i1,F_Real))),(@ p)) = ar * (eval ((1_1 (i1,F_Real)),(@ p))) by POLYNOM7:29
.= a * (p . i1) by A1, Th1 ;
A5: eval ((br * (1_1 (i2,F_Real))),(@ p)) = br * (eval ((1_1 (i2,F_Real)),(@ p))) by POLYNOM7:29
.= b * (p . i2) by A1, Th1 ;
A6: eval ((cr * (1_1 (i3,F_Real))),(@ p)) = cr * (eval ((1_1 (i3,F_Real)),(@ p))) by POLYNOM7:29
.= c * (p . i3) by A1, Th1 ;
eval (Q,(@ (p ^ Z))) = (eval ((((ar * (1_1 (i1,F_Real))) - (br * (1_1 (i2,F_Real)))) - (cr * (1_1 (i3,F_Real)))),(@ p))) - (eval ((dr * (1_ (n,F_Real))),(@ p))) by POLYNOM2:24
.= ((eval (((ar * (1_1 (i1,F_Real))) - (br * (1_1 (i2,F_Real)))),(@ p))) - (eval ((cr * (1_1 (i3,F_Real))),(@ p)))) - (eval ((dr * (1_ (n,F_Real))),(@ p))) by POLYNOM2:24
.= (((eval ((ar * (1_1 (i1,F_Real))),(@ p))) - (eval ((br * (1_1 (i2,F_Real))),(@ p)))) - (eval ((cr * (1_1 (i3,F_Real))),(@ p)))) - (eval ((dr * (1_ (n,F_Real))),(@ p))) by POLYNOM2:24
.= 0 by A2, A3, A4, A5, A6 ;
hence ( s = pZ & eval (Q,(@ (pZ ^ Z))) = 0 ) by A2; :: thesis: verum

end;

given p being n -element XFinSequence of NAT , Z being 0 -element XFinSequence of NAT such that A7: ( s = p & eval (Q,(@ (p ^ Z))) = 0 ) ; :: thesis: s in D
A8: eval ((dr * (1_ (n,F_Real))),(@ p)) = dr * (eval ((1_ (n,F_Real)),(@ p))) by POLYNOM7:29
.= dr * (1. F_Real) by POLYNOM2:21
.= d ;
A9: eval ((ar * (1_1 (i1,F_Real))),(@ p)) = ar * (eval ((1_1 (i1,F_Real)),(@ p))) by POLYNOM7:29
.= a * (p . i1) by A1, Th1 ;
A10: eval ((br * (1_1 (i2,F_Real))),(@ p)) = br * (eval ((1_1 (i2,F_Real)),(@ p))) by POLYNOM7:29
.= b * (p . i2) by A1, Th1 ;
A11: eval ((cr * (1_1 (i3,F_Real))),(@ p)) = cr * (eval ((1_1 (i3,F_Real)),(@ p))) by POLYNOM7:29
.= c * (p . i3) by A1, Th1 ;
eval (Q,(@ (p ^ Z))) = (eval ((((ar * (1_1 (i1,F_Real))) - (br * (1_1 (i2,F_Real)))) - (cr * (1_1 (i3,F_Real)))),(@ p))) - (eval ((dr * (1_ (n,F_Real))),(@ p))) by POLYNOM2:24
.= ((eval (((ar * (1_1 (i1,F_Real))) - (br * (1_1 (i2,F_Real)))),(@ p))) - (eval ((cr * (1_1 (i3,F_Real))),(@ p)))) - (eval ((dr * (1_ (n,F_Real))),(@ p))) by POLYNOM2:24
.= (((eval ((ar * (1_1 (i1,F_Real))),(@ p))) - (eval ((br * (1_1 (i2,F_Real))),(@ p)))) - (eval ((cr * (1_1 (i3,F_Real))),(@ p)))) - (eval ((dr * (1_ (n,F_Real))),(@ p))) by POLYNOM2:24
.= (((a * (p . i1)) - (b * (p . i2))) - (c * (p . i3))) - d by A8, A9, A10, A11 ;
then a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d by A7;
hence s in D by A7; :: thesis: verum

end;

then D is diophantine ;
hence { p where p is n -element XFinSequence of NAT : a * (p . i1) = ((b * (p . i2)) + (c * (p . i3))) + d } is diophantine Subset of (n -xtuples_of NAT) ; :: thesis: verum

end;

end;