let k be Nat; :: thesis: for P being INT -valued Polynomial of (k + 1),F_Real

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i1 holds

{ p where p is b_{2} -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

set k1 = k + 1;

let P be INT -valued Polynomial of (k + 1),F_Real; :: thesis: for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i1 holds

{ p where p is b_{1} -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

let n be Nat; :: thesis: for i1, i2 being Element of n st k + 1 <= n & k in i1 holds

{ p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

let i1, i2 be Element of n; :: thesis: ( k + 1 <= n & k in i1 implies { p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT) )

assume A1: ( k + 1 <= n & k in i1 ) ; :: thesis: { p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

reconsider FR = F_Real as Field ;

set X = n + 1;

A2: ( n < n + 1 & k < n ) by A1, NAT_1:13;

then n in Segm (n + 1) by NAT_1:44;

then reconsider N = n, I1 = i1, I2 = i2 as Element of n + 1 by HILB10_3:2;

defpred S_{1}[ XFinSequence of NAT ] means 1 * ($1 . N),0 * ($1 . I1) are_congruent_mod 1 * ($1 . I2);

A3: { p where p is n + 1 -element XFinSequence of NAT : S_{1}[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT)
by HILB10_3:21;

defpred S_{2}[ XFinSequence of NAT ] means for q being k + 1 -element XFinSequence of NAT st q = <%($1 . I1)%> ^ ($1 | k) holds

1 * ($1 . N) = eval (P,(@ q));

defpred S_{3}[ XFinSequence of NAT ] means for q being k + 1 -element XFinSequence of NAT st q = <%($1 . I1)%> ^ ($1 | k) holds

(- 1) * ($1 . N) = eval (P,(@ q));

defpred S_{4}[ XFinSequence of NAT ] means ( S_{2}[$1] or S_{3}[$1] );

A4: ( k + 1 < n + 1 & k in I1 ) by A1, NAT_1:13;

then A5: { p where p is n + 1 -element XFinSequence of NAT : S_{2}[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT)
by Th14;

A6: { p where p is n + 1 -element XFinSequence of NAT : S_{3}[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT)
by Th14, A4;

{ p where p is n + 1 -element XFinSequence of NAT : ( S_{2}[p] or S_{3}[p] ) } is diophantine Subset of ((n + 1) -xtuples_of NAT)
from HILB10_3:sch 1(A5, A6);

then A7: { p where p is n + 1 -element XFinSequence of NAT : S_{4}[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT)
;

set PQ = { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } ;

A8: { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } is diophantine Subset of ((n + 1) -xtuples_of NAT)
from HILB10_3:sch 3(A3, A7);

set PQr = { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } } ;

defpred S_{5}[ XFinSequence of NAT ] means for q being k + 1 -element XFinSequence of NAT st q = <%($1 . i1)%> ^ ($1 | k) holds

eval (P,(@ q)), 0 are_congruent_mod $1 . i2;

set S = { p where p is n -element XFinSequence of NAT : S_{5}[p] } ;

A9: { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:5, A2, A8;

A10: Segm k c= Segm n by A2, NAT_1:39;

A11: { p where p is n -element XFinSequence of NAT : S_{5}[p] } c= { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } }
_{1}[p] & S_{4}[p] ) } } c= { p where p is n -element XFinSequence of NAT : S_{5}[p] }

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT) by A9, A11, XBOOLE_0:def 10; :: thesis: verum

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i1 holds

{ p where p is b

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

set k1 = k + 1;

let P be INT -valued Polynomial of (k + 1),F_Real; :: thesis: for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i1 holds

{ p where p is b

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

let n be Nat; :: thesis: for i1, i2 being Element of n st k + 1 <= n & k in i1 holds

{ p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

let i1, i2 be Element of n; :: thesis: ( k + 1 <= n & k in i1 implies { p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT) )

assume A1: ( k + 1 <= n & k in i1 ) ; :: thesis: { p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT)

reconsider FR = F_Real as Field ;

set X = n + 1;

A2: ( n < n + 1 & k < n ) by A1, NAT_1:13;

then n in Segm (n + 1) by NAT_1:44;

then reconsider N = n, I1 = i1, I2 = i2 as Element of n + 1 by HILB10_3:2;

defpred S

A3: { p where p is n + 1 -element XFinSequence of NAT : S

defpred S

1 * ($1 . N) = eval (P,(@ q));

defpred S

(- 1) * ($1 . N) = eval (P,(@ q));

defpred S

A4: ( k + 1 < n + 1 & k in I1 ) by A1, NAT_1:13;

then A5: { p where p is n + 1 -element XFinSequence of NAT : S

A6: { p where p is n + 1 -element XFinSequence of NAT : S

{ p where p is n + 1 -element XFinSequence of NAT : ( S

then A7: { p where p is n + 1 -element XFinSequence of NAT : S

set PQ = { p where p is n + 1 -element XFinSequence of NAT : ( S

A8: { p where p is n + 1 -element XFinSequence of NAT : ( S

set PQr = { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S

defpred S

eval (P,(@ q)), 0 are_congruent_mod $1 . i2;

set S = { p where p is n -element XFinSequence of NAT : S

A9: { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S

A10: Segm k c= Segm n by A2, NAT_1:39;

A11: { p where p is n -element XFinSequence of NAT : S

proof

{ (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is n -element XFinSequence of NAT : S_{5}[p] } or y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } } )

assume y in { p where p is n -element XFinSequence of NAT : S_{5}[p] }
; :: thesis: y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } }

then consider p being n -element XFinSequence of NAT such that

A12: ( y = p & S_{5}[p] )
;

A13: ( len p = n & len <%(p . i1)%> = 1 ) by CARD_1:def 7;

then len (p | k) = k by A2, AFINSQ_1:54;

then len (<%(p . i1)%> ^ (p | k)) = k + 1 by A13, AFINSQ_1:17;

then reconsider pi1pk = <%(p . i1)%> ^ (p | k) as k + 1 -element XFinSequence of NAT by CARD_1:def 7;

reconsider E = |.(eval (P,(@ pi1pk))).| as Element of NAT ;

reconsider pE = p ^ <%E%> as n + 1 -element XFinSequence of NAT ;

A14: pE | n = p by A13, AFINSQ_1:57;

A15: pE . N = E by A13, AFINSQ_1:36;

A16: ( pE . I1 = p . i1 & pE . I2 = p . i2 ) by A1, A14, HILB10_3:4;

A17: pE | k = p | k by A10, A14, RELAT_1:74;

then A19: pE . i2 divides - ((eval (P,(@ pi1pk))) - 0) by INT_2:10, INT_2:15;

1 * (pE . N),0 * (pE . I1) are_congruent_mod 1 * (pE . I2)_{1}[p] & S_{4}[p] ) }
by A18;

hence y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } }
by A12, A14; :: thesis: verum

end;assume y in { p where p is n -element XFinSequence of NAT : S

then consider p being n -element XFinSequence of NAT such that

A12: ( y = p & S

A13: ( len p = n & len <%(p . i1)%> = 1 ) by CARD_1:def 7;

then len (p | k) = k by A2, AFINSQ_1:54;

then len (<%(p . i1)%> ^ (p | k)) = k + 1 by A13, AFINSQ_1:17;

then reconsider pi1pk = <%(p . i1)%> ^ (p | k) as k + 1 -element XFinSequence of NAT by CARD_1:def 7;

reconsider E = |.(eval (P,(@ pi1pk))).| as Element of NAT ;

reconsider pE = p ^ <%E%> as n + 1 -element XFinSequence of NAT ;

A14: pE | n = p by A13, AFINSQ_1:57;

A15: pE . N = E by A13, AFINSQ_1:36;

A16: ( pE . I1 = p . i1 & pE . I2 = p . i2 ) by A1, A14, HILB10_3:4;

A17: pE | k = p | k by A10, A14, RELAT_1:74;

A18: now :: thesis: ( S_{2}[pE] or S_{3}[pE] )

eval (P,(@ pi1pk)), 0 are_congruent_mod pE . i2
by A12, A16;end;

then A19: pE . i2 divides - ((eval (P,(@ pi1pk))) - 0) by INT_2:10, INT_2:15;

1 * (pE . N),0 * (pE . I1) are_congruent_mod 1 * (pE . I2)

proof
end;

then
pE in { p where p is n + 1 -element XFinSequence of NAT : ( Shence y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S

proof

hence
{ p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i1)%> ^ (p | k) holds
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } } or y in { p where p is n -element XFinSequence of NAT : S_{5}[p] } )

assume y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } }
; :: thesis: y in { p where p is n -element XFinSequence of NAT : S_{5}[p] }

then consider pP being n + 1 -element XFinSequence of NAT such that

A20: ( y = pP | n & pP in { p where p is n + 1 -element XFinSequence of NAT : ( S_{1}[p] & S_{4}[p] ) } )
;

A21: ex q being n + 1 -element XFinSequence of NAT st

( q = pP & S_{1}[q] & S_{4}[q] )
by A20;

len pP = n + 1 by CARD_1:def 7;

then A22: len (pP | n) = n by A2, AFINSQ_1:54;

then reconsider p = pP | n as n -element XFinSequence of NAT by CARD_1:def 7;

A23: len <%(p . i1)%> = 1 by CARD_1:def 7;

len (p | k) = k by A2, A22, AFINSQ_1:54;

then len (<%(p . i1)%> ^ (p | k)) = k + 1 by A23, AFINSQ_1:17;

then reconsider pi1pk = <%(p . i1)%> ^ (p | k) as k + 1 -element XFinSequence of NAT by CARD_1:def 7;

A24: ( pP . I1 = p . i1 & pP . I2 = p . i2 ) by A1, HILB10_3:4;

A25: pP . I2 divides (pP . N) - 0 by A21, INT_2:15;

eval (P,(@ pi1pk)), 0 are_congruent_mod p . i2_{5}[p]
;

hence y in { p where p is n -element XFinSequence of NAT : S_{5}[p] }
by A20; :: thesis: verum

end;assume y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S

then consider pP being n + 1 -element XFinSequence of NAT such that

A20: ( y = pP | n & pP in { p where p is n + 1 -element XFinSequence of NAT : ( S

A21: ex q being n + 1 -element XFinSequence of NAT st

( q = pP & S

len pP = n + 1 by CARD_1:def 7;

then A22: len (pP | n) = n by A2, AFINSQ_1:54;

then reconsider p = pP | n as n -element XFinSequence of NAT by CARD_1:def 7;

A23: len <%(p . i1)%> = 1 by CARD_1:def 7;

len (p | k) = k by A2, A22, AFINSQ_1:54;

then len (<%(p . i1)%> ^ (p | k)) = k + 1 by A23, AFINSQ_1:17;

then reconsider pi1pk = <%(p . i1)%> ^ (p | k) as k + 1 -element XFinSequence of NAT by CARD_1:def 7;

A24: ( pP . I1 = p . i1 & pP . I2 = p . i2 ) by A1, HILB10_3:4;

A25: pP . I2 divides (pP . N) - 0 by A21, INT_2:15;

eval (P,(@ pi1pk)), 0 are_congruent_mod p . i2

proof

then
S
pi1pk = <%(pP . i1)%> ^ (pP | k)
by A24, A10, RELAT_1:74;

then ( 1 * (pP . N) = eval (P,(@ pi1pk)) or (- 1) * (pP . N) = eval (P,(@ pi1pk)) ) by A21;

end;then ( 1 * (pP . N) = eval (P,(@ pi1pk)) or (- 1) * (pP . N) = eval (P,(@ pi1pk)) ) by A21;

hence y in { p where p is n -element XFinSequence of NAT : S

eval (P,(@ q)), 0 are_congruent_mod p . i2 } is diophantine Subset of (n -xtuples_of NAT) by A9, A11, XBOOLE_0:def 10; :: thesis: verum