let k be Nat; 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; 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; 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; ( 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 )
; { 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 ;
TARSKI:def 3 ( 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] }
;
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 ( S2[pE] or S3[pE] )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)
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;
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] }
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; verum