let n be Nat; :: thesis: for a, b, c being Integer
for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)
let a, b, c be Integer; :: thesis: for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) + c } 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 : a * (p . i1) > (b * (p . i2)) + c } is diophantine Subset of (n -xtuples_of NAT)
set F = F_Real ;
set n1 = n + 1;
set D = { p where p is n -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) + c } ;
{ p where p is n -element XFinSequence of NAT : a * (p . i1) > (b * (p . i2)) + c } 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 } 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 } ; :: 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 ) ;
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 } 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 } 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 } 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 } is diophantine Subset of (n -xtuples_of NAT)

A2: n < n + 1 by NAT_1:13;
n in Segm (n + 1) by A2, NAT_1:44;
then reconsider I = i1, J = i2, N = n as Element of n + 1 by Th2;
reconsider ar = a, br = b, cr = c + 1 as integer Element of F_Real by XREAL_0:def 1;
set Q = (((br * (1_1 (J,F_Real))) - (ar * (1_1 (I,F_Real)))) + (1_1 (N,F_Real))) + (cr * (1_ ((n + 1),F_Real)));
reconsider Q = (((br * (1_1 (J,F_Real))) - (ar * (1_1 (I,F_Real)))) + (1_1 (N,F_Real))) + (cr * (1_ ((n + 1),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 & a * (p . i1) > (b * (p . i2)) + c ) ;
(a * (p . i1)) - ((b * (p . i2)) + c) > 0 by A3, XREAL_1:50;
then reconsider pij = (a * (p . i1)) - ((b * (p . i2)) + c) as Element of NAT by INT_1:3;
reconsider pp = pij - 1 as Element of NAT by A3, XREAL_1:50, NAT_1:20;
reconsider Z = <%pp%> as 1 -element XFinSequence of NAT ;
take pZ = p; :: thesis: ex y being 1 -element XFinSequence of NAT st
( s = pZ & eval (Q,(@ (pZ ^ y))) = 0 )
take Z ; :: thesis: ( s = pZ & eval (Q,(@ (pZ ^ Z))) = 0 )
set P = @ (p ^ Z);
A4: len p = n by CARD_1:def 7;
A5: ( (@ (p ^ Z)) . I = p . i1 & (@ (p ^ Z)) . J = p . i2 ) by A4, A1, AFINSQ_1:def 3;
A6: eval ((ar * (1_1 (I,F_Real))),(@ (p ^ Z))) = ar * (eval ((1_1 (I,F_Real)),(@ (p ^ Z)))) by POLYNOM7:29
.= a * ((@ (p ^ Z)) . I) by Th1 ;
A7: eval ((br * (1_1 (J,F_Real))),(@ (p ^ Z))) = br * (eval ((1_1 (J,F_Real)),(@ (p ^ Z)))) by POLYNOM7:29
.= b * ((@ (p ^ Z)) . J) by Th1 ;
A8: eval ((cr * (1_ ((n + 1),F_Real))),(@ (p ^ Z))) = cr * (eval ((1_ ((n + 1),F_Real)),(@ (p ^ Z)))) by POLYNOM7:29
.= cr * (1. F_Real) by POLYNOM2:21 ;
A9: ( 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 (N,F_Real)),(@ (p ^ Z))) = (@ (p ^ Z)) . N & eval ((1_ ((n + 1),F_Real)),(@ (p ^ Z))) = 1. F_Real ) by Th1, POLYNOM2:21;
eval (Q,(@ (p ^ Z))) = (eval ((((br * (1_1 (J,F_Real))) - (ar * (1_1 (I,F_Real)))) + (1_1 (N,F_Real))),(@ (p ^ Z)))) + (eval ((cr * (1_ ((n + 1),F_Real))),(@ (p ^ Z)))) by POLYNOM2:23
.= ((eval (((br * (1_1 (J,F_Real))) - (ar * (1_1 (I,F_Real)))),(@ (p ^ Z)))) + (eval ((1_1 (N,F_Real)),(@ (p ^ Z))))) + (eval ((cr * (1_ ((n + 1),F_Real))),(@ (p ^ Z)))) by POLYNOM2:23
.= (((eval ((br * (1_1 (J,F_Real))),(@ (p ^ Z)))) - (eval ((ar * (1_1 (I,F_Real))),(@ (p ^ Z))))) + (eval ((1_1 (N,F_Real)),(@ (p ^ Z))))) + (eval ((cr * (1_ ((n + 1),F_Real))),(@ (p ^ Z)))) by POLYNOM2:24
.= (((b * (p . i2)) - (a * (p . i1))) + pp) + cr by A4, AFINSQ_1:36, A5, A9, A6, A7, A8
.= 0 ;
hence ( s = pZ & eval (Q,(@ (pZ ^ Z))) = 0 ) by A3; :: thesis: verum

end;

given p being n -element XFinSequence of NAT , Z being 1 -element XFinSequence of NAT such that A10: ( s = p & eval (Q,(@ (p ^ Z))) = 0 ) ; :: thesis: s in D
set P = @ (p ^ Z);
len p = n by CARD_1:def 7;
then A11: ( (@ (p ^ Z)) . I = p . i1 & (@ (p ^ Z)) . J = p . i2 ) by A1, AFINSQ_1:def 3;
A12: eval ((ar * (1_1 (I,F_Real))),(@ (p ^ Z))) = ar * (eval ((1_1 (I,F_Real)),(@ (p ^ Z)))) by POLYNOM7:29
.= a * ((@ (p ^ Z)) . I) by Th1 ;
A13: eval ((br * (1_1 (J,F_Real))),(@ (p ^ Z))) = br * (eval ((1_1 (J,F_Real)),(@ (p ^ Z)))) by POLYNOM7:29
.= b * ((@ (p ^ Z)) . J) by Th1 ;
A14: eval ((cr * (1_ ((n + 1),F_Real))),(@ (p ^ Z))) = cr * (eval ((1_ ((n + 1),F_Real)),(@ (p ^ Z)))) by POLYNOM7:29
.= cr * (1. F_Real) by POLYNOM2:21 ;
eval (Q,(@ (p ^ Z))) = (eval ((((br * (1_1 (J,F_Real))) - (ar * (1_1 (I,F_Real)))) + (1_1 (N,F_Real))),(@ (p ^ Z)))) + (eval ((cr * (1_ ((n + 1),F_Real))),(@ (p ^ Z)))) by POLYNOM2:23
.= ((eval (((br * (1_1 (J,F_Real))) - (ar * (1_1 (I,F_Real)))),(@ (p ^ Z)))) + (eval ((1_1 (N,F_Real)),(@ (p ^ Z))))) + (eval ((cr * (1_ ((n + 1),F_Real))),(@ (p ^ Z)))) by POLYNOM2:23
.= (((eval ((br * (1_1 (J,F_Real))),(@ (p ^ Z)))) - (eval ((ar * (1_1 (I,F_Real))),(@ (p ^ Z))))) + (eval ((1_1 (N,F_Real)),(@ (p ^ Z))))) + (eval ((cr * (1_ ((n + 1),F_Real))),(@ (p ^ Z)))) by POLYNOM2:24
.= (((b * (p . i2)) - (a * (p . i1))) + ((@ (p ^ Z)) . n)) + cr by Th1, A11, A12, A13, A14 ;
then a * (p . i1) = (((b * (p . i2)) + c) + 1) + ((@ (p ^ Z)) . n) by A10;
then A15: a * (p . i1) >= ((b * (p . i2)) + c) + 1 by XREAL_1:31;
((b * (p . i2)) + c) + 1 > (b * (p . i2)) + c by XREAL_1:29;
then a * (p . i1) > (b * (p . i2)) + c by A15, XXREAL_0:2;
hence s in D by A10; :: thesis: verum

end;

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

end;

end;