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 : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } is diophantine Subset of ()

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 : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } is diophantine Subset of ()
let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } is diophantine Subset of ()
set F = F_Real ;
set n1 = n + 1;
set D = { p where p is n -element XFinSequence of NAT : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } ;
{ p where p is n -element XFinSequence of NAT : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } 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 : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } or y in n -xtuples_of NAT )
assume y in { p where p is n -element XFinSequence of NAT : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } ; :: thesis:
then ex p being n -element XFinSequence of NAT st
( y = p & ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) ) ;
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 : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } as Subset of () ;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } is diophantine Subset of ()
then D is diophantine Subset of () ;
hence { p where p is n -element XFinSequence of NAT : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } is diophantine Subset of () ; :: thesis: verum
end;
suppose A1: n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } is diophantine Subset of ()
A2: n < n + 1 by NAT_1:13;
n in Segm (n + 1) by ;
then reconsider I = i1, J = i2, K = i3, N = n as Element of n + 1 by Th2;
reconsider ar = a, br = b, cr = c as integer Element of F_Real by XREAL_0:def 1;
set Q = ((ar * (1_1 (I,F_Real))) - (br * (1_1 (J,F_Real)))) - (cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real))));
reconsider Q = ((ar * (1_1 (I,F_Real))) - (br * (1_1 (J,F_Real)))) - (cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))) as INT -valued Polynomial of (n + 1),F_Real ;
for s being object holds
( s in D iff ex x being n -element XFinSequence of NAT ex y being 1 -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 1 -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 1 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 ) ) :: thesis: ( ex x being n -element XFinSequence of NAT ex y being 1 -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 1 -element XFinSequence of NAT st
( s = x & eval (Q,(@ (x ^ y))) = 0 )

then consider p being n -element XFinSequence of NAT such that
A3: ( s = p & ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) ) ;
consider z being Nat such that
A4: a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) by A3;
reconsider z = z as Element of NAT by ORDINAL1:def 12;
reconsider Z = <%z%> as 1 -element XFinSequence of NAT ;
take p ; :: thesis: ex y being 1 -element XFinSequence of NAT st
( s = p & eval (Q,(@ (p ^ y))) = 0 )

take Z ; :: thesis: ( s = p & eval (Q,(@ (p ^ Z))) = 0 )
set P = @ (p ^ Z);
A5: len p = n by CARD_1:def 7;
then A6: ( (@ (p ^ Z)) . I = p . i1 & (@ (p ^ Z)) . J = p . i2 & (@ (p ^ Z)) . K = p . i3 ) by ;
A7: ( eval ((1_1 (I,F_Real)),(@ (p ^ Z))) = (@ (p ^ Z)) . I & eval ((1_1 (J,F_Real)),(@ (p ^ Z))) = (@ (p ^ Z)) . J & eval ((1_1 (K,F_Real)),(@ (p ^ Z))) = (@ (p ^ Z)) . K & eval ((1_1 (N,F_Real)),(@ (p ^ Z))) = (@ (p ^ Z)) . N & eval ((1_ ((n + 1),F_Real)),(@ (p ^ Z))) = 1. F_Real ) by ;
A8: eval ((cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))),(@ (p ^ Z))) = cr * (eval (((1_1 (K,F_Real)) *' (1_1 (N,F_Real))),(@ (p ^ Z)))) by POLYNOM7:29
.= cr * ((eval ((1_1 (K,F_Real)),(@ (p ^ Z)))) * (eval ((1_1 (N,F_Real)),(@ (p ^ Z))))) by POLYNOM2:25
.= c * (((@ (p ^ Z)) . K) * ((@ (p ^ Z)) . N)) by A7 ;
eval (Q,(@ (p ^ Z))) = (eval (((ar * (1_1 (I,F_Real))) - (br * (1_1 (J,F_Real)))),(@ (p ^ Z)))) - (eval ((cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))),(@ (p ^ Z)))) by POLYNOM2:24
.= ((eval ((ar * (1_1 (I,F_Real))),(@ (p ^ Z)))) - (eval ((br * (1_1 (J,F_Real))),(@ (p ^ Z))))) - (eval ((cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))),(@ (p ^ Z)))) by POLYNOM2:24
.= ((ar * (eval ((1_1 (I,F_Real)),(@ (p ^ Z))))) - (eval ((br * (1_1 (J,F_Real))),(@ (p ^ Z))))) - (eval ((cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))),(@ (p ^ Z)))) by POLYNOM7:29
.= ((ar * (eval ((1_1 (I,F_Real)),(@ (p ^ Z))))) - (br * (eval ((1_1 (J,F_Real)),(@ (p ^ Z)))))) - (eval ((cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))),(@ (p ^ Z)))) by POLYNOM7:29
.= ((ar * ((@ (p ^ Z)) . I)) - (br * ((@ (p ^ Z)) . J))) - ((c * ((@ (p ^ Z)) . K)) * ((@ (p ^ Z)) . N)) by A7, A8
.= ((a * (p . i1)) - (b * (p . i2))) - ((c * (p . i3)) * z) by
.= 0 by A4 ;
hence ( s = p & eval (Q,(@ (p ^ Z))) = 0 ) by A3; :: thesis: verum
end;
given p being n -element XFinSequence of NAT , Z being 1 -element XFinSequence of NAT such that A9: ( s = p & eval (Q,(@ (p ^ Z))) = 0 ) ; :: thesis: s in D
set P = @ (p ^ Z);
len p = n by CARD_1:def 7;
then A10: ( (@ (p ^ Z)) . I = p . i1 & (@ (p ^ Z)) . J = p . i2 & (@ (p ^ Z)) . K = p . i3 ) by ;
A11: ( eval ((1_1 (I,F_Real)),(@ (p ^ Z))) = (@ (p ^ Z)) . I & eval ((1_1 (J,F_Real)),(@ (p ^ Z))) = (@ (p ^ Z)) . J & eval ((1_1 (K,F_Real)),(@ (p ^ Z))) = (@ (p ^ Z)) . K & eval ((1_1 (N,F_Real)),(@ (p ^ Z))) = (@ (p ^ Z)) . N & eval ((1_ ((n + 1),F_Real)),(@ (p ^ Z))) = 1. F_Real ) by ;
A12: eval ((cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))),(@ (p ^ Z))) = cr * (eval (((1_1 (K,F_Real)) *' (1_1 (N,F_Real))),(@ (p ^ Z)))) by POLYNOM7:29
.= cr * ((eval ((1_1 (K,F_Real)),(@ (p ^ Z)))) * (eval ((1_1 (N,F_Real)),(@ (p ^ Z))))) by POLYNOM2:25
.= c * (((@ (p ^ Z)) . K) * ((@ (p ^ Z)) . N)) by A11 ;
eval (Q,(@ (p ^ Z))) = (eval (((ar * (1_1 (I,F_Real))) - (br * (1_1 (J,F_Real)))),(@ (p ^ Z)))) - (eval ((cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))),(@ (p ^ Z)))) by POLYNOM2:24
.= ((eval ((ar * (1_1 (I,F_Real))),(@ (p ^ Z)))) - (eval ((br * (1_1 (J,F_Real))),(@ (p ^ Z))))) - (eval ((cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))),(@ (p ^ Z)))) by POLYNOM2:24
.= ((ar * (eval ((1_1 (I,F_Real)),(@ (p ^ Z))))) - (eval ((br * (1_1 (J,F_Real))),(@ (p ^ Z))))) - (eval ((cr * ((1_1 (K,F_Real)) *' (1_1 (N,F_Real)))),(@ (p ^ Z)))) by POLYNOM7:29
.= ((ar * (eval ((1_1 (I,F_Real)),(@ (p ^ Z))))) - (br * (eval ((1_1 (J,F_Real)),(@ (p ^ Z)))))) - (c * (((@ (p ^ Z)) . K) * ((@ (p ^ Z)) . N))) by
.= ((a * (p . i1)) - (b * (p . i2))) - ((c * (p . i3)) * ((@ (p ^ Z)) . N)) by ;
then a * (p . i1) = (b * (p . i2)) + ((((@ (p ^ Z)) . N) * c) * (p . i3)) by A9;
hence s in D by A9; :: thesis: verum
end;
then D is diophantine ;
hence { p where p is n -element XFinSequence of NAT : ex z being Nat st a * (p . i1) = (b * (p . i2)) + ((z * c) * (p . i3)) } is diophantine Subset of () ; :: thesis: verum
end;
end;