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 ()

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 ()

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 ()

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 () )

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 ()

reconsider FR = F_Real as Field ;
set X = n + 1;
A2: ( n < n + 1 & k < n ) by ;
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 ;
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 ;
{ 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 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 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 () by ;
A10: Segm k c= Segm n by ;
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 ;
then len (<%(p . i1)%> ^ (p | k)) = k + 1 by ;
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 ;
A15: pE . N = E by ;
A16: ( pE . I1 = p . i1 & pE . I2 = p . i2 ) by ;
A17: pE | k = p | k by ;
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] )
end;
suppose E = - (eval (P,(@ pi1pk))) ; :: thesis: ( S2[pE] or S3[pE] )
end;
end;
end;
eval (P,(@ pi1pk)), 0 are_congruent_mod pE . i2 by ;
then A19: pE . i2 divides - ((eval (P,(@ pi1pk))) - 0) by ;
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 ; :: 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 - () by A19;
hence 1 * (pE . N),0 * (pE . I1) are_congruent_mod 1 * (pE . I2) by ; :: 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 ; :: 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 ;
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 ;
then len (<%(p . i1)%> ^ (p | k)) = k + 1 by ;
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 ;
A25: pP . I2 divides (pP . N) - 0 by ;
eval (P,(@ pi1pk)), 0 are_congruent_mod p . i2
proof
pi1pk = <%(pP . i1)%> ^ (pP | k) by ;
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 ; :: 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 ;
hence eval (P,(@ pi1pk)), 0 are_congruent_mod p . i2 by ; :: 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 () by ; :: thesis: verum