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 b2 -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 b1 -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 S1[ 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 : S1[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT) by HILB10_3:21;
defpred S2[ 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 S3[ 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 S4[ XFinSequence of NAT ] means ( S2[$1] or S3[$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 : S2[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT) by Th14;
A6: { p where p is n + 1 -element XFinSequence of NAT : S3[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT) by Th14, A4;
{ p where p is n + 1 -element XFinSequence of NAT : ( S2[p] or S3[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 : S4[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT) ;
set PQ = { p where p is n + 1 -element XFinSequence of NAT : ( S1[p] & S4[p] ) } ;
A8: { p where p is n + 1 -element XFinSequence of NAT : ( S1[p] & S4[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 : ( S1[p] & S4[p] ) } } ;
defpred S5[ 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 : S5[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 : ( S1[p] & S4[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 : S5[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 : ( S1[p] & S4[p] ) } }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is n -element XFinSequence of NAT : S5[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 : ( S1[p] & S4[p] ) } } )
assume y in { p where p is n -element XFinSequence of NAT : S5[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 : ( S1[p] & S4[p] ) } }
then consider p being n -element XFinSequence of NAT such that
A12: ( y = p & S5[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;
A18: now :: thesis: ( S2[pE] or S3[pE] )
per cases ( E = eval (P,(@ pi1pk)) or E = - (eval (P,(@ pi1pk))) ) by ABSVALUE:1;
suppose E = eval (P,(@ pi1pk)) ; :: thesis: ( S2[pE] or S3[pE] )
hence ( S2[pE] or S3[pE] ) by A13, AFINSQ_1:36, A17, A16; :: thesis: verum
end;
suppose E = - (eval (P,(@ pi1pk))) ; :: thesis: ( S2[pE] or S3[pE] )
hence ( S2[pE] or S3[pE] ) by A15, A10, A14, RELAT_1:74, A16; :: thesis: verum
end;
end;
end;
eval (P,(@ pi1pk)), 0 are_congruent_mod pE . i2 by A12, A16;
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
per cases ( E = eval (P,(@ pi1pk)) or E = - (eval (P,(@ pi1pk))) ) by ABSVALUE:1;
suppose E = eval (P,(@ pi1pk)) ; :: thesis: 1 * (pE . N),0 * (pE . I1) are_congruent_mod 1 * (pE . I2)
hence 1 * (pE . N),0 * (pE . I1) are_congruent_mod 1 * (pE . I2) by A12, A16, A15; :: thesis: verum
end;
suppose E = - (eval (P,(@ pi1pk))) ; :: thesis: 1 * (pE . N),0 * (pE . I1) are_congruent_mod 1 * (pE . I2)
then pE . i2 divides E - (- 0) by A19;
hence 1 * (pE . N),0 * (pE . I1) are_congruent_mod 1 * (pE . I2) by A15, INT_2:15; :: thesis: verum
end;
end;
end;
then pE in { p where p is n + 1 -element XFinSequence of NAT : ( S1[p] & S4[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 : ( S1[p] & S4[p] ) } } by A12, A14; :: thesis: verum
end;
{ (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S1[p] & S4[p] ) } } c= { p where p is n -element XFinSequence of NAT : S5[p] }
proof
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 : ( S1[p] & S4[p] ) } } or y in { p where p is n -element XFinSequence of NAT : S5[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 : ( S1[p] & S4[p] ) } } ; :: thesis: y in { p where p is n -element XFinSequence of NAT : S5[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 : ( S1[p] & S4[p] ) } ) ;
A21: ex q being n + 1 -element XFinSequence of NAT st
( q = pP & S1[q] & S4[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
proof
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;
per cases then ( pP . N = eval (P,(@ pi1pk)) or pP . N = - (eval (P,(@ pi1pk))) ) ;
suppose pP . N = eval (P,(@ pi1pk)) ; :: thesis: eval (P,(@ pi1pk)), 0 are_congruent_mod p . i2
hence eval (P,(@ pi1pk)), 0 are_congruent_mod p . i2 by A21, A1, HILB10_3:4; :: thesis: verum
end;
suppose A26: pP . N = - (eval (P,(@ pi1pk))) ; :: thesis: eval (P,(@ pi1pk)), 0 are_congruent_mod p . i2
p . i2 divides (- (pP . N)) - 0 by A25, INT_2:10, A24;
hence eval (P,(@ pi1pk)), 0 are_congruent_mod p . i2 by A26, INT_2:15; :: thesis: verum
end;
end;
end;
then S5[p] ;
hence y in { p where p is n -element XFinSequence of NAT : S5[p] } by A20; :: thesis: verum
end;
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
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