:: Formalization of the {MRDP } Theorem in the {M}izar System
:: by Karol P\kak
::
:: Received May 27, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0,
FUNCT_1, XXREAL_0, TARSKI, NAT_1, INT_1, ARYTM_3, ZFMISC_1, CARD_1,
ORDINAL1, ARYTM_1, PRE_POLY, QC_LANG1, GROUP_1, ALGSTR_0, RLVECT_1,
VECTSP_1, POLYNOM1, POLYNOM2, AFINSQ_1, COMPLEX1, SQUARE_1, NEWTON,
HILB10_2, INT_2, PARTFUN3, REWRITE2, REAL_1, VALUED_0, FINSEQ_2, CARD_3,
REALSET1, STRUCT_0, SGRAPH1, BINOP_2, PARTFUN1, INT_6, ORDERS_1,
FINSET_1, SUPINF_2, FUNCOP_1, WELLORD2, ALGSEQ_1, UPROOTS, MEMBERED,
RFINSEQ, JORDAN3, FUNCT_2, HILBASIS, FUNCT_4, HILB10_5;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, RELSET_1,
FUNCT_1, FINSET_1, XCMPLX_0, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, NAT_1,
ORDERS_1, FINSEQ_1, STRUCT_0, ALGSTR_0, RLVECT_1, FUNCOP_1, VECTSP_1,
GROUP_1, GROUP_4, XXREAL_0, RECDEF_1, PRE_POLY, POLYNOM1, XREAL_0, INT_1,
POLYNOM2, AFINSQ_1, AFINSQ_2, COMPLEX1, SQUARE_1, NEWTON, HILB10_2,
XXREAL_2, VALUED_0, FINSEQ_2, RVSUM_1, VALUED_1, BINOP_2, MEMBERED,
INT_2, REWRITE2, INT_6, WSIERP_1, FINSEQOP, UPROOTS, PARTFUN3, CARD_1,
NAT_D, HILBASIS, POLYNOM7, HILB10_4;
constructors NAT_D, RECDEF_1, BINOP_2, RELSET_1, GROUP_4, POLYNOM2, AFINSQ_2,
SQUARE_1, NEWTON, HILB10_2, XXREAL_2, WSIERP_1, INT_6, TRIANG_1,
FINSEQOP, FINSOP_1, UPROOTS, REWRITE2, ALGSTR_1, HILBASIS, POLYNOM7,
HILB10_4;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, CARD_1,
VALUED_0, VALUED_1, RELSET_1, INT_1, PEPIN, STRUCT_0, VECTSP_1, PRE_POLY,
MEMBERED, POLYNOM2, AFINSQ_1, HILB10_2, XXREAL_2, XXREAL_0, FINSET_1,
XCMPLX_0, NEWTON, NEWTON02, NAT_6, FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON04,
MOEBIUS2, EUCLID_9, OSALG_1, REWRITE2, INT_6, FOMODEL0, FOMODEL2,
AFINSQ_2, FUNCOP_1, WSIERP_1, ALGSTR_1, ALGSTR_0, HILBASIS, POLYNOM7,
HILB10_3, FUNCT_2, HILB10_4;
requirements NUMERALS, SUBSET, ARITHM, REAL;
definitions TARSKI, INT_6, XBOOLE_0, PARTFUN3, MEMBERED;
equalities FINSEQ_1, STRUCT_0, ALGSTR_0, POLYNOM1, VECTSP_1, FINSEQ_2,
ORDINAL1, SUBSET_1, AFINSQ_1;
expansions POLYNOM1, FUNCT_2, ORDINAL1, REWRITE2;
theorems TARSKI, FUNCT_1, CARD_1, NAT_1, ZFMISC_1, XREAL_1, XXREAL_0, NEWTON,
INT_1, FINSEQ_3, FINSEQ_1, SQUARE_1, ABSVALUE, COMPLEX1, XREAL_0, PEPIN,
RVSUM_1, FINSEQ_5, VALUED_0, FINSEQ_2, VALUED_1, INT_4, EULER_1, INT_2,
NAT_D, ORDINAL1, PREPOWER, HILB10_2, HILB10_3, BASEL_1, NEWTON04,
AFINSQ_1, XBOOLE_0, RELAT_1, INT_6, INT_5, NEWTON03, VECTSP_1, PRE_POLY,
FUNCT_2, POLYNOM1, POLYNOM2, FUNCOP_1, UPROOTS, ORDERS_5, PARTFUN1,
XBOOLE_1, RLVECT_1, BINOP_2, XXREAL_2, FINSET_1, MEMBERED, MATRPROB,
POLYNOM7, GROUP_4, NIVEN, TAYLOR_2, NAT_4, NEWTON05, AFINSQ_2, GR_CY_3,
CARD_2, WELLORD2, FUNCT_4, STIRL2_1, NECKLACE, NUMERAL2, SUBSET_1,
CARD_FIN, HILB10_4, FINSEQ_4;
schemes NAT_1, FINSEQ_1, HILB10_3, FUNCT_2, CLASSES1, AFINSQ_1;
begin :: Preliminaries
reserve i,j,n,n1,n2,m,k,l,u for Nat,
i1,i2,i3,i4,i5,i6 for Element of n,
p,q for n-element XFinSequence of NAT,
a,b,c,d,e,f for Integer;
registration
let n be Nat;
cluster idseq n -> INT -valued;
coherence;
let x be n-element natural-valued XFinSequence;
let p be INT -valued Polynomial of n,F_Real;
cluster eval(p,@x) -> integer;
coherence
proof
@x is INT-valued by HILB10_2:def 1;
hence thesis;
end;
end;
theorem Th1:
for p being INT -valued Polynomial of n, F_Real
for x,y being n-element XFinSequence of NAT st k<>0 &
for i st i in n holds k divides (x.i - y.i) holds
k divides (eval(p,@x) qua Integer) - (eval(p,@y) qua Integer)
proof
let p be INT -valued Polynomial of n, F_Real;
let x,y be n-element XFinSequence of NAT such that
A1: k<>0 and
A2: for i st i in n holds k divides (x.i - y.i);
reconsider FR=F_Real as Field;
reconsider pF=p as Polynomial of n, FR;
reconsider xF=@x,yF=@y as Function of n, the carrier of FR;
set sgmF=SgmX(BagOrder n,Support pF);
set sgm=SgmX(BagOrder n,Support p);
consider X be FinSequence of the carrier of FR such that
A3: len X = len sgmF & eval(pF,xF) = Sum X and
A4: for i be Element of NAT st 1 <= i & i <= len X holds
X/.i = (pF*sgmF)/.i * eval((sgmF/.i),xF) by POLYNOM2:def 4;
consider Y be FinSequence of the carrier of FR such that
A5: len Y = len sgmF & eval(pF,yF) = Sum Y and
A6: for i be Element of NAT st 1 <= i & i <= len Y holds
Y/.i = (pF*sgmF)/.i * eval((sgmF/.i),yF) by POLYNOM2:def 4;
reconsider Yr=Y,Xr=X as FinSequence of REAL;
defpred P[Nat] means
$1 <= len X implies Sum (Xr|$1) - Sum (Yr|$1) is Integer &
for d be Integer st d=Sum (Xr|$1) - Sum (Yr|$1) holds k divides d;
A7: P[0] by INT_2:12;
A8: for i be Nat st P[i] holds P[i+1]
proof
A9: len (p*sgm) = len sgm by CARD_1:def 7;
let i be Nat;
assume
A10: P[i];
set i1=i+1;
set O=(pF*sgmF)/.i1,O1=eval((sgmF/.i1),xF),O2 =eval((sgmF/.i1),yF);
@x is INT -valued & @y is INT -valued by HILB10_2:def 1;
then reconsider o1=O1,o2 =O2 as Integer;
assume
A11: i1 <= len X; then
reconsider S= Sum (Xr|i) - Sum (Yr|i) as Integer by A10,NAT_1:13;
A12: i1 in dom X by A11,NAT_1:11,FINSEQ_3:25;
then
A13: X|i1 = (X|i)^<*X.i1*> & X.i1 = X/.i1 & Xr.i1 = Xr/.i1
by FINSEQ_5:10,PARTFUN1:def 6;
A14: Sum (X|i) = Sum (Xr|i) by MATRPROB:36;
dom (pF*sgmF) = dom X by A3,A9,FINSEQ_3:29;
then (pF*sgmF).i1 = (pF*sgmF)/.i1 by A12,PARTFUN1:def 6;
then reconsider o = O as Integer;
A15: Sum (Xr|i1)= Sum (X|i1) by MATRPROB:36
.= Sum (X|i) + Sum <*X/.i1*> by A13,RLVECT_1:41
.= (addreal).(Sum (X|i),X/.i1) by RLVECT_1:44
.= Sum (Xr|i) + (Xr/.i1) by A14,BINOP_2:def 9;
i1 in dom Y by A11,NAT_1:11,FINSEQ_3:25,A3,A5;
then
A16: Y|i1 = (Y|i)^<*Y.i1*> & Y.i1 = Y/.i1 & Yr.i1 = Yr/.i1
by FINSEQ_5:10,PARTFUN1:def 6;
A17:Sum (Y|i) = Sum (Yr|i) by MATRPROB:36;
A18: Sum (Yr|i1)= Sum (Y|i1) by MATRPROB:36
.= Sum (Y|i) + Sum <*Y/.i1*> by A16,RLVECT_1:41
.= (addreal).(Sum (Y|i),Y/.i1) by RLVECT_1:44
.= Sum (Yr|i) + (Yr/.i1) by A17,BINOP_2:def 9;
A19: Yr/.i1 = O * O2 by A3,A5,A6,A11,NAT_1:11;
reconsider OO1= O * O1, OO2= O * O2, PS = (p*sgm)/.i1 as Element of F_Real;
A20: (Xr/.i1) - (Yr/.i1) = OO1-OO2 by A4,A11,NAT_1:11,A19
.= PS*(eval((sgmF/.i1),@x)-eval((sgmF/.i1),@y)) by VECTSP_1:11
.= o * (o1-o2);
k divides o1-o2
proof
set b=sgmF/.i1, SG=SgmX(RelIncl n, support b);
consider H1 be FinSequence of FR such that
A21: len H1 = len SG & eval(b,xF) = Product H1 and
A22: for i being Element of NAT st 1 <= i & i <= len H1 holds
H1/.i = power(FR).((xF * SG)/.i, (b * SG)/.i) by POLYNOM2:def 2;
consider H2 be FinSequence of FR such that
A23: len H2 = len SG & eval(b,yF) = Product H2 and
A24: for i being Element of NAT st 1 <= i & i <= len H2 holds
H2/.i = power(FR).((yF * SG)/.i, (b * SG)/.i) by POLYNOM2:def 2;
defpred F[Nat] means $1 <= len SG implies Product (H1|$1) is integer &
Product (H2|$1) is integer &
for i1,i2 be Integer st i1= Product (H1|$1) & i2 =Product (H2|$1) holds
k divides i1-i2;
reconsider ZERO=0 as Nat;
A25: F[0]
proof
assume 0 <= len SG;
H2|ZERO = <*>(the carrier of F_Real);
then Product (H2|ZERO) = 1_ F_Real by GROUP_4:8
.=1;
hence thesis by INT_2:12;
end;
A26: for i be Nat st F[i] holds F[i+1]
proof
let i be Nat;
assume
A27: F[i];set i1=i+1,B=(b * SG)/.i1;
assume
A28: i1 <= len SG; then
reconsider p1 = Product (H1|i),p2 = Product (H2|i) as Integer
by A27,NAT_1:13;
A29: i1 in dom SG by NAT_1:11,A28,FINSEQ_3:25;
A30: len x = n & x = xF & y = yF by CARD_1:def 7,HILB10_2:def 1;
rng SG c= n = dom xF & n = dom yF by PARTFUN1:def 2,RELAT_1:def 19;
then i1 in dom (xF * SG) & i1 in dom (yF * SG) by A29,RELAT_1:27;
then
A31: (xF * SG)/.i1 = (xF * SG).i1 & (xF * SG).i1 = xF.(SG.i1) &
(yF * SG)/.i1 = (yF * SG).i1 & (yF * SG).i1 = yF.(SG.i1) &
SG.i1 in dom xF by PARTFUN1:def 6,FUNCT_1:11,12;
then
A32: SG.i1 in dom x by HILB10_2:def 1;
set sg = SG.i1;
reconsider xS = (xF * SG)/.i1,yS = (yF * SG)/.i1 as Integer by A31,A30;
reconsider xfSG = (xF * SG)/.i1,yfSG = (yF * SG)/.i1
as Element of F_Real;
H1/.i1 = power(FR).((xF * SG)/.i1,B) by NAT_1:11,A22,A28,A21;
then
A33: H1/.i1 = xS |^B by NIVEN:7;
H2/.i1 = power(FR).((yF * SG)/.i1,B) by NAT_1:11,A28,A23,A24;
then
A34: H2/.i1 = yS |^B by NIVEN:7;
i1 in dom H1 by A28,NAT_1:11,FINSEQ_3:25,A21;
then H1|i1 = (H1|i)^<*H1.i1*> & H1.i1 = H1/.i1
by FINSEQ_5:10,PARTFUN1:def 6; then
A35: Product (H1|i1) = Product (H1|i) * (H1/.i1) by GROUP_4:6
.= p1 * (xS |^B) by A33,BINOP_2:def 11;
i1 in dom H2 by A28,NAT_1:11,FINSEQ_3:25,A23;
then H2|i1 = (H2|i)^<*H2.i1*> & H2.i1 = H2/.i1
by FINSEQ_5:10,PARTFUN1:def 6;
then
A36: Product (H2|i1) = Product (H2|i) * (H2/.i1) by GROUP_4:6
.= p2 * (yS |^B) by A34,BINOP_2:def 11;
k divides (x.sg - y.sg) by A2,A31,A32;
then
A37: xS|^B,yS|^B are_congruent_mod k
by A1,GR_CY_3:34,INT_1:def 4,A31,A30;
k divides p1-p2 by NAT_1:13,A28,A27;
then p1,p2 are_congruent_mod k by INT_1:def 4;
hence thesis by A35,A36,INT_1:def 4,A37,INT_1:18;
end;
for i be Nat holds F[i] from NAT_1:sch 2(A25,A26);
then F[len SG];
hence thesis by A23,A21;
end;
then k divides o * (o1-o2) by INT_2:2;
then
A38: k divides -(o * (o1-o2)) by INT_2:10;
k divides S by A10,A11,NAT_1:13;
then k divides S --(o * (o1-o2)) by A38,INT_5:1;
hence thesis by A18,A15,A20;
end;
A39: P[i] from NAT_1:sch 2(A7,A8);
Sum (Xr|len X) = eval(pF,xF) & Sum (Yr|len X) = eval(pF,yF)
by A5,A3,MATRPROB:36;
hence thesis by A39;
end;
registration
let f be INT -valued Function;
cluster - f -> INT -valued;
coherence;
end;
scheme SCH1{P[object,object],f() -> XFinSequence-yielding XFinSequence}:
{f().i.j where i,j is Nat:P[i,j]} is finite
proof
deffunc F(object) = rng (f().$1);
consider p being XFinSequence such that
A1: len p = len f() and
A2: for k be Nat st k in len f() holds p.k=F(k) from AFINSQ_1:sch 2;
for X be set st X in rng p holds X is finite
proof
let X be set such that
A3: X in rng p;
consider x be object such that
A4: x in dom p & p.x = X by A3, FUNCT_1:def 3;
p.x = F(x) by A1,A2,A4;
hence thesis by A4;
end;
then
A5: union rng p is finite by FINSET_1:7;
{f().i.j where i,j is Nat:P[i,j]} c= {0}\/union rng p
proof
let x be object;
assume x in {f().i.j where i,j is Nat:P[i,j]};
then consider i,j be Nat such that
A6: x= f().i.j & P[i,j];
now assume not x in {0};
then
A7: x <>0 by TARSKI:def 1;
then j in dom (f().i) by A6,FUNCT_1:def 2;
then
A8: f().i.j in rng (f().i) by FUNCT_1:def 3;
f().i <> {} by A6,A7;
then i in dom f() by FUNCT_1:def 2;
then f().i in rng f() & p.i = F(i) & p.i in rng p
by A1,A2,FUNCT_1:def 3;
hence x in union rng p by A8,A6,TARSKI:def 4;
end;
hence x in {0}\/union rng p by XBOOLE_0:def 3;
end;
hence thesis by A5;
end;
theorem Th2:
m >= n > 0 implies
1+(m! * idseq n) is CR_Sequence
proof
assume
A1: m >= n > 0;
set h=1+(m! * idseq n);
deffunc F(Nat)=(m!)*$1+1;
A2: len h = n by CARD_1:def 7;
A3: for i st i in dom h holds h.i = F(i)
proof
let i such that
A4: i in dom h;
A5: dom h = dom (m! * idseq n) =dom idseq n by VALUED_1:def 2,def 5;
thus h.i = 1 + (m! * idseq n).i by A4,VALUED_1:def 2
.= 1+(m! * ((idseq n).i)) by A4,A5,VALUED_1:def 5
.= F(i) by A4,A5,FINSEQ_2:49;
end;
A6: h is positive-yielding
proof
let r be Real;
assume r in rng h;
then consider x be object such that
A7: x in dom h & h.x=r by FUNCT_1:def 3;
reconsider x as Nat by A7;
F(x)>0;
hence thesis by A7,A3;
end;
reconsider h as non empty positive-yielding INT -valued FinSequence
by A1,A6;
A8: for i,j being Nat st i in dom h & j in dom h & i < j holds
h.i, h.j are_coprime
proof
let i,j be Nat such that
A9: i in dom h & j in dom h & i < j;
reconsider ji=j-i as Nat by A9,NAT_1:21;
set G=h.i gcd h.j;
A10:h.i = F(i) & h.j = F(j) by A9,A3;
then
A11: G >=1 by NAT_1:14;
assume not h.i, h.j are_coprime;
then G > 1 by A11,XXREAL_0:1,INT_2:def 3;
then G is non trivial by NEWTON03:def 1;
then consider g be Prime such that
A12: g divides G by NEWTON03:29;
A13: ji <>0 by A9;
0<=i & j <=n by A9,A2,FINSEQ_3:25;
then ji <= n-0 by XREAL_1:13;
then
A14: ji divides m! by A13,NEWTON:41,A1,XXREAL_0:2;
A15: G divides F(i) & G divides F(j) by A10,INT_2:def 2;
then
A16: G divides F(j)-F(i) by INT_5:1;
A17: g divides F(i) by A15,A12,INT_2:9;
g divides m!*ji by A12,A16,INT_2:9;
then g divides m! or g divides j-i by INT_5:7;
then g divides m! by A14,INT_2:9;
then g divides i*(m!) by INT_2:2;
then g divides F(i)-i*(m!) by A17,INT_5:1;
then g=1 or g=-1 by INT_2:13;
hence thesis by INT_2:def 4;
end;
h is Chinese_Remainder
proof
let i,j be Nat such that A18: i in dom h & j in dom h & i <> j;
i >j or j >i by A18,XXREAL_0:1;
hence thesis by A18,A8;
end;
hence thesis;
end;
Lm1:for K,n being Nat ex Z being Nat st
Product (1+(K * idseq n)) = 1 + K*Z & (n>0 implies Z>0)
proof
let K be Nat;
defpred R[Nat] means ex Z be Nat st Product (1+(K * idseq $1)) = 1 + K*Z
& ($1 > 0 implies Z>0);
reconsider Z=0 as Nat;
Product (1+(K * idseq Z)) = 1+K*0 by RVSUM_1:94;
then
A1: R[0];
A2: for n be Nat st R[n] holds R[n+1]
proof
let n;
assume R[n];
then consider Z be Nat such that
A3: Product (1+(K * idseq n)) = 1 + K*Z & (n > 0 implies Z>0);
set n1=n+1;
A4: 1+K*<*n1*> = 1+<*K*n1*> by RVSUM_1:47
.= <*1+K*n1*> by BASEL_1:2;
idseq n1 = (idseq n)^<*n+1*> by FINSEQ_2:51;
then K*(idseq n1) = (K*(idseq n))^(K*<*n1*>) by NEWTON04:43;
then 1+ K*(idseq n1) = (1+K*(idseq n))^(1+K*<*n1*>) by BASEL_1:3;
then Product (1+(K*(idseq n1)))= (Product (1+(K*(idseq n)))) * (1+K*n1)
by A4,RVSUM_1:96;
then Product (1+(K*(idseq n1))) = 1 + K*(Z+n1+K*Z*n1) by A3;
hence thesis;
end;
for n be Nat holds R[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th12:
for p being Prime
for f being FinSequence of NAT st
f is positive-yielding & p divides Product f
ex i st i in dom f & p divides f.i
proof
let p be Prime;
defpred P[Nat] means for f be FinSequence of NAT st len f=$1
& f is positive-yielding & p divides Product f
ex i st i in dom f & p divides f.i;
A1: P[0]
proof
let f be FinSequence of NAT such that
A2: len f=0 & f is positive-yielding & p divides Product f;
f=<*>REAL by A2;
hence thesis by INT_2:def 4,A2,INT_2:27,RVSUM_1:94;
end;
A3: P[n] implies P[n+1]
proof set n1=n+1;
assume
A4: P[n];
let f be FinSequence of NAT such that
A5: len f=n1 & f is positive-yielding & p divides Product f;
f = (f|n)^ <*f.n1*> by A5,FINSEQ_3:55;
then Product f = Product (f|n) * (f.n1) by RVSUM_1:96;
then per cases by NEWTON:80,A5;
suppose
A6: p divides f.n1;
1<= n1 by NAT_1:11;
hence thesis by A6,A5,FINSEQ_3:25;
end;
suppose
A7: p divides Product (f|n);
len (f|n) = n by A5,FINSEQ_1:59,NAT_1:11;
then consider i such that
A8: i in dom (f|n) & p divides (f|n).i by A7,A4,A5;
i in dom f & (f|n).i = f.i by A8,FUNCT_1:47,RELAT_1:57;
hence thesis by A8;
end;
end;
let f be FinSequence of NAT;
P[n] from NAT_1:sch 2(A1,A3);
then P[len f];
hence thesis;
end;
begin :: Selected operations on polynomials
definition
let n be set, p be Series of n, F_Real;
func |. p .| -> Series of n,F_Real means :Def1:
for b being bag of n holds it.b = |. p.b .|;
existence
proof
defpred P[object,object] means $2 = |. p.$1 .|;
A1: for x being Element of Bags n
ex y being Element of F_Real st P[x,y]
proof
let x be Element of Bags n;
|. p.x .| in REAL by XREAL_0:def 1;
hence thesis;
end;
consider a be Function of Bags n,the carrier of F_Real such that
A2: for x be Element of Bags n holds P[x,a.x] from FUNCT_2:sch 3(A1);
take a;
let b being bag of n;
b in Bags n by PRE_POLY:def 12;
hence thesis by A2;
end;
uniqueness
proof
let a1,a2 be Series of n,F_Real such that
A3: for b being bag of n holds a1.b = |. p.b .| and
A4: for b being bag of n holds a2.b = |. p.b .|;
now let x be Element of Bags n;
thus a1.x = |. p.x .| by A3
.= a2.x by A4;
end;
hence a1=a2;
end;
end;
theorem Th3:
for n being set, p being Series of n, F_Real holds
Support p = Support |. p .|
proof
let n be set, p be Series of n, F_Real;
A1: dom p = Bags n = dom |. p .| by FUNCT_2:def 1;
thus Support p c= Support |. p .|
proof
let x be object;
assume x in Support p;
then x in dom p & p.x <> 0.F_Real &
|. p.x .| = |.p.| .x by Def1,POLYNOM1:def 3;
hence thesis by A1,POLYNOM1:def 3;
end;
let x be object;
assume x in Support |.p.|;
then x in dom |.p.| & |.p.| .x <> 0.F_Real &
|. p.x .| = |.p.| . x by Def1,POLYNOM1:def 3;
then x in dom p & p.x <> 0.F_Real by A1;
hence thesis by POLYNOM1:def 3;
end;
registration
let n be Ordinal;
let p be Polynomial of n, F_Real;
cluster |. p .| -> finite-Support;
coherence
proof
Support p = Support |. p .| by Th3;
hence thesis;
end;
end;
registration
let n be set;
let S be non empty ZeroStr;
let p be finite-Support Series of n, S;
cluster Support p -> finite;
coherence by POLYNOM1:def 5;
end;
definition
let n be Ordinal;
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p be Polynomial of n, L;
func sum_of_coefficients p -> Element of L equals
Sum (p * SgmX(BagOrder n,Support p));
coherence;
end;
definition
let n be Ordinal;
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p be Polynomial of n, L;
func degree p -> Nat means :Def3:
(ex s being bag of n st s in Support p &
it = degree s) &
for s1 being bag of n st s1 in Support p holds
degree s1 <= it
if p <> 0_(n,L) otherwise it = 0;
existence
proof
thus p <> 0_(n,L) implies ex d be Nat st
(ex s be bag of n st s in Support p &
d = degree s) &
for s1 be bag of n st s1 in Support p holds
d >= degree s1
proof
assume p <> 0_(n,L);
then p <> dom p --> 0.L;
then consider b be object such that
A1: b in dom p & p.b <> 0.L by FUNCOP_1:11;
reconsider b as bag of n by A1;
defpred P[object,object] means
for s be bag of n st s=$1 holds $2=degree s;
A2: for e being object st e in Support p ex u being object st P[e,u]
proof
let e be object;
assume e in Support p;
then reconsider e as bag of n;
take degree e;
thus thesis;
end;
consider D be Function such that
A3: dom D= Support p & for e being object st e in Support p holds P[e,D.e]
from CLASSES1:sch 1(A2);
b in Support p by A1, POLYNOM1:def 3;
then dom D<>{} by A3,XBOOLE_0:def 1;
then
A4: rng D <>{} by RELAT_1:42;
now let y be object;
assume y in rng D;
then consider x be object such that
A5: x in dom D & y=D.x by FUNCT_1:def 3;
reconsider x as bag of n by A5,A3;
y=degree x by A5,A3;
hence y is natural;
end;
then reconsider R=rng D as finite non empty natural-membered set
by A4,A3,FINSET_1:8,MEMBERED:def 6;
max R in R by XXREAL_2:def 8;
then consider s be object such that
A6: s in dom D & max R=D.s by FUNCT_1:def 3;
reconsider s as bag of n by A6,A3;
reconsider m=max R as Nat by A6;
take m;
s in Support p & m = degree s by A6,A3;
hence ex s be bag of n st s in Support p & m = degree s;
let s1 be bag of n;
assume s1 in Support p;
then D.s1 in R & D.s1 = degree s1 by FUNCT_1:def 3,A3;
hence thesis by XXREAL_2:def 8;
end;
thus thesis;
end;
uniqueness
proof
let d1,d2 be Nat;
now assume p <> 0_(n,L);
given s be bag of n such that
A7: s in Support p and
A8: d1 = degree s;
assume
A9: for s1 be bag of n st s1 in Support p holds d1 >= degree s1;
given S be bag of n such that
A10: S in Support p and
A11: d2 = degree S;
assume
A12: for s1 be bag of n st s1 in Support p holds
d2 >= degree s1;
d1 <= d2 & d2 <= d1 by A7,A8,A9,A10,A11,A12;
hence d1=d2 by XXREAL_0:1;
end;
hence thesis;
end;
consistency;
end;
theorem Th4:
for n being Ordinal, b being bag of n holds
degree b = Sum (b * SgmX(RelIncl n, support b))
proof
let n be Ordinal, b be bag of n;
set SG=SgmX(RelIncl n, support b);
A1: RelIncl n linearly_orders support b by PRE_POLY:82;
A2: rng SG = support b by A1,PRE_POLY:def 2;
then
A3: rng SG c= dom b = n by PRE_POLY:37,PARTFUN1:def 2;
consider f be FinSequence of NAT such that
A4: degree b = Sum f & f = b*canFS(support b) by UPROOTS:def 4;
rng canFS(support b) = support b by FUNCT_2:def 3;
then reconsider C= canFS(support b) as FinSequence of n by FINSEQ_1:def 4;
rng b c= NAT by VALUED_0:def 6;
then reconsider B=b as Function of n,REAL by A3,FUNCT_2:2;
A5: SG is one-to-one by PRE_POLY:10,82;
A6: rng SG =rng C by FUNCT_2:def 3,A2;
then for x being Element of n st x in rng SG \ rng C holds B.x = 0
by XBOOLE_0:def 1;
hence thesis by A4,ORDERS_5:8,A5,A6;
end;
theorem
for n being Ordinal,L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being Polynomial of n, L holds
degree p = 0 iff Support p c= {EmptyBag n}
proof
let n be Ordinal, L be add-associative right_zeroed right_complementable
non empty addLoopStr,
p be Polynomial of n, L;
thus degree p = 0 implies Support p c= {EmptyBag n}
proof
assume
A1: degree p = 0;
per cases;
suppose
A2: p= 0_(n,L);
let y be object;
assume
A3: y in Support p;
then p.y<>0.L by POLYNOM1:def 3;
hence thesis by A3,A2,POLYNOM1:22;
end;
suppose
A4: p <> 0_(n,L);
let y be object;
assume
A5: y in Support p;
then reconsider S=y as bag of n;
degree S= 0 by A1,A4,Def3,A5;
then S=EmptyBag n by UPROOTS:12;
hence y in {EmptyBag n} by TARSKI:def 1;
end;
end;
assume
A6: Support p c= {EmptyBag n};
assume
A7: degree p <>0;
then p <>0_(n,L) by Def3;
then consider s be bag of n such that
A8: s in Support p & degree p = degree s by Def3;
s=EmptyBag n by A6,A8,TARSKI:def 1;
hence thesis by A7,A8,UPROOTS:11;
end;
theorem Th6:
for n being Ordinal,L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being Polynomial of n, L, b being bag of n st b in Support p holds
degree p >= degree b
proof
let n be Ordinal, L be add-associative right_zeroed right_complementable
non empty addLoopStr,
p be Polynomial of n, L, b be bag of n;
assume
A1: b in Support p;
then Support p <>{} by XBOOLE_0:def 1;
then p <> 0_(n,L) by POLYNOM7:1;
hence thesis by A1,Def3;
end;
theorem Th7:
for n being Ordinal,p being Polynomial of n, F_Real st
|.p.| = 0_(n,F_Real) holds p = 0_(n,F_Real)
proof
let n be Ordinal,p be Polynomial of n, F_Real;
assume
A1: |.p.| = 0_(n,F_Real);
now let b be Element of Bags n;
|. p .b .| = |.p.| .b by Def1
.= 0 by A1;
hence p.b = 0_(n,F_Real).b;
end;
hence thesis;
end;
registration
let n be set;
reduce |. 0_(n,F_Real) .| to 0_(n,F_Real);
reducibility
proof
now let b be Element of Bags n;
thus |. 0_(n,F_Real) .|.b = |. 0_(n,F_Real).b .| by Def1
.= 0_(n,F_Real).b;
end;
hence thesis;
end;
end;
theorem
for n being Ordinal,p being Polynomial of n, F_Real holds
degree p = degree |. p .|
proof
let n be Ordinal,p be Polynomial of n, F_Real;
per cases;
suppose p = 0_(n,F_Real);
hence thesis;
end;
suppose
A1: p <> 0_(n,F_Real);
then consider s be bag of n such that
A2: s in Support p &
degree p = degree s by Def3;
A3: |.p.| <> 0_(n,F_Real) by A1,Th7;
then consider sM be bag of n such that
A4: sM in Support |.p.| &
degree |.p.| = degree sM by Def3;
Support |.p.| = Support p by Th3;
then degree p <= degree |.p.|<= degree p by A2,A1,Def3,A4,A3;
hence thesis by XXREAL_0:1;
end;
end;
theorem Th9:
for n being Ordinal,b being bag of n,r being Real st r >= 1
for x being Function of n, the carrier of F_Real st
for i being object st i in dom x holds |. x.i .| <= r holds
|. eval(b,x).| <= r |^ (degree b)
proof
let n be Ordinal,b be bag of n,r be Real such that
A1: r >= 1;
let x be Function of n, F_Real such that
A2: for i be object st i in dom x holds |. x.i .| <= r;
reconsider FR=F_Real as Field;
reconsider X=x as Function of n, the carrier of F_Real;
set sgm = SgmX(RelIncl n, support b),B=b*sgm;
A3: rng sgm c= n = dom b by PARTFUN1:def 2,RELAT_1:def 19;
then
A4: dom (b*sgm) = dom sgm by RELAT_1:27;
then
A5: len (b*sgm)=len sgm by FINSEQ_3:29;
dom x= n by FUNCT_2:def 1;
then
A6: dom (x*sgm) = dom sgm by A3,RELAT_1:27;
consider y be FinSequence of FR such that
A7: len y = len sgm & eval(b,x) = Product y and
A8: for i being Element of NAT st 1 <= i & i <= len y holds
y/.i = power(F_Real).((x * sgm)/.i,B/.i) by POLYNOM2:def 2;
rng B c= NAT by VALUED_0:def 6;
then reconsider B as FinSequence of NAT by FINSEQ_1:def 4;
reconsider Y=y as FinSequence of F_Real;
defpred P[Nat] means $1 <= len y implies Product (y|$1) is Real &
for P be Real st P=Product (y|$1) holds |. P .| <= r|^ Sum (B|$1);
reconsider ZERO=0 as Nat;
y|ZERO=<*>the carrier of F_Real;
then Product (y|ZERO) = 1_ F_Real by GROUP_4:8;
then
A9: P[0] by NEWTON:4;
A10: for i st P[i] holds P[i+1]
proof
let i be Nat;set i1=i+1;
assume that
A11: P[i] and
A12: i1 <= len y;
reconsider yi1= y/.i1 ,Pi=Product (y|i) as Real;
A13: |. Pi .| <= r|^ Sum (B|i) by A12,A11,NAT_1:13;
i1 in dom y by A12,NAT_1:11,FINSEQ_3:25;
then y|i1 = (y|i)^<*y.i1*> & y.i1 = y/.i1 by FINSEQ_5:10,PARTFUN1:def 6;
then
A14: Product (y|i1) = Product (y|i) * (y/.i1) by GROUP_4:6
.= Pi * yi1 by BINOP_2:def 11;
thus Product (y|i1) is Real;
let P be Real such that
A15: P=Product (y|i1);
A16: |. P .| = |.Pi.| * |.yi1.| by A15,A14,COMPLEX1:65;
i1 in dom B by A7,A12,A4,NAT_1:11,FINSEQ_3:25;
then
A17: B|i1 = (B|i)^<*B.i1*> & B.i1 = B/.i1 & B.i1 = b.(sgm.i1)
by FINSEQ_5:10,PARTFUN1:def 6,FUNCT_1:12;
then Sum (B|i1) = Sum(B|i) + (B/.i1) by RVSUM_1:74;
then
A18: r|^ Sum (B|i1) = (r |^ Sum (B|i)) * (r|^ (B/.i1)) by NEWTON:8;
A19: |.yi1.| <= r|^ (B/.i1)
proof
y/.i1 = power(F_Real).((x * sgm)/.i1,B/.i1) by A8,A12,NAT_1:11
.= ((x * sgm)/.i1) |^ (B/.i1) by NIVEN:7;
then
A20: |.yi1.| = |.(x * sgm)/.i1.| |^ (B/.i1) by TAYLOR_2:1;
i1 in dom (x * sgm) by A6,A7,A12,NAT_1:11,FINSEQ_3:25;
then
A21: (x * sgm)/.i1 = (x * sgm).i1 & (x * sgm).i1 = x.(sgm.i1)
& sgm.i1 in dom x & i1 in dom sgm by PARTFUN1:def 6,FUNCT_1:11,12;
RelIncl n linearly_orders support b by PRE_POLY:82;
then sgm.i1 in rng sgm = support b by A21,FUNCT_1:def 3,PRE_POLY:def 2;
then B/.i1 <>0 by A17,PRE_POLY:def 7;
then
A22: B/.i1 >=1+0 by NAT_1:13;
per cases by COMPLEX1:46;
suppose |. (x * sgm)/.i1.| >0;
hence thesis by A20,A2,A21,PREPOWER:9;
end;
suppose |.(x * sgm)/.i1.|=0;
then |.(x * sgm)/.i1.| |^ (B/.i1) = 0 by A22,NEWTON:11;
hence thesis by A1,A20;
end;
end;
A23: |.Pi.|>=0 by COMPLEX1:46;
|.yi1.|>=0 by COMPLEX1:46;
hence thesis by A13,A18,A23,A16,A19,XREAL_1:66;
end;
for i holds P[i] from NAT_1:sch 2(A9,A10);
then P[len y]; then
|. eval(b,x) .| <= r|^ Sum (B|len B) by A5,A7;
hence thesis by Th4;
end;
theorem Th10:
for n being Ordinal,p being Polynomial of n, F_Real,
r being Real st r >= 1
for x being Function of n, the carrier of F_Real st
for i being object st i in dom x holds |. x.i .| <= r
holds
|. eval(p,x).| <= (sum_of_coefficients |.p.|) * (r|^ degree p)
proof
let n be Ordinal,p be Polynomial of n, F_Real,r be Real such that
A1: r >= 1;
let x be Function of n, the carrier of F_Real such that
A2: for i be object st i in dom x holds |. x.i .| <= r;
reconsider FR=F_Real as Field;
reconsider pF=p,ApF = |.p.| as Polynomial of n, FR;
reconsider xF=x as Function of n, the carrier of FR;
set sgm=SgmX(BagOrder n,Support p);
set SgmF=SgmX(BagOrder n,Support pF);
reconsider H = ApF*SgmF as FinSequence of the carrier of F_Real;
A3: sum_of_coefficients |.p.| = Sum (ApF * SgmF) by Th3;
consider y be FinSequence of the carrier of FR such that
A4: len y = len SgmF & eval(p,x) = Sum y and
A5: for i be Element of NAT st 1 <= i & i <= len y holds
y/.i = (pF*SgmF)/.i * eval((SgmF/.i),xF) by POLYNOM2:def 4;
reconsider Y=y as FinSequence of REAL;
defpred P[Nat] means
$1 <= len y implies |. Sum (Y|$1) .| <= Sum (H|$1) * (r|^ degree p);
A6: P[0];
A7: len (ApF*SgmF) = len SgmF by CARD_1:def 7;
A8: for i be Nat st P[i] holds P[i+1]
proof
A9: BagOrder n linearly_orders Support p by POLYNOM2:18;
A10: rng sgm = Support p by A9,PRE_POLY:def 2;
A11: len (p*sgm) = len sgm by CARD_1:def 7;
let i be Nat;
assume
A12: P[i];set i1=i+1;
assume
A13: i1 <= len y;
then i1 in dom y by NAT_1:11,FINSEQ_3:25;
then
A14: y|i1 = (y|i)^<*y.i1*> & y.i1 = y/.i1 & Y.i1 = Y/.i1
by FINSEQ_5:10,PARTFUN1:def 6;
A15: Sum (y|i) = Sum (Y|i) by MATRPROB:36;
A16: Sum (Y|i1)= Sum (y|i1) by MATRPROB:36
.= Sum (y|i) + Sum <*y/.i1*> by A14,RLVECT_1:41
.= (addreal).(Sum (y|i),y/.i1)by RLVECT_1:44
.= Sum (Y|i) + (Y/.i1) by A15,BINOP_2:def 9;
i1 in dom (ApF*SgmF) by A4,A13,A7,NAT_1:11,FINSEQ_3:25;
then
A17: H|i1 = (H|i)^<*H.i1*> & H/.i1 = H.i1 & (ApF*SgmF)/.i1 = (ApF*SgmF).i1 &
(ApF*SgmF).i1=ApF .(SgmF.i1) by FINSEQ_5:10,PARTFUN1:def 6,FUNCT_1:12;
A18: Sum (H|i1) = Sum ((ApF*SgmF)|i1) by MATRPROB:36
.= Sum ((ApF*SgmF)|i) + Sum <*(ApF*SgmF)/.i1*> by A17, RLVECT_1:41
.= (the addF of FR).(Sum ((ApF*SgmF)|i),(ApF*SgmF)/.i1) by RLVECT_1:44
.= (addreal).(Sum (H|i),H/.i1) by MATRPROB:36
.= Sum (H|i) + H/.i1 by BINOP_2:def 9;
A19: |. (p * sgm)/.i1 .|>=0 & |. eval((sgm/.i1),x).|>=0 by COMPLEX1:46;
A20: (pF*SgmF)/.i1 * eval((SgmF/.i1),xF)
= (p * sgm)/.i1 * eval((sgm/.i1),x) by BINOP_2:def 11;
i1 in dom (p*sgm) by A4,A13,A11,NAT_1:11,FINSEQ_3:25;
then
A21: (p*sgm).i1 = (p*sgm)/.i1 & (p*sgm).i1 = p.(sgm.i1) & i1 in dom sgm
by PARTFUN1:def 6,FUNCT_1:11,12;
then
A22: sgm.i1 in rng sgm & sgm.i1 = sgm/.i1 by FUNCT_1:def 3,PARTFUN1:def 6;
A23: H/.i1 = (|.p.|).(sgm/.i1) by A17,A21,PARTFUN1:def 6
.= |. p.(sgm/.i1) .| by Def1;
A24: |. (p * sgm)/.i1 .| <= (H/.i1) by PARTFUN1:def 6,A21,A23;
A25: r|^ degree (sgm/.i1) <= r|^ degree p by A1,PREPOWER:93,Th6,A22,A10;
|. eval((sgm/.i1),x).| <= r|^ (degree (sgm/.i1)) by A1,A2,Th9;
then |. eval((sgm/.i1),x).| <= r|^ degree p by A25,XXREAL_0:2;
then |. (p * sgm)/.i1.| *|.eval((sgm/.i1),x).|<= (H/.i1)* (r|^ degree p)
by A24,A19,XREAL_1:66;
then
A26: |. (p * sgm)/.i1 * eval((sgm/.i1),x).| <= (H/.i1)* (r|^ degree p)
by COMPLEX1:65;
A27: |. Y/.i1.| <= (H/.i1) * (r|^ degree p) by A20,A26,A5,A13,NAT_1:11;
A28: |. Sum (Y|i).| + |.(Y/.i1).| >= |. Sum (Y|i) + (Y/.i1).| by COMPLEX1:56;
|. Sum (Y|i).| + |.(Y/.i1).| <=
Sum (H|i)* (r|^ degree p) + (H/.i1) * (r|^ degree p)
by A27,XREAL_1:7,A13,A12,NAT_1:13;
hence thesis by A16,A18,A28,XXREAL_0:2;
end;
A29:eval(p,x) = Sum (Y|len y) by A4,MATRPROB:36;
A30:Sum (H|len H) = sum_of_coefficients |.p.| by A3,MATRPROB:36;
for i be Nat holds P[i] from NAT_1:sch 2(A6,A8);
hence thesis by A30,A7,A4,A29;
end;
registration
let n be Ordinal,p be INT -valued Polynomial of n, F_Real;
cluster |.p.| -> natural-valued;
coherence
proof
now let y be object;
assume y in rng |.p.|;
then consider x be object such that
A1: x in dom |.p.| & |. p .| .x =y by FUNCT_1:def 3;
|. p .| .x = |. p.x.| by A1,Def1;
hence y in NAT by A1,ORDINAL1:def 12;
end;
hence thesis by VALUED_0:def 6,TARSKI:def 3;
end;
end;
registration
let n be Ordinal;
cluster natural-valued for Polynomial of n, F_Real;
existence
proof
take |. the INT -valued Polynomial of n, F_Real.|;
thus thesis;
end;
end;
registration
let O be Ordinal,p be natural-valued Polynomial of O, F_Real;
cluster sum_of_coefficients p -> natural;
coherence
proof
reconsider FR = F_Real as Field;
reconsider P=p as Polynomial of O,FR;
set S=SgmX(BagOrder O, Support P);
consider f be sequence of FR such that
A1: Sum (P*S) = f . (len (P*S)) & f . 0 = 0. FR and
A2: for j be Nat for v be Element of FR st
j < len (P*S) & v = (P*S) . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred P[Nat] means $1 <=len (P*S) implies f.$1 is natural;
A3: P[0] by A1;
A4: P[n] implies P[n+1]
proof
set n1=n+1;
assume
A5: P[n];
assume
A6: n1 <= len (P*S);
then
A7: n1 in dom (P*S) by NAT_1:11,FINSEQ_3:25;
A8: (P*S).n1 = (P*S)/.n1 by A7,PARTFUN1:def 6;
reconsider psn1=(P*S)/.n1 as Nat by A8;
reconsider fn=f.n as Nat by A5,A6,NAT_1:13;
(f.n) + (P*S)/.n1= fn + psn1 by BINOP_2:def 9;
hence thesis by A8,A2,A6,NAT_1:13;
end;
P[n] from NAT_1:sch 2(A3,A4);
hence thesis by A1;
end;
end;
begin :: Selected subsets of zero based finite sequences of NAT
:: as diophantine sets
scheme
SubsetDioph{n()->Nat, P[Nat,Nat,Nat,Nat],S() ->set}:
for i2,i3,i4 be Element of n() holds
{p where p is n()-element XFinSequence of NAT:
for i being Nat st i in S() holds P[p.i,p.i2,p.i3,p.i4]}
is diophantine Subset of n() -xtuples_of NAT
provided
A1: for i1,i2,i3,i4 being Element of n() holds
{p where p is n()-element XFinSequence of NAT: P[p.i1,p.i2,p.i3,p.i4]}
is diophantine Subset of n() -xtuples_of NAT
and
A2: S() c= Segm n()
proof
reconsider S=S() as finite set by A2;
defpred R[Nat] means for X be finite set st X c= S & card X = $1 holds
for i2,i3,i4 be Element of n() holds
{p where p is n()-element XFinSequence of NAT:
for i st i in X holds P[p.i,p.i2,p.i3,p.i4]}
is diophantine Subset of n() -xtuples_of NAT;
A3: R[0]
proof
let X be finite set such that
A4: X c= S & card X = 0;
let i2,i3,i4 be Element of n();
set PP={p where p is n()-element XFinSequence of NAT:
for i be Nat st i in X holds P[p.i,p.i2,p.i3,p.i4]};
A5: PP c= [#](n()-xtuples_of NAT)
proof
let x be object;assume x in PP;
then ex p be n()-element XFinSequence of NAT st x=p &
for i be Nat st i in X holds P[p.i,p.i2,p.i3,p.i4];
hence thesis by HILB10_2:def 5;
end;
[#](n()-xtuples_of NAT) c= PP
proof
let x be object;
assume x in [#](n()-xtuples_of NAT);
then reconsider p=x as n()-element XFinSequence of NAT;
X={} by A4;
then for i be Nat st i in X holds P[p.i,p.i2,p.i3,p.i4]
by XBOOLE_0:def 1;
hence thesis;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
A6: for m st R[m] holds R[m+1]
proof
let m such that
A7: R[m];
let X be finite set such that
A8: X c= S & card X = m+1;
let i2,i3,i4 be Element of n();
X is non empty by A8;
then consider x be object such that
A9: x in X by XBOOLE_0:def 1;
x in S by A8,A9;
then reconsider x as Element of n() by A2;
defpred Pn1[XFinSequence of NAT] means for i be Nat st i in X\{x} holds
P[$1.i,$1.i2,$1.i3,$1.i4];
card (X\{x}) = m by A8,A9,STIRL2_1:55;
then
A10: {p where p is n()-element XFinSequence of NAT: Pn1[p]}
is diophantine Subset of n() -xtuples_of NAT by A8,XBOOLE_1:1,A7;
defpred P1[XFinSequence of NAT] means P[$1.x,$1.i2,$1.i3,$1.i4];
A11: {p where p is n()-element XFinSequence of NAT: P1[p]}
is diophantine Subset of n() -xtuples_of NAT by A1;
defpred P[XFinSequence of NAT] means Pn1[$1]& P1[$1];
A12: {p where p is n()-element XFinSequence of NAT: Pn1[p] & P1[p]}
is diophantine Subset of n() -xtuples_of NAT
from HILB10_3:sch 3(A10,A11);
defpred Q[XFinSequence of NAT] means for i be Nat st i in X holds
P[$1.i,$1.i2,$1.i3,$1.i4];
A13: for p be n()-element XFinSequence of NAT holds P[p] iff Q[p]
proof
let p be n()-element XFinSequence of NAT;
thus P[p] implies Q[p]
proof
assume
A14: P[p];
let i be Nat such that
A15: i in X;
i=x or not i in {x} by TARSKI:def 1;
then i=x or i in X\{x} by A15,XBOOLE_0:def 5;
hence thesis by A14;
end;
assume Q[p];
hence thesis by A9,A2;
end;
{p where p is n()-element XFinSequence of NAT: P[p]} =
{p where p is n()-element XFinSequence of NAT: Q[p]}
from HILB10_3:sch 2(A13);
hence thesis by A12;
end;
for m holds R[m] from NAT_1:sch 2(A3,A6);
then R[card S];
hence thesis;
end;
theorem Th11:
for k,n1,n2,i,j,l,m,n,i1,i2,i3,i4 st n1+n2 <= n holds
{p: p.i1 >= k *
(((p.i2)^2+1)* (Product (1+((p/^n1)|n2) ))*(l*p.i3+m)) |^
(i*(p.i4)+j)}
is diophantine Subset of n -xtuples_of NAT
proof
let k,n1,n2,i,j,l,m;
deffunc F0(Nat,Nat,Nat) = $1|^$2;
A1:for n,i1,i2,i3,i4 holds {p:F0(p.i1,p.i2,p.i3)=p.i4}
is diophantine Subset of n -xtuples_of NAT by HILB10_3:24;
defpred P0[Nat,Nat,natural object,Nat,Nat,Nat] means 1* $1 >= k * $3 +0;
A2: for n,i1,i2,i3,i4,i5,i6 holds {p:P0[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT by HILB10_3:8;
A3: for i1,i2,i3,i4,i5 holds
{p: P0[p.i1,p.i2,F0(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A2,A1);
deffunc F1(Nat,Nat,Nat) = i*$1+j;
A4:for n,i1,i2,i3,i4 holds {p:F1(p.i1,p.i2,p.i3)=p.i4}
is diophantine Subset of n -xtuples_of NAT by HILB10_3:15;
defpred P1[Nat,Nat,natural object,Nat,Nat,Nat] means
$1 >= k * ($2|^$3);
A5: now let n,i1,i2,i3,i4,i5,i6;
defpred Q1[XFinSequence of NAT] means
P0[$1.i1,$1.i2,$1.i2|^$1.i3,$1.i4,$1.i5,$1.i6];
defpred Q2[XFinSequence of NAT] means
P1[$1.i1,$1.i2,$1.i3,$1.i4,$1.i5,$1.i6];
A6: for p holds Q1[p] iff Q2[p];
{p : Q1[p]} = {q :Q2[q]} from HILB10_3:sch 2(A6);
hence {p:P1[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT by A3;
end;
A7: for i1,i2,i3,i4,i5 holds
{p: P1[p.i1,p.i2,F1(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A5,A4);
deffunc F2(Nat,Nat,Nat) = 1* $1*$2;
A8:for n,i1,i2,i3,i4 holds {p: F2(p.i1,p.i2,p.i3)=p.i4}
is diophantine Subset of n -xtuples_of NAT by HILB10_4:26;
defpred P2[Nat,Nat,natural object,Nat,Nat,Nat] means
$1 >= k * ($3|^(i*$2+j));
A9:for n,i1,i3,i2,i4,i5,i6 holds {p:P2[p.i1,p.i3,p.i2,p.i4,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT by A7;
A10: for i1,i2,i3,i4,i5 holds
{p: P2[p.i1,p.i2,F2(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A9,A8);
defpred P3[Nat,Nat,natural object,Nat,Nat,Nat] means
$1 >= k * (($6*$3)|^(i*$2+j));
A11: now let n,i1,i2,i4,i5,i6,i3;
defpred Q1[XFinSequence of NAT] means
P2[$1.i1,$1.i2,1 * $1.i3 * $1.i4,$1.i4,$1.i5,$1.i5];
defpred Q2[XFinSequence of NAT] means
P3[$1.i1,$1.i2,$1.i4,$1.i5,$1.i6,$1.i3];
A12: for p holds Q1[p] iff Q2[p];
{p : Q1[p]} = {q :Q2[q]} from HILB10_3:sch 2(A12);
hence {p:P3[p.i1,p.i2,p.i4,p.i5,p.i6,p.i3]}
is diophantine Subset of n -xtuples_of NAT by A10;
end;
A13: for i1,i2,i3,i4,i5 holds
{p: P3[p.i1,p.i2,F2(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A11,A8);
deffunc F5(Nat,Nat,Nat) = 1* $1 +1;
A14:for n,i1,i2,i3,i4 holds {p: F5(p.i1,p.i2,p.i3)=p.i4}
is diophantine Subset of n -xtuples_of NAT by HILB10_3:15;
defpred P5[Nat,Nat,natural object,Nat,Nat,Nat] means
$1 >= k * (($3*$5*$6)|^(i*$2+j));
A15:now let n,i1,i2,i4,i3,i5,i6;
defpred Q1[XFinSequence of NAT] means
P3[$1.i1,$1.i2,1*$1.i4*$1.i5,$1.i4,$1.i5,$1.i6];
defpred Q2[XFinSequence of NAT] means
P5[$1.i1,$1.i2,$1.i4,$1.i3,$1.i5,$1.i6];
A16: for p holds Q1[p] iff Q2[p];
{p : Q1[p]} = {q :Q2[q]} from HILB10_3:sch 2(A16);
hence {p:P5[p.i1,p.i2,p.i4,p.i3,p.i5,p.i6]}
is diophantine Subset of n -xtuples_of NAT by A13;
end;
A17: for i1,i2,i3,i4,i5 holds
{p: P5[p.i1,p.i2,F5(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A15,A14);
deffunc G1(Nat,Nat,Nat) = l*$1+m;
A18:for n,i1,i2,i3,i4 holds {p:G1(p.i1,p.i2,p.i3)=p.i4}
is diophantine Subset of n -xtuples_of NAT by HILB10_3:15;
defpred R1[Nat,Nat,natural object,Nat,Nat,Nat] means
$1 >= k * (($3*$5*($6+1))|^(i*$2+j));
A19: now let n,i1,i2,i6,i4,i5,i3;
defpred Q1[XFinSequence of NAT] means
P5[$1.i1,$1.i2,1*$1.i3+1,$1.i4,$1.i5,$1.i6];
defpred Q2[XFinSequence of NAT] means
R1[$1.i1,$1.i2,$1.i6,$1.i4,$1.i5,$1.i3];
A20: for p holds Q1[p] iff Q2[p];
{p : Q1[p]} = {q :Q2[q]} from HILB10_3:sch 2(A20);
hence {p:R1[p.i1,p.i2,p.i6,p.i4,p.i5,p.i3]}
is diophantine Subset of n -xtuples_of NAT by A17;
end;
A21: for i1,i2,i3,i4,i5 holds
{p: R1[p.i1,p.i2,G1(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A19,A18);
defpred P6[Nat,Nat,natural object,Nat,Nat,Nat] means
$1 >= k * ((($3+1)*$5*(l*$6+m))|^(i*$2+j));
deffunc F6(Nat,Nat,Nat) = 1* $1*$1;
A22:for n,i1,i2,i3,i4 holds {p: F6(p.i1,p.i2,p.i3)=p.i4}
is diophantine Subset of n -xtuples_of NAT by HILB10_4:26;
A23: now let n,i1,i2,i6,i4,i5,i3;
defpred Q1[XFinSequence of NAT] means
R1[$1.i1,$1.i2,l*$1.i3+m,$1.i4,$1.i5,$1.i6];
defpred Q2[XFinSequence of NAT] means
P6[$1.i1,$1.i2,$1.i6,$1.i4,$1.i5,$1.i3];
A24: for p holds Q1[p] iff Q2[p];
{p : Q1[p]} = {q :Q2[q]} from HILB10_3:sch 2(A24);
hence {p:P6[p.i1,p.i2,p.i6,p.i4,p.i5,p.i3]}
is diophantine Subset of n -xtuples_of NAT by A21;
end;
A25: for n,i1,i2,i3,i4,i5 holds
{p: P6[p.i1,p.i2,F6(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 4(A23,A22);
let n,i1,i2,i3,i4 such that
A26: n1+n2 <= n;
set X=n+1;
A27: n < X by NAT_1:13;
then n in Segm X by NAT_1:44;
then reconsider N=n,I1=i1,I2=i2,I3=i3,I4=i4 as Element of X by HILB10_3:2;
defpred P7[XFinSequence of NAT] means
$1.I1 >= k * (((1*($1.I2)*($1.I2)+1) *
($1.N) * (l*$1.I3+m)) |^ (i*($1.I4)+j));
A28: {p where p is X-element XFinSequence of NAT:P7[p]}
is diophantine Subset of X -xtuples_of NAT by A25;
defpred Q7[XFinSequence of NAT] means $1.N = Product (1+(($1/^n1) | n2) );
A29: {p where p is X-element XFinSequence of NAT:Q7[p]}
is diophantine Subset of X -xtuples_of NAT by HILB10_4:39;
set PQ = {p where p is X-element XFinSequence of NAT:P7[p]&Q7[p]};
A30: PQ is diophantine Subset of X -xtuples_of NAT
from HILB10_3:sch 3(A28,A29);
set PQr = {p|n where p is X-element XFinSequence of NAT: p in PQ};
defpred S[XFinSequence of NAT] means $1.i1 >= k * ((($1.i2)^2+1) *
(Product (1+(($1/^n1) | n2) ))* (l*$1.i3+m)) |^ (i*($1.i4)+j);
set S={p: S[p]};
A31: PQr is diophantine Subset of n -xtuples_of NAT by HILB10_3:5,A27,A30;
A32: n1 <=n1+n2 by NAT_1:11;
A33: n-'n1 = n-n1 by A32,A26,XXREAL_0:2,XREAL_1:233;
A34: n2 <= n-n1 by A26,XREAL_1:19;
S c= n -xtuples_of NAT
proof
let y be object;
assume y in S;
then ex p st y=p & S[p];
hence thesis by HILB10_2:def 5;
end;
then reconsider S as Subset of n -xtuples_of NAT;
per cases;
suppose
n=0;
then S is diophantine Subset of n -xtuples_of NAT;
hence thesis;
end;
suppose
A35: n<>0;
A36: S c= PQr
proof
let y be object;assume y in S;
then consider p such that
A37: y=p & S[p];
A38: len p=n by CARD_1:def 7;
then
A39: len (p/^n1) >= n2 by A34,A33,AFINSQ_2:def 2;
reconsider P = Product(1+((p/^n1)|n2)) as Element of NAT
by ORDINAL1:def 12;
reconsider pP = p^<%P%> as X-element XFinSequence of NAT;
A40: pP|n = p by A38,AFINSQ_1:57;
A41: pP.N = P;
A42: pP.I1 = p.i1 & pP.I2 = p.i2 & pP.I3 = p.i3 & pP.I4=p.i4
by A35,A40,HILB10_3:4;
A43: (pP /^n1) | n2 = ((p /^n1) ^ <%P%>) |n2
by HILB10_4:10,A38,A32,A26,XXREAL_0:2
.= (p/^n1)|n2 by AFINSQ_1:58,A39;
P7[pP] & Q7[pP] by A43,A42,A37,SQUARE_1:def 1;
then pP in PQ;
hence thesis by A37,A40;
end;
PQr c= S
proof
let y be object;assume y in PQr;
then consider pP be X-element XFinSequence of NAT such that
A44: y=pP|n & pP in PQ;
A45: ex q be X-element XFinSequence of NAT st pP=q & P7[q] & Q7[q] by A44;
A46: len pP=X by CARD_1:def 7;
then
A47: len (pP|n) = n by A27,AFINSQ_1:54;
then reconsider p=pP|n as n-element XFinSequence of NAT by CARD_1:def 7;
A48: len (p/^n1) >= n2 by A34,A33,A47,AFINSQ_2:def 2;
set P = Product(1+((p/^n1) | n2));
A49: pP = p ^<%pP.n%> by A46,AFINSQ_1:56;
A50: (pP/^n1)|n2 = ((p/^n1)^<%pP.n%>)|n2
by A49,HILB10_4:10,A47,A32,A26,XXREAL_0:2
.= (p/^n1)|n2 by AFINSQ_1:58,A48;
A51: pP.I1 = p.i1 & pP.I2 = p.i2 & pP.I3 = p.i3 & pP.I4 = p.i4
by A35,HILB10_3:4;
(p.i2)*(p.i2) = (p.i2)^2 by SQUARE_1:def 1;
hence thesis by A44,A50,A51,A45;
end;
hence thesis by A31,A36,XBOOLE_0:def 10;
end;
end;
theorem Th13:
for P being INT -valued Polynomial of k,F_Real, a being Integer,
perm being Permutation of n,i1 st k <= n
holds
{p: for q be k-element XFinSequence of NAT st q = (p*perm)|k holds
a * (p.i1) = eval(P,@q)}
is diophantine Subset of n -xtuples_of NAT
proof
let P be INT -valued Polynomial of k,F_Real,a be Integer,
perm be Permutation of n,i1 such that
A1: k <= n;
defpred P[XFinSequence of NAT] means
for q be k-element XFinSequence of NAT st q = ($1*perm)|k holds
a*$1.i1 = eval(P,@q);
set A = {p: P[p]};
A c= n -xtuples_of NAT
proof
let y be object such that
A2: y in A;
ex p be n-element XFinSequence of NAT st y=p & P[p] by A2;
hence thesis by HILB10_2:def 5;
end;
then reconsider A as Subset of n -xtuples_of NAT;
per cases;
suppose n=0;
then A is diophantine;
hence thesis;
end;
suppose
A3: n<>0;
reconsider nk=n-k as Nat by A1,NAT_1:21;
consider Q be Polynomial of k+nk,F_Real such that
A4: rng Q c= rng P \/ {0.F_Real} and
A5: for x being Function of k, F_Real,
y being Function of (k+nk), F_Real st y|k=x
holds eval(P,x) = eval(Q,y) by HILB10_2:27;
A6: rng P c= INT by RELAT_1:def 19;
0.F_Real in INT by INT_1:def 1;
then {0.F_Real} c= INT by ZFMISC_1:31;
then rng P \/ {0.F_Real} c= INT by A6,XBOOLE_1:8;
then reconsider Q1=Q as INT-valued Polynomial of n,F_Real
by RELAT_1:def 19,A4,XBOOLE_1:1;
set T = Q1 permuted_by perm;
A7: rng T = rng Q1 by HILB10_2:26;
rng Q1 c= INT by RELAT_1:def 19;
then reconsider T1=T as INT-valued Polynomial of n,F_Real
by A7,RELAT_1:def 19;
reconsider FR=F_Real as Field;
reconsider ar=a as Element of FR by XREAL_0:def 1;
reconsider Ar=ar as Element of F_Real;
reconsider t = T as Polynomial of n,FR;
T1=t; then reconsider TI = t - ar*1_1(i1,FR)
as INT-valued Polynomial of n+0,F_Real;
for s be object holds s in A iff ex x being n-element XFinSequence of NAT,
y being 0-element XFinSequence of NAT st s = x & eval(TI,@(x^y)) = 0
proof
let s be object;
thus s in A implies ex x being n-element XFinSequence of NAT,
y being 0-element XFinSequence of NAT st
s = x & eval(TI,@(x^y)) = 0
proof
assume s in A;
then consider p be n-element XFinSequence of NAT such that
A8: s=p & P[p];
reconsider E = <%>NAT as 0-element XFinSequence of NAT;
take p,E;
thus s = p by A8;
reconsider pE = @(p^E) as Function of n, FR;
A9: eval(1_1(i1,FR),pE) = (pE.i1) by A3,HILB10_3:1
.= p.i1 by HILB10_2:def 1;
reconsider Eval=eval(1_1(i1,FR),pE) as Element of F_Real;
A10: eval(ar*1_1(i1,FR),pE) =Ar*Eval by POLYNOM7:29
.= a * (p.i1) by A9;
A11: dom perm = n & rng perm = n & len p = n
by FUNCT_2:52,def 3,CARD_1:def 7;
then dom (p*perm) = n by RELAT_1:27;
then reconsider pp= p*perm as XFinSequence by AFINSQ_1:5;
A12: len pp = n by A11,RELAT_1:27;
reconsider PP = pp as n-element XFinSequence of NAT
by A12,CARD_1:def 7;
len (PP|k) = k by A12,A1,AFINSQ_1:54;
then reconsider PPk = PP|k as k-element XFinSequence of NAT
by CARD_1:def 7;
(@PP)|k = PP|k by HILB10_2:def 1;
then
A13: (@PP)|k = @PPk by HILB10_2:def 1;
PP*perm" = p * (perm*perm") by RELAT_1:36
.= p*(id n) by FUNCT_2:61
.= p by A11,RELAT_1:51;
then
A14: PP*perm" = @p by HILB10_2:def 1;
A15: eval(T,@p) = eval(T,@PP*(perm")) by A14,HILB10_2:def 1
.= eval(Q1,@PP) by HILB10_2:25
.= eval(P,@PPk) by A5,A13
.= a* (p.i1) by A8;
thus eval(TI,@(p^E)) = eval(t,pE) - eval(ar*1_1(i1,FR),pE)
by POLYNOM2:24
.= 0.FR by A10,A15,RLVECT_1:5
.= 0;
end;
given x be n-element XFinSequence of NAT,
y be 0-element XFinSequence of NAT such that
A16: s = x & eval(TI,@(x^y)) = 0;
reconsider xy = @(x^y) as Function of n, FR;
A17: eval(1_1(i1,FR),xy) = (xy.i1) by A3,HILB10_3:1
.= x.i1 by HILB10_2:def 1;
reconsider Eval=eval(1_1(i1,FR),xy) as Element of F_Real;
A18: eval(ar*1_1(i1,FR),xy) =Ar*Eval by POLYNOM7:29
.= a * (x.i1) by A17;
A19: dom perm = n & rng perm = n & len x = n
by FUNCT_2:52,def 3,CARD_1:def 7;
then dom (x*perm) = n by RELAT_1:27;
then reconsider xp= x*perm as XFinSequence by AFINSQ_1:5;
A20: len xp = n by A19,RELAT_1:27;
reconsider XP = xp as n-element XFinSequence of NAT by A20,CARD_1:def 7;
len (XP|k) = k by A20,A1,AFINSQ_1:54;
then reconsider XPk = XP|k as k-element XFinSequence of NAT
by CARD_1:def 7;
(@XP)|k = XP|k by HILB10_2:def 1;
then
A21: (@XP)|k = @XPk by HILB10_2:def 1;
XP*perm" = x * (perm*perm") by RELAT_1:36
.= x*(id n) by FUNCT_2:61
.= x by A19,RELAT_1:51;
then
A22: XP*perm" = @x by HILB10_2:def 1;
A23: eval(T,@x) = eval(T,@XP*(perm")) by A22,HILB10_2:def 1
.= eval(Q1,@XP) by HILB10_2:25
.= eval(P,@XPk) by A5,A21;
A24: eval(t,xy) - eval(ar*1_1(i1,FR),xy) = 0.FR by POLYNOM2:24,A16;
P[x] by A24,A18,A23,VECTSP_1:19;
hence thesis by A16;
end;
hence thesis by HILB10_2:def 6;
end;
end;
theorem Th14:
for P being INT -valued Polynomial of k+1,F_Real,a being Integer,
n,i1,i2 st k+1 <= n & k in i2
holds
{p: for q being k+1-element XFinSequence of NAT st q = <%p.i2%>^(p|k) holds
a* p.i1 = eval(P,@q)}
is diophantine Subset of n -xtuples_of NAT
proof
let P be INT -valued Polynomial of k+1,F_Real,a be Integer,n,i1,i2 such that
A1: k+1 <= n & k in i2;
set k1=k+1;
dom id k = k;
then reconsider Idk=id k as XFinSequence by AFINSQ_1:5;
A2: len Idk=k;
A3: rng id k=Segm k;
reconsider Idk as k-element XFinSequence of NAT by A2,CARD_1:def 7;
reconsider nk=n-k1 as Nat by A1,NAT_1:21;
set f = <%i2%>^Idk;
A4: rng <%i2%>={i2} by AFINSQ_1:33;
{i2} misses k by A1,ZFMISC_1:50;
then rng <%i2%> misses rng Idk by AFINSQ_1:33;
then
A6: f is one-to-one by CARD_FIN:52;
set R=rng f;
A7: len f = k1 by CARD_1:def 7;
A8: card dom f = k1 by CARD_1:def 7;
A: k < n by A1,NAT_1:13;
then
A9: Segm k c= Segm n by NAT_1:39;
i2 in n by A1,SUBSET_1:def 1;
then {i2} c= n by ZFMISC_1:31;
then k \/ {i2} c= n by A9,XBOOLE_1:8;
then
A10: R c= n by AFINSQ_1:26,A4,A3;
then card (n\R) = (card n) - card R by CARD_2:44;
then
A11: card (n\R) = nk by A8,A6,CARD_1:70;
A12: Segm k1 c= Segm n by A1,NAT_1:39;
then
card (n\k1) = card n-card k1 by CARD_2:44
.= nk;
then consider g be Function such that
A13: g is one-to-one & dom g =n\k1 & rng g = n\R
by A11,CARD_1:5,WELLORD2:def 4;
A14: rng f misses rng g & dom f misses dom g by A7,A13,XBOOLE_1:79;
then
A15: f +* g is one-to-one by A6,A13,FUNCT_4:92;
A16: dom (f+*g) = k1 \/ (n\k1) by A7,A13,FUNCT_4:def 1
.= k1\/n by XBOOLE_1:39
.= n by A12,XBOOLE_1:12;
A17: rng (f+*g) = R \/ rng g by A14,NECKLACE:6
.= n \/ R by A13,XBOOLE_1:39
.= n by A10,XBOOLE_1:12;
then reconsider fg = f+*g as Function of n,n by A16,FUNCT_2:2;
card n = card n;
then fg is onto by A15,FINSEQ_4:63;
then reconsider fg as Permutation of n by A15;
defpred Q[XFinSequence of NAT] means
for q be k1-element XFinSequence of NAT st q = ($1*fg)|k1 holds
a*($1.i1) = eval(P,@q);
defpred R[XFinSequence of NAT] means
for q be k+1-element XFinSequence of NAT st q = <%$1.i2%>^($1|k) holds
a*($1.i1) = eval(P,@q);
A18:for p be n-element XFinSequence of NAT holds Q[p] iff R[p]
proof
let p be n-element XFinSequence of NAT;
A19: len p = n by CARD_1:def 7;
then dom (p*fg)= n by A17,A16,RELAT_1:27;
then reconsider pfg=p*fg as XFinSequence by AFINSQ_1:5;
set I =<%p.i2%>;
len pfg = n by A19,A17,A16,RELAT_1:27;
then
A20: len (pfg|k1) = k1 by A1,AFINSQ_1:54;
A21: len (p|k)=k & len I=1 by AFINSQ_1:11,A,A19,CARD_1:def 7; then
A22: len(I^(p|k)) = k1 by AFINSQ_1:17;
for i st i in dom (I^(p|k)) holds (I^(p|k)).i = (pfg|k1).i
proof
let i; assume
A23: i in dom (I^(p|k)); then
A24: i in dom pfg & i in k1 & (pfg|k1).i = pfg.i
by RELAT_1:57,FUNCT_1:47,A20,A22;
then
A25: pfg.i = p.(fg.i) & not i in dom g
by FUNCT_1:12,A13,XBOOLE_1:79,XBOOLE_0:3;
then
A26: fg.i = f.i by FUNCT_4:11;
A27: len <%i2%> = 1 by CARD_1:def 7;
per cases by A23,AFINSQ_1:20;
suppose
A28: i in dom I;
then i < len I =1 by AFINSQ_1:66,CARD_1:def 7;
then i=0 & i in dom <%i2%> by CARD_1:def 7,A28,NAT_1:14;
then f.i = <%i2%>.i =i2 & I.i = p.i2 by AFINSQ_1:def 3;
hence thesis by A24,A25,A26,A28,AFINSQ_1:def 3;
end;
suppose ex j st j in dom (p|k) & i=len I+j;
then consider j such that
A29: j in dom (p|k) & i=len I+j;
A30: (I^(p|k)).i = (p|k).j = p.j by A29,AFINSQ_1:def 3,FUNCT_1:47;
j in dom Idk by A,A19,A29,AFINSQ_1:11;
then f.i = Idk .j =j by A21,A27,A29,AFINSQ_1:def 3,FUNCT_1:17;
hence thesis by A30,A24,A25,FUNCT_4:11;
end;
end;
hence thesis by A20,A22,AFINSQ_1:8;
end;
{p: Q[p]} = {q: R[q]} from HILB10_3:sch 2(A18);
hence thesis by Th13,A1;
end;
theorem Th15:
for P being INT -valued Polynomial of k+1,F_Real,n,i1,i2 st
k+1 <= n & k in i1
holds
{p: for q be 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
proof
set k1=k+1;
let P be INT -valued Polynomial of k1,F_Real,n,i1,i2 such that
A1: k+1 <= n & k in i1;
reconsider FR=F_Real as Field;
set X=n+1;
A2: n < X & k < n by A1,NAT_1:13;
then n in Segm X by NAT_1:44;
then reconsider N=n,I1=i1,I2=i2 as Element of X by HILB10_3:2;
defpred P[XFinSequence of NAT] means
1 * $1.N,0*$1.I1 are_congruent_mod 1*$1.I2;
A3: {p where p is X-element XFinSequence of NAT:P[p]}
is diophantine Subset of X -xtuples_of NAT by HILB10_3:21;
defpred QP[XFinSequence of NAT] means
for q be k1-element XFinSequence of NAT st q = <%$1.I1%>^($1|k) holds
1 * $1.N = eval(P,@q);
defpred QM[XFinSequence of NAT] means
for q be k1-element XFinSequence of NAT st q = <%$1.I1%>^($1|k) holds
(-1) * $1.N = eval(P,@q);
defpred Q[XFinSequence of NAT] means QP[$1] or QM[$1];
A4: k1 < X & k in I1 by A1,NAT_1:13;
then
A5: {p where p is X-element XFinSequence of NAT:QP[p]}
is diophantine Subset of X -xtuples_of NAT by Th14;
A6: {p where p is X-element XFinSequence of NAT:QM[p]}
is diophantine Subset of X -xtuples_of NAT by Th14,A4;
{p where p is X-element XFinSequence of NAT:QP[p]or QM[p]}
is diophantine Subset of X -xtuples_of NAT from HILB10_3:sch 1(A5,A6);
then
A7: {p where p is X-element XFinSequence of NAT:Q[p]}
is diophantine Subset of X -xtuples_of NAT;
set PQ = {p where p is X-element XFinSequence of NAT:P[p]&Q[p]};
A8: PQ is diophantine Subset of X -xtuples_of NAT from HILB10_3:sch 3(A3,A7);
set PQr = {p|n where p is X-element XFinSequence of NAT: p in PQ};
defpred S[XFinSequence of NAT] means
for q be k1-element XFinSequence of NAT st q = <%$1.i1%>^($1|k) holds
eval(P,@q),0 are_congruent_mod $1.i2;
set S={p: S[p]};
A9: PQr 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: S c= PQr
proof
let y be object;
assume y in S;
then consider p such that
A12: y=p & S[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))=k1 by A13,AFINSQ_1:17;
then reconsider pi1pk=<%p.i1%>^(p|k) as k1-element XFinSequence of NAT
by CARD_1:def 7;
reconsider E=|.eval(P,@pi1pk).| as Element of NAT;
reconsider pE = p^<%E%> as X-element XFinSequence of NAT;
A14: pE|n = p by A13,AFINSQ_1:57;
A15: pE.N = E;
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 per cases by ABSVALUE:1;
suppose E=eval(P,@pi1pk);
hence QP[pE] or QM[pE] by A17,A16;
end;
suppose E=-eval(P,@pi1pk);
hence QP[pE] or QM[pE] by A10,A14,RELAT_1:74,A16;
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,15;
1 * pE.N,0*pE.I1 are_congruent_mod 1*pE.I2
proof
per cases by ABSVALUE:1;
suppose E=eval(P,@pi1pk);
hence thesis by A12,A16;
end;
suppose E=-eval(P,@pi1pk);
then pE.i2 divides (E - -0) by A19;
hence thesis by INT_2:15;
end;
end;
then pE in PQ by A18;
hence thesis by A12,A14;
end;
PQr c= S
proof
let y be object;
assume y in PQr;
then consider pP be X-element XFinSequence of NAT such that
A20: y=pP|n & pP in PQ;
A21: ex q be X-element XFinSequence of NAT st q=pP & P[q]&Q[q] by A20;
len pP=X 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))=k1 by A23,AFINSQ_1:17;
then reconsider pi1pk=<%p.i1%>^(p|k) as k1-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;
then per cases;
suppose pP.N = eval(P,@pi1pk);
hence thesis by A21,A1,HILB10_3:4;
end;
suppose
A26: pP.N = - eval(P,@pi1pk);
p.i2 divides (-(pP.N) -0) by A25,INT_2:10,A24;
hence thesis by A26,INT_2:15;
end;
end;
then S[p];
hence thesis by A20;
end;
hence thesis by A9,A11,XBOOLE_0:def 10;
end;
begin :: Bounded quantifier theorem and its variant
theorem Th16:
for p being INT -valued Polynomial of 2+n+k,F_Real,
X being n-element XFinSequence of NAT,
x be Element of NAT holds
( for z being Element of NAT st z <= x
ex y being k-element XFinSequence of NAT st
eval(p,@(<%z,x%>^X^y)) = 0) iff
ex Y being k-element XFinSequence of NAT,
Z,e,K being Element of NAT st
K > x & K >= (sum_of_coefficients |.p.|)*
((x^2+1) * (Product (1+X))*e)|^degree p &
(for i being Nat st i in k holds Y.i > e) &
e > x &
1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1)))&
eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) &
(for i being Nat st i in k holds
Product ((Y.i + 1)+(-idseq e)),0 are_congruent_mod (1+(Z+1)*(K!)))
proof
let p be INT -valued Polynomial of 2+n+k,F_Real,
X be n-element XFinSequence of NAT,
x be Element of NAT;
set x1=x+1;
thus ( for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
eval(p,@(<%z,x%>^X^y)) = 0) implies
ex Y be k-element XFinSequence of NAT,
Z,e,K be Element of NAT st
K>x & K >= (sum_of_coefficients |.p.|)*
((x^2+1) * (Product (1+X))*e)|^(degree p) &
(for i be Nat st i in k holds Y.i > e) &
e > x &
1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1)))&
eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) &
(for i be Nat st i in k holds
Product ((Y.i+1)+(-idseq e)),0 are_congruent_mod (1+(Z+1)*(K!)))
proof
assume
A1: for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
eval(p,@(<%z,x%>^X^y)) = 0;
defpred P[object,object] means
$1 in NAT & $2 is k-element XFinSequence of NAT &
for z be Element of NAT,y be k-element XFinSequence of NAT st
z=$1 & y=$2 holds eval(p,@(<%z,x%>^X^y)) = 0;
A2: for i be Nat st i in x1 ex g be object st P[i,g]
proof
let i be Nat; assume i in x1;
then
A3: i in Segm (x1);
reconsider z = i as Element of NAT by ORDINAL1:def 12;
i <x1 by A3,NAT_1:44;
then i<= x by NAT_1:13;
then consider y be k-element XFinSequence of NAT such that
A4: eval(p,@(<%z,x%>^X^y)) = 0 by A1;
take y;
thus thesis by A4,ORDINAL1:def 12;
end;
consider YY be XFinSequence such that
A5: dom YY = x1 & for i be Nat st i in x+1 holds P[i,YY.i]
from AFINSQ_1:sch 1(A2);
YY is XFinSequence-yielding by A5;
then reconsider YY as XFinSequence-yielding XFinSequence;
defpred Q[object,object] means not contradiction;
set M = {YY.i.j where i,j is Nat : Q[i,j]};
A6: M is finite from SCH1;
A7: M is natural-membered
proof
let x be object;
assume x in M;
then consider i,j be Nat such that
A8: x= YY.i.j & Q[i,j];
per cases;
suppose
i in dom YY;
then P[i,YY.i] by A5;
hence x is natural by A8;
end;
suppose not i in dom YY;
then YY.i= {} by FUNCT_1:def 2;
hence thesis by A8;
end;
end;
then reconsider Mx=M\/{x,1} as non empty natural-membered finite set by A6;
set e = 1+max Mx;
set K = x1+e+(sum_of_coefficients |.p.|)*
((x^2+1) * (Product (1+X))*e)|^(degree p);
set h=1+(K! * idseq x1);
A9: len h = x1 by CARD_1:def 7;
A10: for i st i in dom h holds h.i = (K!)*i +1
proof
let i such that
A11: i in dom h;
A12: dom h = dom (K! * idseq x1) =dom idseq x1 by VALUED_1:def 2,def 5;
thus h.i = 1 + (K! * idseq x1).i by A11,VALUED_1:def 2
.= 1+(K! * ((idseq x1).i)) by A11,A12,VALUED_1:def 5
.= (K!)*i +1 by A11,A12,FINSEQ_2:49;
end;
A13: x1+e <=K & x1 <= x1+e & e <= x1+e by NAT_1:11;
then
A14: K >= x1 > 0 by XXREAL_0:2;
then reconsider h as CR_Sequence by Th2;
rng h c= NAT by VALUED_0:def 6;
then
A15: h is FinSequence of NAT by FINSEQ_1:def 4;
0+1<=x1 by NAT_1:13;
then h.1 divides Product h & h.1 = K!*1+1
by A10,A15,INT_4:32,A9,FINSEQ_3:25;
then h.1 <= Product h & h.1 > K! by INT_2:27,NAT_1:13;
then K <= K! & K! < Product h by XXREAL_0:2,NEWTON:38;
then e <= K & K < Product h by A13,XXREAL_0:2;
then
A16: e < Product h by XXREAL_0:2;
defpred Q[object,object] means
$1 in NAT & $2 in NAT & for i,z be Nat st i = $1 & z= $2 holds
e < z & for j,F being Nat st j in x1 & F = YY.j.i
holds z,F are_congruent_mod h.(j+1);
A17: for i be Nat st i in k ex Y be object st Q[i,Y]
proof
let i be Nat such that i in k;
deffunc H(Nat) = YY.($1-'1).i;
consider X be FinSequence such that
A18: len X = x1 & for k be Nat st k in dom X holds X.k=H(k)
from FINSEQ_1:sch 2;
rng X c= NAT
proof
let y be object;
assume y in rng X;
then consider x be object such that
A19: x in dom X & X.x=y by FUNCT_1:def 3;
reconsider x as Nat by A19;
X.x = YY.(x-'1).i by A18,A19;
then X.x in M;
then X.x is natural by A7;
hence thesis by A19;
end;
then reconsider X as FinSequence of NAT by FINSEQ_1:def 4;
consider z be Integer such that
A20: 0 <= z & z < Product h and
A21: for i being Nat st i in dom X holds z,X.i are_congruent_mod h.i
by INT_6:41,A18,A9;
take Y= z+Product h;
thus i in NAT & Y in NAT by A20,ORDINAL1:def 12;
let I,Z be Nat such that
A22: I=i & Z=Y;
Y >= Product h by A20,NAT_1:11;
hence e < Z by A22,A16,XXREAL_0:2;
let j,F be Nat such that
A23: j in x1 & F = YY.j.I;
x1= Segm x1;
then j < x1 by A23,NAT_1:44;
then
A24: 1 <= j+1 <= x1 by NAT_1:11,13;
then
A25: z,X.(j+1) are_congruent_mod h.(j+1) by A21,A18,FINSEQ_3:25;
j+1 in dom h by A24,A9,FINSEQ_3:25;
then h.(j+1) divides (Product h)-0 by A15,INT_4:32;
then Product h,0 are_congruent_mod h.(j+1) by INT_1:def 4;
then
A26: Y,(X.(j+1)) +0 are_congruent_mod h.(j+1) by A25,INT_1:16;
X.(j+1) =YY.(j+1-'1).i by A18,A24,FINSEQ_3:25;
hence thesis by A26,A23,A22,NAT_D:34;
end;
consider YC be XFinSequence such that
A27: dom YC = k & for i be Nat st i in k holds Q[i,YC.i]
from AFINSQ_1:sch 1(A17);
rng YC c= NAT
proof
let y be object;
assume y in rng YC;
then ex x be object st x in dom YC & YC.x=y by FUNCT_1:def 3;
hence thesis by A27;
end;
then reconsider YC as k-element XFinSequence of NAT
by A27,CARD_1:def 7,RELAT_1:def 19;
consider Z be Nat such that
A29: Product (1+(K! * idseq x1)) = 1 + (K!)*Z & (x1>0 implies Z>0) by Lm1;
reconsider Z1=Z-1 as Element of NAT by NAT_1:20,A29;
reconsider e,K as Element of NAT by ORDINAL1:def 12;
take YC,Z1,e,K;
thus K > x & K >= (sum_of_coefficients |.p.|)*
((x^2+1) * (Product (1+X))*e)|^(degree p) by NAT_1:11,A14,NAT_1:13;
thus for i be Nat st i in k holds YC.i > e by A27;
x in {x,1} by TARSKI:def 2;
then x in Mx by XBOOLE_0:def 3;
then x <= max Mx by XXREAL_2:def 8;
hence x < e by NAT_1:13;
thus 1+(Z1+1)*(K!) = Product (1+(K! * idseq x1)) by A29;
A30: for b,c be Element of NAT st b in dom h & c in dom h & b<>c
holds h.b gcd h.c =1 by INT_2:def 3,INT_6:def 2;
reconsider E=eval(p,@(<%Z1,x%>^X^YC)) as Integer;
A31: for b be Element of NAT st b in dom h holds h.b divides E
proof
let b be Element of NAT such that
A32: b in dom h;
A33: h.b = (K!)*b+1 by A32,A10;
1<= b <= x1 by A9,A32,FINSEQ_3:25;
then reconsider b1=b-1 as Element of NAT by NAT_1:21;
b1+1<=x1 by A9,A32,FINSEQ_3:25;
then b1 < Segm x1 by NAT_1:13;
then
A34: b1 in x1 by NAT_1:44;
then reconsider YYb=YY.b1 as k-element XFinSequence of NAT by A5;
A35: eval(p,@(<%b1,x%>^X^YYb)) = 0 by A34,A5;
for i st i in 2+n+k holds h.b divides ((<%Z1,x%>^X^YC).i -
(<%b1,x%>^X^YYb).i)
proof
let i;
A36: len (<%Z1,x%>^X^YC) = 2+n+k by CARD_1:def 7;
A37: len <%Z1,x%> = 1+1 & len <%b1,x%> = 1+1 by CARD_1:def 7;
A38: len (<%Z1,x%>^X) = len <%Z1,x%> + len X &
len (<%b1,x%>^X) = len <%b1,x%> + len X by AFINSQ_1:17;
A39: len YC = k = len YYb by CARD_1:def 7;
assume i in 2+n+k;
then per cases by A36,AFINSQ_1:20;
suppose
A40: i in dom (<%Z1,x%>^X);
then
A41: (<%Z1,x%>^X^YC).i = (<%Z1,x%>^X).i & (<%b1,x%>^X^YYb).i
= (<%b1,x%>^X).i by A38,A37,AFINSQ_1:def 3;
per cases by A40,AFINSQ_1:20;
suppose
A42: i in dom <%Z1,x%>;
then
A43: i in Segm 2 by CARD_1:def 7;
A44: (<%Z1,x%>^X).i = <%Z1,x%>.i & (<%b1,x%>^X).i = <%b1,x%>.i
by A42,A37,AFINSQ_1:def 3;
per cases by A43,NAT_1:23,NAT_1:44;
suppose i=0;
then
A45: (<%Z1,x%>^X^YC).i = Z1 & (<%b1,x%>^X^YYb).i = b1
by A40,A38,A37,AFINSQ_1:def 3,A44;
A46: (K!+1) gcd (K!)= ((b1 * (K!))+(K!+1)) gcd (K!) by EULER_1:8;
A47: (K!+1) gcd K! = 1 by INT_2:def 3,PEPIN:1;
A48: h.b divides Product h by A15,A32,INT_4:32;
A49: (Z1-b1)*(K!) = Product (1+(K! * idseq x1)) - h.b by A29,A33;
h.b divides (Z1-b1)*(K!) by A48,A49,INT_5:1;
hence thesis by A45,A47,A46,INT_2:def 3,A33,INT_2:25;
end;
suppose i=1;
hence thesis by INT_2:12,A41,A44;
end;
end;
suppose ex j st j in dom X & i = len (<%Z1,x%>)+j;
then consider j such that
A50: j in dom X & i = 2+j by A37;
(<%Z1,x%>^X).i = X.j&(<%b1,x%>^X).i = X.j
by A37,A50,AFINSQ_1:def 3;
hence thesis by A41,INT_2:12;
end;
end;
suppose ex j st j in dom YC & i = len (<%Z1,x%>^X)+j;
then consider j such that
A51: j in dom YC & i = len (<%Z1,x%>^X)+j;
A52: (<%Z1,x%>^X^YC).i = YC.j by A51,AFINSQ_1:def 3;
A53: (<%b1,x%>^X^YYb).i = YYb.j by A39,A37,A38,A51,AFINSQ_1:def 3;
reconsider J=j, YCj=YC.j as Element of NAT by A51;
YC.j,YYb.j are_congruent_mod h.(b1+1) by A34,A27,A51;
hence thesis by A52,A53,INT_1:def 4;
end;
end;
then h.b divides E-0 by A32,A35,Th1;
hence thesis;
end;
Product h divides E
proof
per cases;
suppose E>=0;
hence thesis by A30,A31,A15,INT_4:38;
end;
suppose E <0;
then reconsider mE=-E as Element of NAT by INT_1:3;
for b be Element of NAT st b in dom h holds h.b divides mE
by A31,INT_2:10;
hence thesis by INT_2:10,A30,A15,INT_4:38;
end;
end;
then Product h divides E-0;
hence eval(p,@(<%Z1,x%>^X^YC)),0 are_congruent_mod (1+(Z1+1)*(K!))
by A29,INT_1:def 4;
let i be Nat such that
A54: i in k;
set YCe = ((YC.i+1)+(-idseq e));
A55: dom YCe = dom (-idseq e) =dom idseq e by VALUED_1:def 2,8;
A56: for j st j in dom YCe holds YCe.j = (YC.i+1) - j
proof
let j such that
A57: j in dom YCe;
thus YCe.j = (YC.i+1) + (- idseq e).j by A57,VALUED_1:def 2
.= (YC.i+1) +-((idseq e).j) by VALUED_1:8
.= (YC.i+1) +- j by A57,A55,FINSEQ_2:49
.= (YC.i+1) - j;
end;
rng YCe c= NAT
proof
let b be Integer;
assume b in rng YCe;
then consider a be object such that
A58: a in dom YCe & YCe.a=b by FUNCT_1:def 3;
reconsider a as Nat by A58;
A59: YCe.a = (YC.i+1)-a by A56,A58;
YC.i > e>= a by A27,A54,A55,A58,FINSEQ_1:1;
then YC.i > a by XXREAL_0:2;
then YC.i +1 > a by NAT_1:13;
then (YC.i+1)-a is Nat by NAT_1:21;
hence thesis by A58,A59,ORDINAL1:def 12;
end;
then
reconsider YCe as FinSequence of NAT by FINSEQ_1:def 4;
reconsider PP=Product YCe as Element of NAT;
A60: for b be Element of NAT st b in dom h holds h.b divides PP
proof
let b be Element of NAT such that
A61: b in dom h;
1<= b <= x1 by A61,A9,FINSEQ_3:25;
then reconsider b1=b-1 as Nat;
A62: YY.b1.i in M;
then reconsider YYb1i= YY.b1.i as Nat by A7;
b1+1<=x1 by A61,A9,FINSEQ_3:25;
then b1 < Segm x1 by NAT_1:13;
then b1 in x1 by NAT_1:44;
then YC.i,YYb1i are_congruent_mod h.(b1+1) by A27,A54;
then
A63: h.b divides (YC.i - YYb1i) by INT_1:def 4;
YYb1i in Mx by A62,XBOOLE_0:def 3;
then YYb1i <= max Mx by XXREAL_2:def 8;
then 0+1 <= YYb1i+1 <= e by XREAL_1:7;
then
A64: YYb1i+1 in dom YCe by A55;
then
A65: YCe.(YYb1i+1) = (YC.i+1) - (YYb1i+1) by A56;
YCe.(YYb1i+1) divides PP by A64,INT_4:32;
hence thesis by A65,A63,INT_2:9;
end;
Product h divides PP-0 by A30,A60,A15,INT_4:38;
hence Product ((YC.i+1)+(-idseq e)),0 are_congruent_mod (1+(Z1+1)*(K!))
by INT_1:def 4,A29;
end;
given Y be k-element XFinSequence of NAT,Z,e,K be Element of NAT such that
A66: K> x & K >= (sum_of_coefficients |.p.|)* ((x^2+1) *
(Product (1+X))*e)|^(degree p) and
A67: for i be Nat st i in k holds Y.i > e and
A68: e > x & 1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1)))&
eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) and
A69: for i be Nat st i in k holds
Product ((Y.i+1)+(-idseq e)),0 are_congruent_mod (1+(Z+1)*(K!));
let z be Element of NAT such that
A70:z <= x;
set z1=z+1,K1 = K!,ZZ = 1+(z+1)*K1;
A71: ZZ >1 +0 by XREAL_1:8;
consider prim be Element of NAT such that
A72: prim divides ZZ & prim <= ZZ & prim is prime by A71, NAT_4:13;
deffunc P(object) = Y.$1 mod prim;
consider Yz be XFinSequence such that
A73: len Yz = k & for i be Nat st i in k holds Yz.i = P(i)
from AFINSQ_1:sch 2;
rng Yz c= NAT
proof
let y be object;
assume y in rng Yz;
then consider x be object such that
A74: x in dom Yz & Yz.x=y by FUNCT_1:def 3;
y = P(x) by A73,A74;
hence thesis by ORDINAL1:def 12;
end;
then reconsider Yz as k-element XFinSequence of NAT
by A73,RELAT_1:def 19,CARD_1:def 7;
1<=z1 <=x1 by A70,NAT_1:11,XREAL_1:6;
then
A75: z1 in Seg (x1);
K>=x1 by A66,NAT_1:13;
then
reconsider h=1+(K1 * idseq (x1)) as CR_Sequence by Th2;
rng h c= NAT by VALUED_0:def 6;
then
A76: h is FinSequence of NAT by FINSEQ_1:def 4;
A77: dom h = dom (K1 * idseq (x+1)) =dom idseq (x+1) by VALUED_1:def 2,def 5;
A78: h.z1 = 1 + (K1 * idseq (x+1)).z1 by A75,A77,VALUED_1:def 2
.= 1+K1 * ((idseq (x+1)).z1) by A75,A77,VALUED_1:def 5
.=ZZ by A75,FINSEQ_2:49;
ZZ divides (1+(Z+1)*K1) by A78,A68,A76,INT_4:32,A75,A77;
then
A79: prim divides (1+(Z+1)*K1) by A72,INT_2:9;
1+(Z+1)*K1 divides eval(p,@(<%Z,x%>^X^Y)) - 0 by A68,INT_1:def 4;
then
A80: prim divides eval(p,@(<%Z,x%>^X^Y)) by A79,INT_2:9;
reconsider E1=eval(p,@(<%Z,x%>^X^Y)) as Integer;
A81: K < prim
proof
assume K >= prim;
then prim divides (Z+1)*K1 by INT_2:2,A72,NEWTON:41;
then prim divides 1 by A79,INT_2:1;
then prim = 1 by INT_2:13;
hence thesis by A72,INT_2:def 4;
end;
A82:len <%z,x%> = 2 = len <%Z,x%> by CARD_1:def 7;
A83:len (<%z,x%>^X) = 2+n = len (<%Z,x%>^X) by CARD_1:def 7;
A84:len Y = k = len Yz by CARD_1:def 7;
A85:len (<%z,x%>^X^Yz) = 2+k+n by CARD_1:def 7;
for i st i in 2+k+n holds prim divides ((<%Z,x%>^X^Y).i - (<%z,x%>^X^Yz).i)
proof
let i such that
A86: i in 2+k+n;
per cases by A86,A85,AFINSQ_1:20;
suppose
A87: i in dom (<%z,x%>^X);
then
A88: ((<%z,x%>^X^Yz)).i = (<%z,x%>^X).i & ((<%Z,x%>^X^Y)).i = (<%Z,x%>^X).i
by A83,AFINSQ_1:def 3;
per cases by A87,AFINSQ_1:20;
suppose i in dom <%z,x%>;
then
A89: i in Segm 2 & (<%z,x%>^X).i = <%z,x%>.i &
(<%Z,x%>^X).i = <%Z,x%>.i by A82,AFINSQ_1:def 3;
per cases by A89,NAT_1:23,NAT_1:44;
suppose i=0;
then
A90: (<%Z,x%>^X^Y).i =Z & (<%z,x%>^X^Yz).i = z
by A87,A83,AFINSQ_1:def 3,A89;
A91: K1,prim are_coprime
proof
assume not K1,prim are_coprime;
then
A92: K1 gcd prim <>1 by INT_2:def 3;
K1 gcd prim divides prim by INT_2:def 2;
then K1 gcd prim = prim by A92,A72,INT_2:def 4;
then prim divides K1 by INT_2:def 2;
hence thesis by A81,NAT_4:19,A72;
end;
prim divides (1+(Z+1)*K1) - (1+(z+1)*K1) by A79,A72,INT_5:1;
then prim divides (Z-z)*K1;
hence thesis by A90,A91,INT_2:25;
end;
suppose i=1;
hence thesis by A88,A89,INT_2:12;
end;
end;
suppose ex j be Nat st j in dom X & i = len (<%z,x%>)+j;
then consider j such that
A93: j in dom X & i = len (<%z,x%>)+j;
(<%z,x%>^X).i = X.j & (<%Z,x%>^X).i = X.j by A82,A93,AFINSQ_1:def 3;
hence thesis by INT_2:12,A88;
end;
end;
suppose ex j be Nat st j in dom Yz & i = len (<%z,x%>^X)+j;
then consider j such that
A94: j in dom Yz & i = len (<%z,x%>^X)+j;
A95: (<%Z,x%>^X^Y).i =Y.j & (<%z,x%>^X^Yz).i = Yz.j
by A83,A84,A94,AFINSQ_1:def 3;
Yz.j = Y.j mod prim by A73,A94;
hence thesis by A95,A72,PEPIN:8;
end;
end;
then prim divides E1 - eval(p,@(<%z,x%>^X^Yz)) by A72,Th1;
then prim divides eval(p,@(<%z,x%>^X^Yz)) by INT_5:2,A80;
then |.prim.| divides |.eval(p,@(<%z,x%>^X^Yz)).| by INT_2:16;
then consider m be Nat such that
A96: |.eval(p,@(<%z,x%>^X^Yz)).| =prim *m by NAT_D:def 3;
A97: x^2=x*x by SQUARE_1:def 1;
for i be object st i in dom @(<%z,x%>^X^Yz) holds |.(@(<%z,x%>^X^Yz)).i.|
<= (x^2+1) * (Product (1+X))*e
proof
let i be object;assume i in dom @(<%z,x%>^X^Yz);
then
A98: i in dom (<%z,x%>^X^Yz) & (<%z,x%>^X^Yz) = @(<%z,x%>^X^Yz)
by HILB10_2:def 1;
reconsider i as Nat by A98;
per cases by A98,AFINSQ_1:20;
suppose
A99: i in dom (<%z,x%>^X);
then
A100: (@(<%z,x%>^X^Yz)).i = (<%z,x%>^X).i by A98,AFINSQ_1:def 3;
per cases by A99,AFINSQ_1:20;
suppose i in dom <%z,x%>;
then
A101: i in Segm 2 & (<%z,x%>^X).i = <%z,x%>.i
by CARD_1:def 7,AFINSQ_1:def 3;
A102: (Product (1+X))*e>= 1 by A68,NAT_1:14;
x^2 >= x*1 by NAT_1:14,A97, XREAL_1:64;
then x^2+1 >= x+0 by XREAL_1:7;
then
A103: (x^2+1)* ((Product (1+X))*e)>= x*1 by A102,XREAL_1:66;
per cases by A101,NAT_1:23,NAT_1:44;
suppose i=0;
hence thesis by A103,A70,XXREAL_0:2,A100,A101;
end;
suppose i=1;
hence thesis by A103,A100,A101;
end;
end;
suppose ex j be Nat st j in dom X & i = len (<%z,x%>)+j;
then consider j such that
A104: j in dom X & i = len (<%z,x%>)+j;
A105: dom (1+X) = dom X by VALUED_1:def 2;
then
A106: (1+X).j <= Product (1+X) by A104,HILB10_4:11;
(1+X).j = 1+(X.j) by A104,A105,VALUED_1:def 2;
then
A107: X.j <= Product (1+X) by A106,NAT_1:13;
e*(x^2+1)>=1 by NAT_1:14,A68;
then 1*(X.j) <= e*(x^2+1) * Product (1+X) by A107,XREAL_1:66;
hence thesis by A104,AFINSQ_1:def 3,A100;
end;
end;
suppose ex j be Nat st j in dom Yz & i = len (<%z,x%>^X)+j;
then consider j such that
A108: j in dom Yz & i = len (<%z,x%>^X)+j;
set YE = (Y.j+1)+(-idseq e);
A109: (<%z,x%>^X^Yz).i = Yz.j by A108,AFINSQ_1:def 3;
A110: Yz.j = Y.j mod prim by A108,A73;
A111: 1+(Z+1)*K1 divides Product YE - 0 by INT_1:def 4,A69,A108,A73;
A112: len YE = len idseq e = e by CARD_1:def 7;
A113: for w be Nat st w in dom YE holds
((Y.j+1)+(-idseq e)).w = (Y.j) +1-w
proof
let w be Nat;
assume
A114: w in dom YE;
then w in dom (-idseq e) by VALUED_1:def 2;
then w in dom idseq e by VALUED_1:8;
then (idseq e).w=w by FINSEQ_2:49;
then (- idseq e).w = -w by VALUED_1:8;
then YE.w = (Y.j) +1+ -w by A114,VALUED_1:def 2;
hence thesis;
end;
A115: now let a be Nat;
assume
A116: a in dom YE;
1<= a <= e by A116,A112,FINSEQ_3:25;
then reconsider a1=a-1 as Nat;
a1+1 <=e by A116,A112,FINSEQ_3:25;
then a1 < e by NAT_1:13;
then
A117: e-a1 >0 by XREAL_1:50;
YE.a = Y.j +1-a by A116,A113;
then YE.a+a1 > e by A67,A84,A108;
hence YE.a >0 by A117,XREAL_1:19;
end;
now let r be object;
assume r in rng YE;
then consider a be object such that
A118: a in dom YE & YE.a = r by FUNCT_1:def 3;
reconsider a as Nat by A118;
YE.a >0 by A115,A118;
hence r in NAT by A118,INT_1:3;
end;
then
A119: YE is FinSequence of NAT by FINSEQ_1:def 4,TARSKI:def 3;
YE is positive-yielding
proof
let r be Real;
assume r in rng YE;
then consider a be object such that
A120: a in dom YE & YE.a = r by FUNCT_1:def 3;
thus thesis by A115,A120;
end;
then consider w be Nat such that
A121: w in dom YE & prim divides YE.w by A111,A79,INT_2:9,Th12,A72,A119;
A122: 1 <= w <= e by A112,A121,FINSEQ_3:25;
then reconsider w1=w-1 as Nat;
prim divides Y.j+ 1 -w by A121,A113;
then prim divides Y.j -w1;
then Yz.j = w1 mod prim by A110,INT_4:23,A72;
then Yz.j < w1+1 by NAT_1:13,NEWTON05:11;
then
A123: Yz.j < e by A122,XXREAL_0:2;
(x^2+1) * Product (1+X)>=1 by NAT_1:14;
then 1*(Yz.j) <= e*((x^2+1) * Product (1+X)) by A123,XREAL_1:66;
hence thesis by A109,A98;
end;
end;
then |.eval(p,@(<%z,x%>^X^Yz)).| <= (sum_of_coefficients |.p.|) *
(((x^2+1) * (Product (1+X))*e)|^ degree p) by A68,NAT_1:14,Th10;
then |.eval(p,@(<%z,x%>^X^Yz)).| <= K by A66,XXREAL_0:2;
then prim*m < prim*1 by A96,A81,XXREAL_0:2;
then m < 1 by XREAL_1:66;
then m=0 by NAT_1:14;
then eval(p,@(<%z,x%>^X^Yz))=0 by A96;
hence thesis;
end;
theorem Th17:
for p being INT -valued Polynomial of 2+n+k,F_Real,
X being n-element XFinSequence of NAT,
x being Element of NAT holds
( for z being Element of NAT st z <= x
ex y being k-element XFinSequence of NAT st
(for i st i in k holds y.i <= x)&
eval(p,@(<%z,x%>^X^y)) = 0)
iff
ex Y being k-element XFinSequence of NAT,
Z,K being Element of NAT st
K > x & K >= (sum_of_coefficients |.p.|)*
((x^2+1) * (Product (1+X)))|^degree p &
(for i being Nat st i in k holds Y.i > (x+1)) &
1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1)))&
eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) &
(for i being Nat st i in k holds
Product ((Y.i + 1)+(-idseq (x+1))),
0 are_congruent_mod (1+(Z+1)*(K!)))
proof
let p be INT -valued Polynomial of 2+n+k,F_Real,
X be n-element XFinSequence of NAT,
x be Element of NAT;
set x1=x+1;
thus (for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
(for i st i in k holds y.i <= x) &
eval(p,@(<%z,x%>^X^y)) = 0) implies
ex Y be k-element XFinSequence of NAT,Z,K be Element of NAT st
K>x & K >= (sum_of_coefficients |.p.|)*
((x^2+1) * (Product (1+X)))|^(degree p) &
(for i be Nat st i in k holds Y.i > x1) &
1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1)))&
eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) &
(for i be Nat st i in k holds
Product ((Y.i+1)+(-idseq x1)),0 are_congruent_mod (1+(Z+1)*(K!)))
proof
assume
A1: for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
(for i st i in k holds y.i <= x)&
eval(p,@(<%z,x%>^X^y)) = 0;
defpred P[object,object] means
$1 in NAT & $2 is k-element XFinSequence of NAT &
for z be Element of NAT,y be k-element XFinSequence of NAT st
z=$1 & y=$2 holds (for i st i in k holds y.i <= x)&
eval(p,@(<%z,x%>^X^y)) = 0;
A2: for i be Nat st i in x1 ex g be object st P[i,g]
proof
let i be Nat;
assume i in x1;
then
A3: i in Segm (x1);
reconsider z = i as Element of NAT by ORDINAL1:def 12;
i <x1 by A3,NAT_1:44;
then i<= x by NAT_1:13;then
consider y be k-element XFinSequence of NAT such that
A4: for i st i in k holds y.i <= x and
A5: eval(p,@(<%z,x%>^X^y)) = 0 by A1;
take y;
thus thesis by A4,A5,ORDINAL1:def 12;
end;
consider YY be XFinSequence such that
A6: dom YY = x1 & for i be Nat st i in x+1 holds P[i,YY.i]
from AFINSQ_1:sch 1(A2);
YY is XFinSequence-yielding by A6;
then reconsider YY as XFinSequence-yielding XFinSequence;
defpred Q[object,object] means not contradiction;
set M = {YY.i.j where i,j is Nat : Q[i,j]};
A7: M is finite from SCH1;
A8: M is natural-membered
proof
let x be object;
assume x in M;
then consider i,j be Nat such that
A9: x= YY.i.j & Q[i,j];
per cases;
suppose
i in dom YY;
then P[i,YY.i] by A6;
hence x is natural by A9;
end;
suppose not i in dom YY;
then YY.i= {} by FUNCT_1:def 2;
hence thesis by A9;
end;
end;
then reconsider Mx = M\/{x,1} as non empty natural-membered finite set
by A7;
set K = x1+ (sum_of_coefficients |.p.|)*
((x^2+1)*(Product (1+X)))|^(degree p);
set h=1+(K! * idseq x1);
A10: len h = x1 by CARD_1:def 7;
A11: for i st i in dom h holds h.i = (K!)*i +1
proof
let i such that
A12: i in dom h;
A13: dom h = dom (K! * idseq x1) =dom idseq x1 by VALUED_1:def 2,def 5;
thus h.i = 1 + (K! * idseq x1).i by A12,VALUED_1:def 2
.= 1+(K! * ((idseq x1).i)) by A12,A13,VALUED_1:def 5
.= (K!)*i +1 by A12,A13,FINSEQ_2:49;
end;
A14:K >= x1 > 0 by NAT_1:11;
reconsider h as CR_Sequence by NAT_1:11,Th2;
rng h c= NAT by VALUED_0:def 6;
then
A15: h is FinSequence of NAT by FINSEQ_1:def 4;
0+1<=x1 by NAT_1:13;
then h.1 divides Product h & h.1 = K!*1+1
by A11,A15,INT_4:32,A10,FINSEQ_3:25;
then h.1 <= Product h & h.1 > K! by INT_2:27,NAT_1:13;
then K <= K! & K! < Product h by XXREAL_0:2,NEWTON:38;
then x1 <= K & K < Product h by NAT_1:11,XXREAL_0:2;
then
A16: x1 < Product h by XXREAL_0:2;
defpred Q[object,object] means
$1 in NAT & $2 in NAT & for i,z be Nat st i = $1 & z= $2 holds x1 < z &
for j,F being Nat st j in x1 & F = YY.j.i
holds z,F are_congruent_mod h.(j+1);
A17: for i be Nat st i in k ex Y be object st Q[i,Y]
proof
let i be Nat such that i in k;
deffunc H(Nat) = YY.($1-'1).i;
consider X be FinSequence such that
A18: len X = x1 & for k be Nat st k in dom X holds X.k=H(k)
from FINSEQ_1:sch 2;
rng X c= NAT
proof
let y be object;
assume y in rng X;
then consider x be object such that
A19: x in dom X & X.x=y by FUNCT_1:def 3;
reconsider x as Nat by A19;
X.x = YY.(x-'1).i by A18,A19;
then X.x in M;
then X.x is natural by A8;
hence thesis by A19;
end;
then reconsider X as FinSequence of NAT by FINSEQ_1:def 4;
consider z be Integer such that
A20: 0 <= z & z < Product h and
A21: for i being Nat st i in dom X holds z,X.i are_congruent_mod h.i
by INT_6:41,A18,A10;
take Y= z+Product h;
thus i in NAT & Y in NAT by A20,ORDINAL1:def 12;
let I,Z be Nat such that
A22: I=i & Z=Y;
Y >= Product h by A20,NAT_1:11;
hence x1 < Z by A22,A16,XXREAL_0:2;
let j,F be Nat such that
A23: j in x1 & F = YY.j.I;
x1= Segm x1;
then j < x1 by A23,NAT_1:44;
then
A24: 1 <= j+1 <= x1 by NAT_1:11,13;
then
A25: z,X.(j+1) are_congruent_mod h.(j+1) by A21,A18,FINSEQ_3:25;
j+1 in dom h by A24,A10,FINSEQ_3:25;
then h.(j+1) divides (Product h)-0 by A15,INT_4:32;
then Product h,0 are_congruent_mod h.(j+1) by INT_1:def 4;
then
A26: Y,(X.(j+1)) +0 are_congruent_mod h.(j+1) by A25,INT_1:16;
X.(j+1) =YY.(j+1-'1).i by A18,A24,FINSEQ_3:25;
hence thesis by A26,A23,A22,NAT_D:34;
end;
consider YC be XFinSequence such that
A27: dom YC = k & for i be Nat st i in k holds Q[i,YC.i]
from AFINSQ_1:sch 1(A17);
rng YC c= NAT
proof
let y be object;
assume y in rng YC;
then ex x be object st x in dom YC & YC.x=y by FUNCT_1:def 3;
hence thesis by A27;
end;
then reconsider YC as k-element XFinSequence of NAT
by A27,CARD_1:def 7,RELAT_1:def 19;
consider Z be Nat such that
A29: Product (1+(K! * idseq x1)) = 1 + (K!)*Z & (x1>0 implies Z>0) by Lm1;
reconsider Z1=Z-1 as Element of NAT by NAT_1:20,A29;
reconsider K as Element of NAT by ORDINAL1:def 12;
take YC,Z1,K;
thus K > x & K >= (sum_of_coefficients |.p.|)*
((x^2+1) * (Product (1+X)))|^(degree p) by NAT_1:11,13,A14;
thus for i be Nat st i in k holds YC.i > x1 by A27;
thus 1+(Z1+1)*(K!) = Product (1+(K! * idseq x1)) by A29;
A30: for b,c be Element of NAT st b in dom h & c in dom h & b<>c
holds h.b gcd h.c =1 by INT_2:def 3,INT_6:def 2;
reconsider E=eval(p,@(<%Z1,x%>^X^YC)) as Integer;
A31: for b be Element of NAT st b in dom h holds h.b divides E
proof
let b be Element of NAT such that
A32: b in dom h;
A33: h.b = (K!)*b+1 by A32,A11;
1<= b <= x1 by A10,A32,FINSEQ_3:25;
then reconsider b1=b-1 as Element of NAT by NAT_1:21;
b1+1<=x1 by A10,A32,FINSEQ_3:25;
then b1 < Segm x1 by NAT_1:13;
then
A34: b1 in x1 by NAT_1:44;
then reconsider YYb=YY.b1 as k-element XFinSequence of NAT by A6;
A35: eval(p,@(<%b1,x%>^X^YYb)) = 0 by A34,A6;
for i st i in 2+n+k holds
h.b divides ((<%Z1,x%>^X^YC).i - (<%b1,x%>^X^YYb).i)
proof
let i;
A36: len (<%Z1,x%>^X^YC) = 2+n+k by CARD_1:def 7;
A37: len <%Z1,x%> = 1+1 & len <%b1,x%> = 1+1 by CARD_1:def 7;
A38: len (<%Z1,x%>^X) = len <%Z1,x%> + len X &
len (<%b1,x%>^X) = len <%b1,x%> + len X by AFINSQ_1:17;
A39: len YC = k = len YYb by CARD_1:def 7;
assume i in 2+n+k;
then per cases by A36,AFINSQ_1:20;
suppose
A40: i in dom (<%Z1,x%>^X);
then
A41: (<%Z1,x%>^X^YC).i = (<%Z1,x%>^X).i &
(<%b1,x%>^X^YYb).i = (<%b1,x%>^X).i by A38,A37,AFINSQ_1:def 3;
per cases by A40,AFINSQ_1:20;
suppose
A42: i in dom <%Z1,x%>;
then
A43: i in Segm 2 by CARD_1:def 7;
A44: (<%Z1,x%>^X).i = <%Z1,x%>.i & (<%b1,x%>^X).i = <%b1,x%>.i
by A42,A37,AFINSQ_1:def 3;
per cases by A43,NAT_1:23,NAT_1:44;
suppose i=0;
then
A45: (<%Z1,x%>^X^YC).i = Z1 & (<%b1,x%>^X^YYb).i = b1
by A40,A38,A37,AFINSQ_1:def 3,A44;
A46: (K!+1) gcd (K!)= ((b1 * (K!))+(K!+1)) gcd (K!) by EULER_1:8;
A47: (K!+1) gcd K! = 1 by INT_2:def 3,PEPIN:1;
A48: h.b divides Product h by A15,A32,INT_4:32;
A49: (Z1-b1)*(K!) = Product (1+(K! * idseq x1)) - h.b by A29,A33;
h.b divides (Z1-b1)*(K!) by A48,A49,INT_5:1;
hence thesis by A45,A47,INT_2:25,A46,INT_2:def 3,A33;
end;
suppose i=1;
hence thesis by INT_2:12,A41,A44;
end;
end;
suppose ex j st j in dom X & i = len (<%Z1,x%>)+j;
then consider j such that
A50: j in dom X & i = 2+j by A37;
(<%Z1,x%>^X).i = X.j&(<%b1,x%>^X).i = X.j
by A37,A50,AFINSQ_1:def 3;
hence thesis by A41,INT_2:12;
end;
end;
suppose ex j st j in dom YC & i = len (<%Z1,x%>^X)+j;
then consider j such that
A51: j in dom YC & i = len (<%Z1,x%>^X)+j;
A52: (<%Z1,x%>^X^YC).i = YC.j by A51,AFINSQ_1:def 3;
A53: (<%b1,x%>^X^YYb).i = YYb.j by A39,A37,A38,A51,AFINSQ_1:def 3;
reconsider J=j, YCj=YC.j as Element of NAT by A51;
YC.j,YYb.j are_congruent_mod h.(b1+1) by A34,A27,A51;
hence thesis by A52,A53,INT_1:def 4;
end;
end;
then h.b divides E-0 by A32,A35,Th1;
hence thesis;
end;
Product h divides E
proof
per cases;
suppose E>=0;
hence thesis by A30,A31,A15,INT_4:38;
end;
suppose E <0;
then reconsider mE=-E as Element of NAT by INT_1:3;
for b be Element of NAT st b in dom h holds h.b divides mE
by A31,INT_2:10;
hence thesis by INT_2:10,A30,A15,INT_4:38;
end;
end;
then Product h divides E-0;
hence eval(p,@(<%Z1,x%>^X^YC)),0 are_congruent_mod (1+(Z1+1)*(K!))
by A29,INT_1:def 4;
let i be Nat such that
A54: i in k;
set YCe = ((YC.i+1)+(-idseq x1));
A55: dom YCe = dom (-idseq x1) =dom idseq x1 by VALUED_1:def 2,8;
A56: for j st j in dom YCe holds YCe.j = (YC.i+1) - j
proof
let j such that
A57: j in dom YCe;
thus YCe.j = (YC.i+1) + (- idseq x1).j by A57,VALUED_1:def 2
.= (YC.i+1) +-((idseq x1).j) by VALUED_1:8
.= (YC.i+1) +- j by A57,A55,FINSEQ_2:49
.= (YC.i+1) - j;
end;
rng YCe c= NAT
proof
let b be Integer;
assume b in rng YCe;
then consider a be object such that
A58: a in dom YCe & YCe.a=b by FUNCT_1:def 3;
reconsider a as Nat by A58;
A59: YCe.a = (YC.i+1)-a by A56,A58;
YC.i > x1>= a by A27,A54,A55,A58,FINSEQ_1:1;
then YC.i > a by XXREAL_0:2;
then YC.i +1 > a by NAT_1:13;
then (YC.i+1)-a is Nat by NAT_1:21;
hence thesis by A58,A59,ORDINAL1:def 12;
end;
then
reconsider YCe as FinSequence of NAT by FINSEQ_1:def 4;
reconsider PP=Product YCe as Element of NAT;
A60: for b be Element of NAT st b in dom h holds h.b divides PP
proof
let b be Element of NAT such that
A61: b in dom h;
1<= b <= x1 by A61,A10,FINSEQ_3:25;
then reconsider b1=b-1 as Nat;
YY.b1.i in M;
then reconsider YYb1i= YY.b1.i as Nat by A8;
b1+1<=x1 by A61,A10,FINSEQ_3:25;
then b1 < Segm x1 by NAT_1:13;
then
A62: b1 in x1 by NAT_1:44;
then P[b1,YY.b1] by A6;
then
A63: YYb1i <= x by A54;
YC.i,YYb1i are_congruent_mod h.(b1+1) by A62,A27,A54;
then
A64: h.b divides (YC.i - YYb1i) by INT_1:def 4;
0+1 <= YYb1i+1 <= x1 by A63,XREAL_1:7;
then
A65: YYb1i+1 in dom YCe by A55;
then
A66: YCe.(YYb1i+1) = (YC.i+1) - (YYb1i+1) by A56;
YCe.(YYb1i+1) divides PP by A65,INT_4:32;
hence thesis by A66,A64,INT_2:9;
end;
Product h divides PP-0 by A30,A60,A15,INT_4:38;
hence Product ((YC.i+1)+(-idseq x1)),0 are_congruent_mod (1+(Z1+1)*(K!))
by INT_1:def 4,A29;
end;
given Y be k-element XFinSequence of NAT,
Z,K be Element of NAT such that
A67: K> x & K >= (sum_of_coefficients |.p.|)* ((x^2+1)
* (Product (1+X)))|^(degree p) and
A68: for i be Nat st i in k holds Y.i > x1 and
A69: 1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1)))&
eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) and
A70: for i be Nat st i in k holds
Product ((Y.i+1)+(-idseq x1)),0 are_congruent_mod (1+(Z+1)*(K!));
let z be Element of NAT such that
A71: z <= x;
set z1=z+1,K1 = K!,ZZ = 1+(z+1)*K1;
A72: ZZ >1 +0 by XREAL_1:8;
consider prim be Element of NAT such that
A73: prim divides ZZ & prim <= ZZ & prim is prime by A72, NAT_4:13;
deffunc P(object) = Y.$1 mod prim;
consider Yz be XFinSequence such that
A74: len Yz = k & for i be Nat st i in k holds Yz.i = P(i)
from AFINSQ_1:sch 2;
rng Yz c= NAT
proof
let y be object;
assume y in rng Yz;
then consider x be object such that
A75: x in dom Yz & Yz.x=y by FUNCT_1:def 3;
y = P(x) by A74,A75;
hence thesis by ORDINAL1:def 12;
end;
then reconsider Yz as k-element XFinSequence of NAT
by A74,RELAT_1:def 19,CARD_1:def 7;
take Yz;
1<= z1 <= x1 by A71,NAT_1:11,XREAL_1:6;
then
A76: z1 in Seg (x1);
K>=x1 by A67,NAT_1:13;
then reconsider h=1+(K1 * idseq (x1)) as CR_Sequence by Th2;
rng h c= NAT by VALUED_0:def 6;
then
A77: h is FinSequence of NAT by FINSEQ_1:def 4;
A78: dom h = dom (K1 * idseq (x+1)) =dom idseq (x+1) by VALUED_1:def 2,def 5;
A79: h.z1 = 1 + (K1 * idseq (x+1)).z1 by A76,A78,VALUED_1:def 2
.= 1+K1 * ((idseq (x+1)).z1) by A76,A78,VALUED_1:def 5
.=ZZ by A76,FINSEQ_2:49;
ZZ divides (1+(Z+1)*K1) by A79,A69,A77,INT_4:32,A76,A78;
then
A80: prim divides (1+(Z+1)*K1) by A73,INT_2:9;
1+(Z+1)*K1 divides eval(p,@(<%Z,x%>^X^Y)) - 0 by A69,INT_1:def 4;
then
A81: prim divides eval(p,@(<%Z,x%>^X^Y)) by A80,INT_2:9;
reconsider E1=eval(p,@(<%Z,x%>^X^Y)) as Integer;
A82: K < prim
proof
assume K >= prim;
then prim divides (Z+1)*K1 by INT_2:2,A73,NEWTON:41;
then prim divides 1 by A80,INT_2:1;
then prim = 1 by INT_2:13;
hence thesis by A73,INT_2:def 4;
end;
A83: len <%z,x%> = 2 = len <%Z,x%> by CARD_1:def 7;
A84: len (<%z,x%>^X) = 2+n = len (<%Z,x%>^X) by CARD_1:def 7;
A85: len Y = k = len Yz by CARD_1:def 7;
A86: len (<%z,x%>^X^Yz) = 2+k+n by CARD_1:def 7;
thus for i be Nat st i in k holds Yz.i <=x
proof
let j be Nat such that
A87: j in k;
set YE = (Y.j+1)+(-idseq x1);
A88: Yz.j = Y.j mod prim by A87,A74;
A89: 1+(Z+1)*K1 divides Product YE - 0 by INT_1:def 4,A70,A87;
A90: len YE = len idseq x1 = x1 by CARD_1:def 7;
A91:for w be Nat st w in dom YE holds
((Y.j+1)+(-idseq x1)).w = (Y.j) +1-w
proof
let w be Nat;
assume
A92: w in dom YE;
then w in dom (-idseq x1) by VALUED_1:def 2;
then w in dom idseq x1 by VALUED_1:8;
then (idseq x1).w=w by FINSEQ_2:49;
then (- idseq x1).w = -w by VALUED_1:8;
then YE.w = (Y.j) +1+ -w by A92,VALUED_1:def 2;
hence thesis;
end;
A93: now let a be Nat;
assume
A94: a in dom YE;
then 1<= a <= x1 by A90,FINSEQ_3:25;
then reconsider a1=a-1 as Nat;
a1+1 <=x1 by A94,A90,FINSEQ_3:25;
then a1 < x1 by NAT_1:13;
then
A95: x1-a1 >0 by XREAL_1:50;
YE.a = Y.j +1-a by A94,A91;
then YE.a+a1 > x1 by A68,A87;
hence YE.a >0 by A95,XREAL_1:19;
end;
now let r be object;
assume r in rng YE;
then consider a be object such that
A96: a in dom YE & YE.a = r by FUNCT_1:def 3;
reconsider a as Nat by A96;
YE.a >0 by A93,A96;
hence r in NAT by A96,INT_1:3;
end;
then
A97: YE is FinSequence of NAT by FINSEQ_1:def 4,TARSKI:def 3;
YE is positive-yielding
proof
let r be Real;
assume r in rng YE;
then consider a be object such that
A98: a in dom YE & YE.a = r by FUNCT_1:def 3;
thus thesis by A93,A98;
end;
then consider w be Nat such that
A99: w in dom YE & prim divides YE.w by A89,A80,INT_2:9,Th12,A73,A97;
A100: 1 <= w <= x1 by A90,A99,FINSEQ_3:25;
then reconsider w1=w-1 as Nat;
prim divides Y.j+ 1 -w by A99,A91;
then prim divides Y.j -w1;
then Yz.j = w1 mod prim by A88,INT_4:23,A73;
then Yz.j < w1+1 by NAT_1:13,NEWTON05:11;
then Yz.j < x1 by A100,XXREAL_0:2;
hence thesis by NAT_1:13;
end;
for i st i in 2+k+n holds prim divides ((<%Z,x%>^X^Y).i - (<%z,x%>^X^Yz).i)
proof
let i such that
A101: i in 2+k+n;
per cases by A101,A86,AFINSQ_1:20;
suppose
A102: i in dom (<%z,x%>^X);
then
A103: ((<%z,x%>^X^Yz)).i = (<%z,x%>^X).i & ((<%Z,x%>^X^Y)).i = (<%Z,x%>^X).i
by A84,AFINSQ_1:def 3;
per cases by A102,AFINSQ_1:20;
suppose i in dom <%z,x%>;
then
A104: i in Segm 2 & (<%z,x%>^X).i = <%z,x%>.i & (<%Z,x%>^X).i = <%Z,x%>.i
by A83,AFINSQ_1:def 3;
per cases by A104,NAT_1:23,NAT_1:44;
suppose i=0;
then
A105: (<%Z,x%>^X^Y).i =Z & (<%z,x%>^X^Yz).i = z
by A102,A84,AFINSQ_1:def 3,A104;
A106: K1,prim are_coprime
proof
assume not K1,prim are_coprime;
then
A107: K1 gcd prim <>1 by INT_2:def 3;
K1 gcd prim divides prim by INT_2:def 2;
then K1 gcd prim = prim by A107,A73,INT_2:def 4;
then prim divides K1 by INT_2:def 2;
hence thesis by A82,NAT_4:19,A73;
end;
prim divides (1+(Z+1)*K1) - (1+(z+1)*K1) by A80,A73,INT_5:1;
then prim divides (Z-z)*K1;
hence thesis by A105,A106,INT_2:25;
end;
suppose i=1;
hence thesis by A103,A104,INT_2:12;
end;
end;
suppose ex j be Nat st j in dom X & i = len (<%z,x%>)+j;
then consider j such that
A108: j in dom X & i = len (<%z,x%>)+j;
(<%z,x%>^X).i = X.j & (<%Z,x%>^X).i = X.j by A83,A108,AFINSQ_1:def 3;
hence thesis by INT_2:12,A103;
end;
end;
suppose ex j be Nat st j in dom Yz & i = len (<%z,x%>^X)+j;
then consider j such that
A109: j in dom Yz & i = len (<%z,x%>^X)+j;
A110:(<%Z,x%>^X^Y).i =Y.j & (<%z,x%>^X^Yz).i = Yz.j
by A84,A85,A109,AFINSQ_1:def 3;
Yz.j = Y.j mod prim by A74,A109;
hence thesis by A110,A73,PEPIN:8;
end;
end;
then prim divides E1 - eval(p,@(<%z,x%>^X^Yz)) by A73,Th1;
then prim divides eval(p,@(<%z,x%>^X^Yz)) by INT_5:2,A81;
then |.prim.| divides |.eval(p,@(<%z,x%>^X^Yz)).| by INT_2:16;
then consider m be Nat such that
A111: |.eval(p,@(<%z,x%>^X^Yz)).| =prim *m by NAT_D:def 3;
A112: x^2=x*x by SQUARE_1:def 1;
for i be object st i in dom @(<%z,x%>^X^Yz) holds
|.(@(<%z,x%>^X^Yz)).i.| <= (x^2+1) * (Product (1+X))
proof
let i be object;assume i in dom @(<%z,x%>^X^Yz);
then
A113: i in dom (<%z,x%>^X^Yz) & (<%z,x%>^X^Yz) = @(<%z,x%>^X^Yz)
by HILB10_2:def 1;
reconsider i as Nat by A113;
per cases by A113,AFINSQ_1:20;
suppose
A114: i in dom (<%z,x%>^X);
then
A115: (@(<%z,x%>^X^Yz)).i = (<%z,x%>^X).i by A113,AFINSQ_1:def 3;
per cases by A114,AFINSQ_1:20;
suppose i in dom <%z,x%>;
then
A116: i in Segm 2 & (<%z,x%>^X).i = <%z,x%>.i
by CARD_1:def 7,AFINSQ_1:def 3;
A117: (Product (1+X))>= 1 by NAT_1:14;
x^2 >= x*1 by NAT_1:14,A112, XREAL_1:64;
then x^2+1 >= x+0 by XREAL_1:7;
then
A118: (x^2+1)* ((Product (1+X)))>= x*1 by A117,XREAL_1:66;
i=0 or i=1 by A116,NAT_1:23,NAT_1:44;
hence thesis by A118,A71,XXREAL_0:2,A115,A116;
end;
suppose ex j be Nat st j in dom X & i = len (<%z,x%>)+j;
then consider j such that
A119: j in dom X & i = len (<%z,x%>)+j;
A120: dom (1+X) = dom X by VALUED_1:def 2;
then
A121: (1+X).j <= Product (1+X) by A119,HILB10_4:11;
(1+X).j = 1+(X.j) by A119,A120,VALUED_1:def 2;
then
A122: X.j <= Product (1+X) by A121,NAT_1:13;
x^2+1>=1 by NAT_1:11;
then 1*(X.j) <= (x^2+1) * Product (1+X) by A122,XREAL_1:66;
hence thesis by A119,AFINSQ_1:def 3,A115;
end;
end;
suppose ex j be Nat st j in dom Yz & i = len (<%z,x%>^X)+j;
then consider j such that
A123: j in dom Yz & i = len (<%z,x%>^X)+j;
set YE = (Y.j+1)+(-idseq x1);
A124: (<%z,x%>^X^Yz).i = Yz.j by A123,AFINSQ_1:def 3;
A125: Yz.j = Y.j mod prim by A123,A74;
A126: 1+(Z+1)*K1 divides Product YE - 0 by INT_1:def 4,A70,A123,A74;
A127: len YE = len idseq x1 = x1 by CARD_1:def 7;
A128: for w be Nat st w in dom YE holds
((Y.j+1)+(-idseq x1)).w = (Y.j) +1-w
proof
let w be Nat;
assume
A129: w in dom YE;
then w in dom (-idseq x1) by VALUED_1:def 2;
then w in dom idseq x1 by VALUED_1:8;
then (idseq x1).w=w by FINSEQ_2:49;
then (- idseq x1).w = -w by VALUED_1:8;
then YE.w = (Y.j) +1+ -w by A129,VALUED_1:def 2;
hence thesis;
end;
A130: now let a be Nat;
assume
A131: a in dom YE;
1<= a <= x1 by A131,A127,FINSEQ_3:25;
then reconsider a1=a-1 as Nat;
a1+1 <=x1 by A131,A127,FINSEQ_3:25;
then a1 < x1 by NAT_1:13;
then
A132: x1-a1 >0 by XREAL_1:50;
YE.a = Y.j +1-a by A131,A128;
then YE.a+a1 > x1 by A68,A85,A123;
hence YE.a >0 by A132,XREAL_1:19;
end;
now let r be object;
assume r in rng YE;
then consider a be object such that
A133: a in dom YE & YE.a = r by FUNCT_1:def 3;
reconsider a as Nat by A133;
YE.a >0 by A130,A133;
hence r in NAT by A133,INT_1:3;
end;
then
A134: YE is FinSequence of NAT by FINSEQ_1:def 4,TARSKI:def 3;
YE is positive-yielding
proof
let r be Real;
assume r in rng YE;
then consider a be object such that
A135: a in dom YE & YE.a = r by FUNCT_1:def 3;
thus thesis by A130,A135;
end;
then consider w be Nat such that
A136: w in dom YE & prim divides YE.w by A126,A80,INT_2:9,Th12,A73,A134;
A137: 1 <= w <= x1 by A127,A136,FINSEQ_3:25;
then reconsider w1=w-1 as Nat;
prim divides Y.j+ 1 -w by A136,A128;
then prim divides Y.j -w1;
then Yz.j = w1 mod prim by A125,INT_4:23,A73;
then Yz.j < w1+1 by NAT_1:13,NEWTON05:11;
then
A138: Yz.j < x1 by A137,XXREAL_0:2;
x^2 >= x*1 by NAT_1:14,A112, XREAL_1:64;
then x^2+1 >= x1 by XREAL_1:7;
then
A139: Yz.j < x^2+1 by A138,XXREAL_0:2;
Product (1+X)>=1 by NAT_1:14;
then 1*(Yz.j) <= (x^2+1) * Product (1+X) by A139,XREAL_1:66;
hence thesis by A124,A113;
end;
end;
then |.eval(p,@(<%z,x%>^X^Yz)).| <= (sum_of_coefficients |.p.|)
* (((x^2+1) * (Product (1+X)))|^ degree p) by NAT_1:14,Th10;
then |.eval(p,@(<%z,x%>^X^Yz)).| <= K by A67,XXREAL_0:2;
then prim*m < prim*1 by A111,A82,XXREAL_0:2;
then m < 1 by XREAL_1:66;
then m=0 by NAT_1:14;
hence thesis by A111;
end;
theorem
for p being INT -valued Polynomial of 2+n+k,F_Real holds
{X where X is n-element XFinSequence of NAT:
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex y being k-element XFinSequence of NAT st
eval(p,@(<%z,x%>^X^y)) = 0}
is diophantine Subset of n -xtuples_of NAT
proof
let p being INT -valued Polynomial of 2+n+k,F_Real;
set X0= {X where X is n-element XFinSequence of NAT:
ex x be Element of NAT st for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st eval(p,@(<%z,x%>^X^y)) = 0};
set NK=1+n+k, sum=sum_of_coefficients |.p.|,Deg=degree p;
A1: 0 <NK+4 & NK+0< NK+4 & NK+1 < NK+4 & NK+2 < NK+4 & NK+3 < NK+4
by XREAL_1:8;
then 0 in Segm (NK+4) & NK+0 in Segm (NK+4) & NK+1 in Segm (NK+4) &
NK+2 in Segm (NK+4) & NK+3 in Segm (NK+4) by NAT_1:44;
then reconsider ZERO=0,i0=NK,i1 = NK+1,i2 = NK+2,i3 = NK+3
as Element of NK+4;
defpred P2[XFinSequence of NAT] means 1 * ($1.i1) > 1 * ($1.ZERO) + 0;
A2: {q where q is (NK+4)-element XFinSequence of NAT:P2[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by HILB10_3:7;
defpred P3[XFinSequence of NAT] means $1.i1 >= sum* ((($1.ZERO)^2+1) *
(Product (1+(($1/^1) | n) ))*(1*$1.i0+0))|^(0*($1.i0)+Deg);
1+n <= NK by NAT_1:11;
then
A3: {q where q is NK+4-element XFinSequence of NAT:P3[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by Th11,A1,XXREAL_0:2;
defpred P4[XFinSequence of NAT] means
for i be Nat st i in k holds $1.(1+n+i) > $1.i0 &
Product (($1.((1+n+i)) + 1)+(-idseq ($1.i0))),0
are_congruent_mod $1.i2;
A4: {q where q is NK+4-element XFinSequence of NAT:P4[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
proof
defpred T[Nat,Nat,Nat,Nat] means
Product (($1 + 1)+(-idseq ($2))),0 are_congruent_mod $3 & $1 > $2;
A5: for i1,i2,i3,i4 be Element of NK+4 holds
{q where q is NK+4-element XFinSequence of NAT:T[q.i1,q.i2,q.i3,q.i4]}
is diophantine Subset of (NK+4) -xtuples_of NAT
proof
let i1,i2,i3,i4 be Element of NK+4;set NK5=NK+4+1;
A6: NK+4+0 < NK5 by NAT_1:13;
then NK+4 in Segm NK5 by NAT_1:44;
then reconsider I1=i1,I2=i2,I3=i3,I4=i4,M0 =NK+4 as Element of NK5
by HILB10_3:2;
defpred G[XFinSequence of NAT] means
$1.M0 = Product (($1.I1+1)+(-idseq ($1.I2))) & $1.I1 > $1.I2;
A7: {q where q is NK5-element XFinSequence of NAT:G[q]}
is diophantine Subset of NK5 -xtuples_of NAT
by HILB10_4:38;
defpred H[XFinSequence of NAT] means 1*$1.M0,0*$1.I4
are_congruent_mod 1*$1.I3;
A8: {q where q is NK5-element XFinSequence of NAT:H[q]}
is diophantine Subset of NK5 -xtuples_of NAT by HILB10_3:21;
set GH={q where q is NK5-element XFinSequence of NAT:G[q]&H[q]};
set GHr={q|(NK+4) where q is NK5-element XFinSequence of NAT:q in GH};
set QQ = {q where q is NK+4-element XFinSequence of NAT:
T[q.i1,q.i2,q.i3,q.i4]};
A9: GH is diophantine Subset of NK5 -xtuples_of NAT
from HILB10_3:sch 3(A7,A8);
A10: GHr is diophantine Subset of (NK+4) -xtuples_of NAT
by A9,NAT_1:11,HILB10_3:5;
A11: GHr c= QQ
proof
let y be object such that
A12: y in GHr;
consider q be NK5-element XFinSequence of NAT such that
A13: y = q|(NK+4) & q in GH by A12;
A14: ex w be NK5-element XFinSequence of NAT st w = q & G[w]&H[w]
by A13;
len q = NK5 by CARD_1:def 7;then
len (q|(NK+4)) = NK+4 by A6,AFINSQ_1:54;
then reconsider Q=q|(NK+4) as NK+4-element XFinSequence of NAT
by CARD_1:def 7;
Q.i1 = q.I1 & Q.i2 = q.I2 & Q.i3 = q.I3 & Q.i4 = q.I4 by HILB10_3:4;
hence thesis by A14,A13;
end;
QQ c= GHr
proof
let y be object;
assume y in QQ;
then consider q be NK+4-element XFinSequence of NAT such that
A15: y=q & T[q.i1,q.i2,q.i3,q.i4];
Product (((q.i1) + 1)+(-idseq (q.i2)))
= (q.i2)!*((q.i1) choose (q.i2)) by HILB10_4:23,A15;
then reconsider P = Product ((q.i1 + 1)+(-idseq (q.i2)))
as Element of NAT;
set qP= q^<%P%>;
A16: len q = NK+4 by CARD_1:def 7;
A17: qP|(NK+4) = q by A16,AFINSQ_1:57;
qP.i1 = q.i1 & qP.i2 = q.i2 & qP.i3 = q.i3 by A17,HILB10_3:4;
then G[qP] & H[qP] by A15;
then qP in GH;
hence thesis by A15,A17;
end;
hence thesis by A10,A11,XBOOLE_0:def 10;
end;
set SN = { 1+n+i where i is Nat: i in k};
A18: SN c= Segm (NK+4)
proof
let x be object;assume x in SN;
then consider i be Nat such that
A19: x=1+n+i & i in k;
i in Segm k by A19;
then i+0 < k+4 by NAT_1:44, XREAL_1:8;
then 1+n+(i+0) < 1+n+(k +4) by XREAL_1:8;
hence thesis by A19,NAT_1:44;
end;
set PP = {p where p is NK+4-element XFinSequence of NAT:
for i be Nat st i in SN holds T[p.i,p.i0,p.i2,p.i2]};
for i2,i3,i4 be Element of NK+4 holds
{p where p is NK+4-element XFinSequence of NAT:
for i be Nat st i in SN holds T[p.i,p.i2,p.i3,p.i4]}
is diophantine Subset of (NK+4) -xtuples_of NAT from SubsetDioph(A5,A18);
then
A20: PP is diophantine Subset of (NK+4) -xtuples_of NAT;
set QQ= {q where q is NK+4-element XFinSequence of NAT:P4[q]};
A21: QQ c= PP
proof
let x be object;
assume x in QQ;
then consider p be NK+4-element XFinSequence of NAT such that
A22: x=p & P4[p];
for i be Nat st i in SN holds T[p.i,p.i0,p.i2,p.i2]
proof
let i be Nat;assume i in SN;
then ex j be Nat st i=1+n+j & j in k;
hence T[p.i,p.i0,p.i2,p.i2] by A22;
end;
hence thesis by A22;
end;
PP c= QQ
proof
let x be object;
assume x in PP;
then consider p be NK+4-element XFinSequence of NAT such that
A23:x=p & for i be Nat st i in SN holds T[p.i,p.i0,p.i2,p.i2];
P4[p]
proof
let i such that
A24: i in k;
1+n+i in SN by A24;
hence thesis by A23;
end;
hence thesis by A23;
end;
hence thesis by A20,XBOOLE_0:def 10,A21;
end;
defpred P5[XFinSequence of NAT] means 1 * ($1.i0) > 1 * ($1.ZERO) + 0;
A25: {q where q is NK+4-element XFinSequence of NAT:P5[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by HILB10_3:7;
defpred P6[XFinSequence of NAT] means 1+($1.(i3)+1)*($1.(i1)!) = $1.i2;
A26: {q where q is NK+4-element XFinSequence of NAT:P6[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by HILB10_4:33;
defpred P7[XFinSequence of NAT] means
$1.i2 = Product (1+(($1.i1)! * idseq (1+ $1.ZERO)));
A27: {q where q is NK+4-element XFinSequence of NAT:P7[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by HILB10_4:36;
reconsider R=p as INT -valued Polynomial of 1+NK,F_Real;
defpred P8[XFinSequence of NAT] means
for Y be (1+NK)-element XFinSequence of NAT st Y=<%$1.i3%>^($1|NK) holds
eval(R,@Y),0 are_congruent_mod $1.i2;
NK+0 < NK+3 by XREAL_1:8;
then NK+1<= NK+4 & NK in Segm i3 by XREAL_1:8, NAT_1:44;
then
A28: {q where q is NK+4-element XFinSequence of NAT:P8[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by Th15;
defpred P123[XFinSequence of NAT] means P2[$1] & P3[$1];
A29: {q where q is (NK+4)-element XFinSequence of NAT:P123[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A2,A3);
defpred P1234[XFinSequence of NAT] means P123[$1] & P4[$1];
A30: {q where q is (NK+4)-element XFinSequence of NAT:P1234[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A29,A4);
defpred P12345[XFinSequence of NAT] means P1234[$1] & P5[$1];
A31: {q where q is (NK+4)-element XFinSequence of NAT:P12345[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A30,A25);
defpred P123456[XFinSequence of NAT] means P12345[$1] & P6[$1];
A32: {q where q is (NK+4)-element XFinSequence of NAT:P123456[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A31,A26);
defpred P1234567[XFinSequence of NAT] means P123456[$1] & P7[$1];
A33: {q where q is (NK+4)-element XFinSequence of NAT:P1234567[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A32,A27);
defpred P12345678[XFinSequence of NAT] means P1234567[$1] & P8[$1];
set X3 ={q where q is (NK+4)-element XFinSequence of NAT:P12345678[q]};
A34: X3 is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A33,A28);
set X2 = {X|(n+1) where X is NK+4-element XFinSequence of NAT:X in X3};
n+1 <= 1+n+(k+4) by NAT_1:11;then
A35: X2 is diophantine Subset of (n+1) -xtuples_of NAT by A34,HILB10_3:5;
defpred S[XFinSequence of NAT] means
for z be Element of NAT st z <= $1.0
ex y be k-element XFinSequence of NAT st
for X1 be n-element XFinSequence of NAT st X1=$1/^1 holds
eval(p,@(<%z,$1.0%>^X1^y)) = 0;
set X1= {X where X is n+1-element XFinSequence of NAT: S[X]};
for s be object holds s in X1 iff s in X2
proof
let s be object;
thus s in X1 implies s in X2
proof
assume s in X1;
then consider h be n+1-element XFinSequence of NAT
such that
A36: s=h & S[h];
set X= h/^1;
len h = n+1 >= 1 by NAT_1:11,CARD_1:def 7;
then
A37: len X= n+1-'1 by AFINSQ_2:def 2;
then
A38: len X= n by NAT_D:34;
reconsider X as n-element XFinSequence of NAT
by A37,NAT_D:34,CARD_1:def 7;
set x = h.0;
for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st eval(p,@(<%z,x%>^X^y))=0
proof
let z be Element of NAT such that
A39: z <= x;
consider y be k-element XFinSequence of NAT such that
A40: for X1 be n-element XFinSequence of NAT st X1=h/^1 holds
eval(p,@(<%z,x %>^X1^y)) = 0 by A39,A36;
eval(p,@(<%z,x %>^X^y)) = 0 by A40;
hence thesis;
end;
then consider Y be k-element XFinSequence of NAT,
Z,e,K be Element of NAT such that
A41: K> x & K >= sum * ((x^2+1) * (Product (1+X))*e)|^Deg and
A42: for i be Nat st i in k holds Y.i > e and
A43: e > x and
A44: 1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1))) and
A45: eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) and
A46: for i be Nat st i in k holds
Product ((Y.i + 1)+(-idseq e)),0 are_congruent_mod (1+(Z+1)*(K!))
by Th16;
set xXY = <%x%>^X^Y, E = <%e%>^<%K%>^<%1+(Z+1)*(K!)%>^<%Z%>;
set H = xXY^E;
0 in Segm 1 by NAT_1:44;
then
A47: 0 in dom <%x%> & len <%x%> =1 &
dom <%x%> c= dom (<%x%>^X) by AFINSQ_1:21,33;
then 0 in dom (<%x%>^X) & dom (<%x%>^X) c= dom xXY by AFINSQ_1:21;
then
A48: H.0 = xXY.0 by AFINSQ_1:def 3
.= (<%x%>^X).0 by AFINSQ_1:def 3,A47
.= <%x%>.0 by AFINSQ_1:def 3,A47;
H = (<%x%>^(X^Y))^E by AFINSQ_1:27
.= <%x%>^((X^Y)^E) by AFINSQ_1:27;
then
A49: H/^1 = X^Y^E by A47,AFINSQ_2:12
.= X^(Y^E) by AFINSQ_1:27;
A50: len xXY = NK by CARD_1:def 7;
then
A51: H|NK = xXY by AFINSQ_1:57;
A52: len E=4 by CARD_1:def 7;
0 in dom E by AFINSQ_1:66;
then
A53: H.(NK+0) = E.0 by A50,AFINSQ_1:def 3
.= e by AFINSQ_1:45;
1 in dom E by A52,AFINSQ_1:66;
then
A54: H.(NK+1) = E.1 by A50,AFINSQ_1:def 3
.= K by AFINSQ_1:45;
2 in dom E by A52,AFINSQ_1:66;
then
A55: H.(NK+2) = E.2 by A50,AFINSQ_1:def 3
.= 1+(Z+1)*(K!) by AFINSQ_1:45;
3 in dom E by A52,AFINSQ_1:66;
then
A56: H.(NK+3) = E.3 by A50,AFINSQ_1:def 3
.= Z;
A57: for i be Nat st i in k holds H.(1+n+i)=Y.i
proof
let i be Nat such that
A58: i in k;
A59: len Y = k & len (<%x%>^X)=1+n by CARD_1:def 7;
then 1+n+i in dom xXY by AFINSQ_1:23,A58;
hence H.(1+n+i) = xXY.(1+n+i) by AFINSQ_1:def 3
.= Y.i by A59,A58,AFINSQ_1:def 3;
end;
A60: for i be Nat st i in k holds H.(1+n+i) > H.(NK)
proof
let i be Nat such that
A61: i in k;
H.(1+n+i)=Y.i by A61,A57;
hence thesis by A53,A42,A61;
end;
A62: for Y be 2+n+k-element XFinSequence of NAT st
Y=<%H.(NK+3)%> ^ (H|NK) holds
eval(p,@Y),0 are_congruent_mod H.(NK+2)
proof
let YY be 2+n+k-element XFinSequence of NAT such that
A63: YY=<%H.(NK+3)%> ^ (H|NK);
YY = <%Z%>^(<%x%>^(X^Y)) by A56,AFINSQ_1:27,A51,A63
.= <%Z%>^<%x%>^(X^Y) by AFINSQ_1:27
.= <%Z,x%>^X^Y by AFINSQ_1:27;
hence thesis by A45,A55;
end;
A64: for i be Nat st i in k holds
Product ((H.(1+n+i) + 1)+(-idseq (H.(NK)))),0
are_congruent_mod H.(NK+2)
proof
let i be Nat such that
A65: i in k;
H.(1+n+i) = Y.i by A65,A57;
hence thesis by A53,A55,A46,A65;
end;
A66: P2[H] by A48,A54,A41;
A67: P3[H] by A48,A49,A38,AFINSQ_1:57,A53,A54,A41;
A68: P4[H] by A60,A64;
H in X3 by A66,A67,A68,A53,A43,A56,A48,A54,A55,A44,A62;
then
A69: H|(n+1) in X2;
H|(n+1) = xXY| (n+1) & len (<%x%>^X) = 1+n
by NAT_1:11,A50,AFINSQ_1:58,CARD_1:def 7;
then H|(n+1) = <%x%>^X by AFINSQ_1:57;
hence thesis by A36,A69,NUMERAL2:2;
end;
assume s in X2;
then consider x be NK+4-element XFinSequence of NAT such that
A70: s = x|(n+1) & x in X3;
consider H be NK+4-element XFinSequence of NAT such that
A71: H=x and
A72: P12345678[H] by A70;
A73: NK+4>=NK & len H = NK+4 by NAT_1:11,CARD_1:def 7;
then
A74: len (H|NK) = NK by AFINSQ_1:54;
then
A75: len ((H|NK)/^(n+1)) = NK -'(n+1) by AFINSQ_2:def 2;
then
A76: len ((H|NK)/^(n+1)) = k by NAT_D:34;
reconsider Y = (H|NK)/^(n+1) as k-element XFinSequence of NAT
by A75,NAT_D:34,CARD_1:def 7;
reconsider x=H.0, e = H.NK, K = H.(NK+1),Z=H.(NK+3) as Element of NAT;
A77: len H = NK+3+1 by CARD_1:def 7;
then len (H/^1) = NK+3+1-'1 by AFINSQ_2:def 2;
then
A78: len (H/^1) = NK+3 by NAT_D:34;
1+k+3+n >= n by NAT_1:11;
then len ((H/^1)|n) = n by AFINSQ_1:54,A78;
then reconsider X = (H/^1)|n as n-element XFinSequence of NAT
by CARD_1:def 7;
A79: for i be Nat st i in k holds Y.i = H.(1+n+i)
proof
let i be Nat such that
A80: i in k;
A81: Y.i = (H|NK).(n+1+i) by A80,A76,AFINSQ_2:def 2;
i in Segm k by A80;
then 1+n+i < Segm NK by XREAL_1:8,NAT_1:44;
hence thesis by A81,NAT_1:44,FUNCT_1:49;
end;
A82: for i be Nat st i in k holds Y.i > e
proof
let i such that
A83: i in k;
Y.i = H.(1+n+i) by A83,A79;
hence thesis by A83,A72;
end;
len <%Z%>=1 by CARD_1:def 7;
then len (<%Z%> ^ (H|NK)) = 1+NK by A74,AFINSQ_1:17;
then reconsider ZY = <%Z%> ^ (H|NK) as 2+n+k-element XFinSequence of NAT
by CARD_1:def 7;
Segm(n+1) c= Segm(NK) by NAT_1:11,39;then
(H|NK)|(n+1) = H|(n+1) by RELAT_1:74;
then
A84: H|NK = (H|(n+1))^Y;
A85: (1+1)-'1 = 1 & n+2-'2 = n by NAT_D:34;
n+1 <= n+1+(k+4) by NAT_1:11;
then
A86: (H/^((1+1)-'1))|(n+1+1-'(1+1))=mid(H,1+1,n+1) by A73,AFINSQ_2:15
.= (H|(n+1))/^(1+1-'1) by AFINSQ_2:def 3;
A87: H|(n+1) = (H|(n+1)|1)^((H/^1)|n) by A85,A86;
Segm 1 c= Segm(n+1) by NAT_1:11,39;
then (H|(n+1)|1) = H|1 by RELAT_1:74
.= <%H.0%> by NUMERAL2:1;
then ZY = <%Z%> ^ (<% x %>^(X^Y)) by A84,A87,AFINSQ_1:27
.=<%Z%> ^ <% x %>^(X^Y) by AFINSQ_1:27
.= <%Z,x%>^X^Y by AFINSQ_1:27;
then
A88: eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) by A72;
A89: for i be Nat st i in k holds
Product ((Y.i + 1)+(-idseq e)),0 are_congruent_mod (1+(Z+1)*(K!))
proof
let i; assume
A90: i in k; then
Y.i = H.(n+1+i) by A79;
hence thesis by A90,A72;
end;
n+1 <= n+1+(k+4) by NAT_1:11;
then len (H|(n+1)) = n+1 by AFINSQ_1:54,A77;
then reconsider F = H|(n+1) as n+1-element XFinSequence of NAT
by CARD_1:def 7;
A91: 0 < len F;
then
A92: F.0=H.0 by FUNCT_1:47,AFINSQ_1:66;
for z be Element of NAT st z <= F.0
ex y be k-element XFinSequence of NAT st
for X1 be n-element XFinSequence of NAT st X1=F/^1 holds
eval(p,@(<%z,F.0%>^X1^y)) = 0
proof
let z be Element of NAT such that
A93: z<=F.0;
consider y be k-element XFinSequence of NAT such that
A94: eval(p,@(<%z,x%>^X^y)) = 0 by A93,A92,A89,Th16,A72,A82,A88;
take y;
let X1 be n-element XFinSequence of NAT;
assume X1=F/^1;
hence thesis by A94,A91,FUNCT_1:47,AFINSQ_1:66,A86,A85;
end;
hence thesis by A71,A70;
end;
then
A95: X1 =X2 by TARSKI:2;
set Y1 = {X/^1 where X is n+1-element XFinSequence of NAT: X in X1};
A96: Y1 is diophantine Subset of n -xtuples_of NAT by A95,A35,HILB10_4:27;
for s be object holds s in Y1 iff s in X0
proof
let s be object;
thus s in Y1 implies s in X0
proof
assume s in Y1;
then consider xS be (n+1)-element XFinSequence of NAT such that
A97: s=xS/^1 & xS in X1;
A98: ex w be (n+1)-element XFinSequence of NAT st xS = w & S[w]
by A97;
len xS=n+1 by CARD_1:def 7;
then len (xS/^1)=n+1-'1 by AFINSQ_2:def 2;
then reconsider S=xS/^1 as n-element XFinSequence of NAT
by NAT_D:34,CARD_1:def 7;
ex x be Element of NAT st for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
eval(p,@(<%z,x%>^S^y)) = 0
proof
take x=xS.0;
let z be Element of NAT such that
A99: z <= x;
consider y be k-element XFinSequence of NAT such that
A100: for X1 be n-element XFinSequence of NAT st X1=xS/^1 holds
eval(p,@(<%z,xS.0%>^X1^y)) = 0 by A98,A99;
eval(p,@(<%z,x%>^S^y)) = 0 by A100;
hence thesis;
end;
hence thesis by A97;
end;
assume s in X0;
then consider S be n-element XFinSequence of NAT such that
A101: s=S & ex x be Element of NAT st for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
eval(p,@(<%z,x%>^S^y)) = 0;
consider x be Element of NAT such that
A102: for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
eval(p,@(<%z,x%>^S^y)) = 0 by A101;
set xS = <%x%>^S;
A103: len <%x%> =1 by CARD_1:def 7;
then
A104: xS/^1 =S by AFINSQ_2:12;
S[xS]
proof
let z be Element of NAT such that
A105: z <= xS.0;
A106: xS.0 = x by AFINSQ_1:35;
then consider y be k-element XFinSequence of NAT such that
A107: eval(p,@(<%z,x%>^S^y)) = 0 by A102,A105;
take y;
thus thesis by AFINSQ_2:12,A103,A106,A107;
end;
then xS in X1;
hence s in Y1 by A104,A101;
end;
hence thesis by A96,TARSKI:2;
end;
theorem Th19:
for p being INT -valued Polynomial of 2+n+k,F_Real holds
{X where X is n-element XFinSequence of NAT:
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex y being k-element XFinSequence of NAT st
(for i being Nat st i in k holds y.i <= x) &
eval(p,@(<%z,x%>^X^y)) = 0}
is diophantine Subset of n -xtuples_of NAT
proof
let p being INT -valued Polynomial of 2+n+k,F_Real;
set X0= {X where X is n-element XFinSequence of NAT:
ex x be Element of NAT st for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
(for i be Nat st i in k holds y.i <= x) &
eval(p,@(<%z,x%>^X^y)) = 0};
set NK=1+n+k, sum=sum_of_coefficients |.p.|,Deg=degree p;
A1: 0 <NK+4 & NK+0< NK+4 & NK+1 < NK+4 & NK+2 < NK+4 & NK+2 < NK+4
by XREAL_1:8;
then 0 in Segm (NK+4) & NK+0 in Segm (NK+4) & NK+1 in Segm (NK+4) &
NK+2 in Segm (NK+4) by NAT_1:44;
then reconsider ZERO=0,i0=NK,i1 = NK+1,i2 = NK+2,i3 = NK+3
as Element of NK+4 by HILB10_3:3;
defpred P2[XFinSequence of NAT] means 1 * ($1.i1) > 1 * ($1.ZERO) + 0;
A2:{q where q is (NK+4)-element XFinSequence of NAT:P2[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by HILB10_3:7;
defpred P3[XFinSequence of NAT] means
$1.i1 >= sum* ((($1.ZERO)^2+1) *
(Product (1+(($1/^1) | n) ))*(0*$1.i0+1))|^(0*($1.i0)+Deg);
1+n <= NK by NAT_1:11;
then
A3:{q where q is NK+4-element XFinSequence of NAT:P3[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by Th11,A1,XXREAL_0:2;
defpred P4[XFinSequence of NAT] means
for i be Nat st i in k holds $1.(1+n+i) > $1.i0 &
Product (($1.((1+n+i)) + 1)+(-idseq ($1.i0))),
0 are_congruent_mod $1.i2;
A4:{q where q is NK+4-element XFinSequence of NAT:P4[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
proof
defpred T[Nat,Nat,Nat,Nat] means
Product (($1 + 1)+(-idseq ($2))),0 are_congruent_mod $3 & $1 > $2;
A5: for i1,i2,i3,i4 be Element of NK+4 holds
{q where q is NK+4-element XFinSequence of NAT:T[q.i1,q.i2,q.i3,q.i4]}
is diophantine Subset of (NK+4) -xtuples_of NAT
proof
let i1,i2,i3,i4 be Element of NK+4;set NK5=NK+4+1;
A6: NK+4+0 < NK5 by NAT_1:13;
then NK+4 in Segm NK5 by NAT_1:44;
then reconsider I1=i1,I2=i2,I3=i3,I4=i4,M0 =NK+4 as Element of NK5
by HILB10_3:2;
defpred G[XFinSequence of NAT] means
$1.M0 = Product (($1.I1+1)+(-idseq ($1.I2))) & $1.I1 > $1.I2;
A7: {q where q is NK5-element XFinSequence of NAT:G[q]}
is diophantine Subset of NK5 -xtuples_of NAT by HILB10_4:38;
defpred H[XFinSequence of NAT] means
1*$1.M0,0*$1.I4 are_congruent_mod 1*$1.I3;
A8: {q where q is NK5-element XFinSequence of NAT:H[q]}
is diophantine Subset of NK5 -xtuples_of NAT by HILB10_3:21;
set GH={q where q is NK5-element XFinSequence of NAT:G[q]&H[q]};
set GHr={q|(NK+4) where q is NK5-element XFinSequence of NAT : q in GH};
set QQ = {q where q is NK+4-element XFinSequence of NAT:
T[q.i1,q.i2,q.i3,q.i4]};
A9: GH is diophantine Subset of NK5 -xtuples_of NAT
from HILB10_3:sch 3(A7,A8);
A10: GHr is diophantine Subset of (NK+4) -xtuples_of NAT
by A9,HILB10_3:5,NAT_1:11;
A11: GHr c= QQ
proof
let y be object such that
A12: y in GHr;
consider q be NK5-element XFinSequence of NAT such that
A13: y = q|(NK+4) & q in GH by A12;
A14: ex w be NK5-element XFinSequence of NAT st w=q&G[w]&H[w] by A13;
len q = NK5 by CARD_1:def 7;
then len (q|(NK+4)) = NK+4 by A6,AFINSQ_1:54;
then reconsider Q=q|(NK+4) as NK+4-element XFinSequence of NAT
by CARD_1:def 7;
Q.i1 = q.I1 & Q.i2 = q.I2 & Q.i3 = q.I3 & Q.i4 = q.I4 by HILB10_3:4;
hence thesis by A13,A14;
end;
QQ c= GHr
proof
let y be object;
assume y in QQ;
then consider q be NK+4-element XFinSequence of NAT such that
A15: y=q & T[q.i1,q.i2,q.i3,q.i4];
Product (((q.i1) + 1)+(-idseq (q.i2)))
= (q.i2)!*((q.i1) choose (q.i2)) by A15,HILB10_4:23;
then reconsider P = Product ((q.i1 + 1)+(-idseq (q.i2)))
as Element of NAT;
set qP= q^<%P%>;
A16: len q = NK+4 by CARD_1:def 7;
A17: qP|(NK+4) = q by A16,AFINSQ_1:57;
qP.i1 = q.i1 & qP.i2 = q.i2 & qP.i3 = q.i3 by A17,HILB10_3:4;
then G[qP] & H[qP] by A15;
then qP in GH;
hence thesis by A15,A17;
end;
hence thesis by A10,A11,XBOOLE_0:def 10;
end;
set SN = { 1+n+i where i is Nat: i in k};
A18: SN c= Segm (NK+4)
proof
let x be object;assume x in SN;
then consider i be Nat such that
A19: x=1+n+i & i in k;
i in Segm k by A19;
then i+0 < k+4 by NAT_1:44, XREAL_1:8;
then 1+n+(i+0) < 1+n+(k +4) by XREAL_1:8;
hence thesis by A19,NAT_1:44;
end;
set PP = {p where p is NK+4-element XFinSequence of NAT:
for i be Nat st i in SN holds T[p.i,p.i0,p.i2,p.i2]};
for i2,i3,i4 be Element of NK+4 holds {p where p
is NK+4-element XFinSequence of NAT:
for i be Nat st i in SN holds T[p.i,p.i2,p.i3,p.i4]}
is diophantine Subset of (NK+4) -xtuples_of NAT from SubsetDioph(A5,A18);
then
A20: PP is diophantine Subset of (NK+4) -xtuples_of NAT;
set QQ= {q where q is NK+4-element XFinSequence of NAT:P4[q]};
A21: QQ c= PP
proof
let x be object;
assume x in QQ;
then consider p be NK+4-element XFinSequence of NAT such that
A22: x=p & P4[p];
for i be Nat st i in SN holds T[p.i,p.i0,p.i2,p.i2]
proof
let i be Nat;assume i in SN;
then ex j be Nat st i=1+n+j & j in k;
hence T[p.i,p.i0,p.i2,p.i2] by A22;
end;
hence thesis by A22;
end;
PP c= QQ
proof
let x be object;
assume x in PP;
then consider p be NK+4-element XFinSequence of NAT such that
A23: x=p & for i be Nat st i in SN holds T[p.i,p.i0,p.i2,p.i2];
P4[p]
proof
let i;
assume i in k;
then 1+n+i in SN;
hence thesis by A23;
end;
hence thesis by A23;
end;
hence thesis by A20,XBOOLE_0:def 10,A21;
end;
defpred P5[XFinSequence of NAT] means ($1.i0) = 1 * ($1.ZERO) + 1;
A24: {q where q is NK+4-element XFinSequence of NAT:P5[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by HILB10_3:15;
defpred P6[XFinSequence of NAT] means 1+($1.(i3)+1)*($1.(i1)!) = $1.i2;
A25: {q where q is NK+4-element XFinSequence of NAT:P6[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by HILB10_4:33;
defpred P7[XFinSequence of NAT] means
$1.i2 = Product (1+(($1.i1)! * idseq (1+ $1.ZERO)));
A26: {q where q is NK+4-element XFinSequence of NAT:P7[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by HILB10_4:36;
reconsider R=p as INT -valued Polynomial of 1+NK,F_Real;
defpred P8[XFinSequence of NAT] means
for Y be (1+NK)-element XFinSequence of NAT st Y=<%$1.i3%> ^ ($1|NK) holds
eval(R,@Y),0 are_congruent_mod $1.i2;
NK+0 < NK+3 by XREAL_1:8;
then NK+1<= NK+4 & NK in Segm i3 by XREAL_1:8, NAT_1:44;
then
A27: {q where q is NK+4-element XFinSequence of NAT:P8[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT by Th15;
defpred P123[XFinSequence of NAT] means P2[$1] & P3[$1];
A28: {q where q is (NK+4)-element XFinSequence of NAT:P123[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A2,A3);
defpred P1234[XFinSequence of NAT] means P123[$1] & P4[$1];
A29: {q where q is (NK+4)-element XFinSequence of NAT:P1234[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A28,A4);
defpred P12345[XFinSequence of NAT] means P1234[$1] & P5[$1];
A30: {q where q is (NK+4)-element XFinSequence of NAT:P12345[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A29,A24);
defpred P123456[XFinSequence of NAT] means P12345[$1] & P6[$1];
A31: {q where q is (NK+4)-element XFinSequence of NAT:P123456[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A30,A25);
defpred P1234567[XFinSequence of NAT] means P123456[$1] & P7[$1];
A32: {q where q is (NK+4)-element XFinSequence of NAT:P1234567[q]}
is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A31,A26);
defpred P12345678[XFinSequence of NAT] means P1234567[$1] & P8[$1];
set X3 ={q where q is (NK+4)-element XFinSequence of NAT:P12345678[q]};
A33: X3 is diophantine Subset of (NK+4) -xtuples_of NAT
from HILB10_3:sch 3(A32,A27);
set X2 = {X|(n+1) where X is NK+4-element XFinSequence of NAT:X in X3};
n+1 <= 1+n+(k+4) by NAT_1:11;then
A34: X2 is diophantine Subset of (n+1) -xtuples_of NAT by A33,HILB10_3:5;
defpred S[XFinSequence of NAT] means
for z be Element of NAT st z <= $1.0
ex y be k-element XFinSequence of NAT st
for X1 be n-element XFinSequence of NAT st X1=$1/^1 holds
(for i st i in k holds y.i <= $1.0) & eval(p,@(<%z,$1.0%>^X1^y)) = 0;
set X1= {X where X is n+1-element XFinSequence of NAT: S[X]};
for s be object holds s in X1 iff s in X2
proof
let s be object;
thus s in X1 implies s in X2
proof
assume s in X1;then consider h be n+1-element XFinSequence
of NAT such that
A35: s=h & S[h];
set X= h/^1;
len h = n+1 >= 1 by NAT_1:11,CARD_1:def 7;
then
A36: len X= n+1-'1 by AFINSQ_2:def 2;
then
A37: len X= n by NAT_D:34;
reconsider X as n-element XFinSequence of NAT
by A36,NAT_D:34,CARD_1:def 7;
set x = h.0, e=x+1;
for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
(for i st i in k holds y.i <= x) & eval(p,@(<%z,x%>^X^y)) = 0
proof
let z be Element of NAT such that
A38: z <= x;
consider y be k-element XFinSequence of NAT such that
A39: for X1 be n-element XFinSequence of NAT st X1=h/^1 holds
(for i st i in k holds y.i <= x) &
eval(p,@(<%z,x %>^X1^y)) = 0 by A38,A35;
X=h/^1;
then (for i st i in k holds y.i <= x) & eval(p,@(<%z,x %>^X^y)) = 0
by A39;
hence thesis;
end;
then consider Y be k-element XFinSequence of NAT,
Z,K be Element of NAT such that
A40: K> x & K >= sum * ((x^2+1) * (Product (1+X)))|^Deg and
A41: for i be Nat st i in k holds Y.i > (x+1) and
A42: 1+(Z+1)*(K!) = Product (1+(K! * idseq (x+1))) and
A43: eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) and
A44: for i be Nat st i in k holds
Product ((Y.i + 1)+(-idseq e)),0 are_congruent_mod (1+(Z+1)*(K!))
by Th17;
set xXY = <%x%>^X^Y, E = <%e%>^<%K%>^<%1+(Z+1)*(K!)%>^<%Z%>;
set H = xXY^E;
0 in Segm 1 by NAT_1:44;
then
A45: 0 in dom <%x%> & len <%x%> =1 &
dom <%x%> c= dom (<%x%>^X) by AFINSQ_1:21,33;
then 0 in dom (<%x%>^X) & dom (<%x%>^X) c= dom xXY by AFINSQ_1:21;
then
A46: H.0 = xXY.0 by AFINSQ_1:def 3
.= (<%x%>^X).0 by AFINSQ_1:def 3,A45
.= <%x%>.0 by AFINSQ_1:def 3,A45;
H = (<%x%>^(X^Y))^E by AFINSQ_1:27
.= <%x%>^((X^Y)^E) by AFINSQ_1:27;
then
A47: H/^1 = X^Y^E by A45,AFINSQ_2:12
.= X^(Y^E) by AFINSQ_1:27;
A48: len xXY = NK by CARD_1:def 7;
A49: len E=4 by CARD_1:def 7;
0 in dom E by AFINSQ_1:66;
then
A50: H.(NK+0) = E.0 by A48,AFINSQ_1:def 3
.= e by AFINSQ_1:45;
1 in dom E by A49,AFINSQ_1:66;
then
A51: H.(NK+1) = E.1 by A48,AFINSQ_1:def 3
.= K by AFINSQ_1:45;
2 in dom E by A49,AFINSQ_1:66;
then
A52: H.(NK+2) = E.2 by A48,AFINSQ_1:def 3
.= 1+(Z+1)*(K!) by AFINSQ_1:45;
3 in dom E by A49,AFINSQ_1:66;
then
A53: H.(NK+3) = E.3 by A48,AFINSQ_1:def 3
.= Z;
A54: for i be Nat st i in k holds H.(1+n+i)=Y.i
proof
let i be Nat such that
A55: i in k;
A56: len Y = k & len (<%x%>^X)=1+n by CARD_1:def 7;
then 1+n+i in dom xXY by AFINSQ_1:23,A55;
hence H.(1+n+i) = xXY.(1+n+i) by AFINSQ_1:def 3
.= Y.i by A56,A55,AFINSQ_1:def 3;
end;
A57: for i be Nat st i in k holds H.(1+n+i) > H.(NK)
proof
let i be Nat such that
A58: i in k;
H.(1+n+i)=Y.i by A58,A54;
hence thesis by A50,A41,A58;
end;
A59: for Y be 2+n+k-element XFinSequence of NAT st
Y=<%H.(NK+3)%> ^ (H|NK) holds
eval(p,@Y),0 are_congruent_mod H.(NK+2)
proof
let YY be 2+n+k-element XFinSequence of NAT such that
A60: YY=<%H.(NK+3)%> ^ (H|NK);
YY = <%H.(NK+3)%>^xXY by A48,AFINSQ_1:57,A60
.= <%Z%>^(<%x%>^(X^Y)) by A53,AFINSQ_1:27
.= <%Z%>^<%x%>^(X^Y) by AFINSQ_1:27
.= <%Z,x%>^X^Y by AFINSQ_1:27;
hence thesis by A52,A43;
end;
A61: for i be Nat st i in k holds
Product ((H.(1+n+i) + 1)+(-idseq (H.(NK)))),0
are_congruent_mod H.(NK+2)
proof
let i be Nat; assume
A62: i in k; then
H.(1+n+i) = Y.i by A54;
hence thesis by A50,A52,A44,A62;
end;
A63: P2[H] by A46,A51,A40;
A64: P3[H] by A46,A47,A37,AFINSQ_1:57,A51,A40;
P4[H] by A57,A61; then
H in X3 by A63,A64,A46,A50,A51,A52,A53,A42,A59;
then
A66: H|(n+1) in X2;
H|(n+1) = xXY| (n+1) & len (<%x%>^X) = 1+n
by NAT_1:11,A48,AFINSQ_1:58,CARD_1:def 7;
then H|(n+1) = <%x%>^X by AFINSQ_1:57;
hence thesis by A35,A66,NUMERAL2:2;
end;
assume s in X2;
then consider x be NK+4-element XFinSequence of NAT such that
A67: s = x|(n+1) & x in X3;
consider H be NK+4-element XFinSequence of NAT such that
A68: H=x and
A69: P12345678[H] by A67;
A70: NK+4>=NK & len H = NK+4 by NAT_1:11,CARD_1:def 7;
then
A71: len (H|NK) = NK by AFINSQ_1:54;
then
A72: len ((H|NK)/^(n+1)) = NK -'(n+1) by AFINSQ_2:def 2;
then
A73: len ((H|NK)/^(n+1)) = k by NAT_D:34;
reconsider Y = (H|NK)/^(n+1) as k-element XFinSequence of NAT
by A72,CARD_1:def 7,NAT_D:34;
reconsider x=H.0, e = H.NK, K = H.(NK+1),Z=H.(NK+3) as Element of NAT;
A74: len H = NK+3+1 by CARD_1:def 7;
then len (H/^1) = NK+3+1-'1 by AFINSQ_2:def 2;
then
A75: len (H/^1) = NK+3 by NAT_D:34;
1+k+3+n >= n by NAT_1:11;
then len ((H/^1)|n) = n by AFINSQ_1:54,A75;
then reconsider X = (H/^1)|n as n-element XFinSequence of NAT
by CARD_1:def 7;
A76:for i be Nat st i in k holds Y.i = H.(1+n+i)
proof
let i be Nat; assume
A77: i in k; then
i in Segm k;
then 1+n+i < Segm NK by NAT_1:44,XREAL_1:8;
then (H|NK).(n+1+i) = H.(n+1+i) by NAT_1:44,FUNCT_1:49;
hence thesis by A77,A73,AFINSQ_2:def 2;
end;
A78:for i be Nat st i in k holds Y.i > x+1
proof
let i such that
A79: i in k;
Y.i = H.(1+n+i) by A79,A76;
hence thesis by A79,A69;
end;
len <%Z%>=1 by CARD_1:def 7;
then len (<%Z%> ^ (H|NK)) = 1+NK by A71,AFINSQ_1:17;
then reconsider ZY = <%Z%> ^ (H|NK) as 2+n+k-element XFinSequence of
NAT by CARD_1:def 7;
Segm(n+1) c= Segm(NK) by NAT_1:11,39;
then aa: (H|NK)|(n+1) = H|(n+1) by RELAT_1:74;
A81: (1+1)-'1 = 1 & n+2-'2 = n by NAT_D:34;
n+1 <= n+1+(k+4) by NAT_1:11;
then
A82: (H/^((1+1)-'1))|(n+1+1-'(1+1))=mid(H,1+1,n+1) by A70,AFINSQ_2:15
.= (H|(n+1))/^(1+1-'1) by AFINSQ_2:def 3;
Segm 1 c= Segm(n+1) by NAT_1:11,39;
then (H|(n+1)|1) = H|1 by RELAT_1:74
.= <%H.0%> by NUMERAL2:1;
then H|NK = <% x %>^X^Y by aa,A82,A81;
then ZY = <%Z%> ^ (<% x %>^(X^Y)) by AFINSQ_1:27
.= <%Z%> ^ <% x %>^(X^Y) by AFINSQ_1:27
.= <%Z,x%>^X^Y by AFINSQ_1:27;
then
A83: eval(p,@(<%Z,x%>^X^Y)),0 are_congruent_mod (1+(Z+1)*(K!)) by A69;
A84: for i be Nat st i in k holds
Product ((Y.i + 1)+(-idseq (x+1))),0 are_congruent_mod (1+(Z+1)*(K!))
proof
let i; assume
A85: i in k; then
Y.i = H.(n+1+i) by A76;
hence thesis by A85,A69;
end;
n+1 <= n+1+(k+4) by NAT_1:11;
then len (H|(n+1)) = n+1 by AFINSQ_1:54,A74;
then reconsider F = H|(n+1) as n+1-element XFinSequence of NAT
by CARD_1:def 7;
0 < len F;
then
A86: F.0=H.0 by AFINSQ_1:66,FUNCT_1:47;
for z be Element of NAT st z <= F.0
ex y be k-element XFinSequence of NAT st
for X1 be n-element XFinSequence of NAT st X1=F/^1 holds
(for i st i in k holds y.i <=F.0)& eval(p,@(<%z,F.0%>^X1^y)) = 0
proof
let z be Element of NAT;
assume z<=F.0; then
consider y be k-element XFinSequence of NAT such that
A88: (for i st i in k holds y.i <=x) & eval(p,@(<%z,x%>^X^y)) = 0
by A86,A84,Th17,A69,A78,A83;
take y;
let X1 be n-element XFinSequence of NAT;
assume X1=F/^1;
hence thesis by A88,A86,A82,A81;
end;
hence thesis by A68,A67;
end;
then
A89: X1 =X2 by TARSKI:2;
set Y1 = {X/^1 where X is n+1-element XFinSequence of NAT: X in X1};
A90: Y1 is diophantine Subset of n -xtuples_of NAT by HILB10_4:27,A89,A34;
for s be object holds s in Y1 iff s in X0
proof let s be object;
thus s in Y1 implies s in X0
proof
assume s in Y1;
then consider xS be (n+1)-element XFinSequence of NAT such that
A91: s=xS/^1 & xS in X1;
A92: ex w be (n+1)-element XFinSequence of NAT st xS = w & S[w] by A91;
len xS=n+1 by CARD_1:def 7;
then len (xS/^1)=n+1-'1 by AFINSQ_2:def 2;
then reconsider S=xS/^1 as n-element XFinSequence of NAT
by NAT_D:34,CARD_1:def 7;
ex x be Element of NAT st for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
(for i st i in k holds y.i <= x) &
eval(p,@(<%z,x%>^S^y)) = 0
proof
take x=xS.0;
let z be Element of NAT such that
A93: z <= x;
consider y be k-element XFinSequence of NAT such that
A94: for X1 be n-element XFinSequence of NAT st X1=xS/^1 holds
(for i st i in k holds y.i <= x)& eval(p,@(<%z,xS.0%>^X1^y)) = 0
by A92,A93;
take y;
S = xS/^1;
hence thesis by A94;
end;
hence thesis by A91;
end;
assume s in X0;
then consider S be n-element XFinSequence of NAT such that
A95: s=S & ex x be Element of NAT st for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
(for i st i in k holds y.i <= x) & eval(p,@(<%z,x%>^S^y)) = 0;
consider x be Element of NAT such that
A96: for z be Element of NAT st z <= x
ex y be k-element XFinSequence of NAT st
(for i st i in k holds y.i <= x)& eval(p,@(<%z,x%>^S^y)) = 0 by A95;
set xS = <%x%>^S;
len <%x%> =1 by CARD_1:def 7;
then
A97: xS/^1 =S by AFINSQ_2:12;
S[xS]
proof
let z be Element of NAT such that
A98: z <= xS.0;
xS.0 = x by AFINSQ_1:35;
then consider y be k-element XFinSequence of NAT such that
A99: (for i st i in k holds y.i <= xS.0) & eval(p,@(<%z,x%>^S^y)) = 0
by A96,A98;
take y;
thus thesis by A97,AFINSQ_1:35,A99;
end;
then xS in X1;
hence s in Y1 by A97,A95;
end;
hence thesis by A90,TARSKI:2;
end;
::$N Davis Normal Form
definition
let n be Nat;
let A be Subset of n -xtuples_of NAT;
attr A is recursively_enumerable means
ex m being Nat, P being INT -valued Polynomial of 2+n+m,F_Real st
for X being n -element XFinSequence of NAT holds
X in A
iff
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex Y being m-element XFinSequence of NAT st
(for i being object st i in dom Y holds Y.i <= x) &
eval(P,@(<%z,x%>^X^Y)) = 0;
end;
theorem
for n being Nat
for A being Subset of n -xtuples_of NAT holds
A is diophantine implies A is recursively_enumerable
proof
let n be Nat;
let A be Subset of n -xtuples_of NAT;
assume A is diophantine;
then consider m being Nat, P being INT -valued Polynomial of n+m,F_Real
such that
A1: for s be object holds
s in A iff ex x being n-element XFinSequence of NAT,
y being m-element XFinSequence of NAT st
s = x & eval(P,@(x^y)) = 0 by HILB10_2:def 6;
set nm=n+m;
reconsider P0=P as INT -valued Polynomial of 0+nm,F_Real;
consider q be Polynomial of 0+2+nm,F_Real such that
A2: rng q c= rng P0 \/{0.F_Real} and
A3: for XY being Function of 0+nm,F_Real,
XanyY being Function of 0+2+nm,F_Real st
XY|0 = XanyY|0 & @XY/^0 = @XanyY/^(0+2) holds eval(P0,XY) = eval(q,XanyY)
by HILB10_2:28;
A4: rng P0 c= INT by RELAT_1:def 19;
0.F_Real in INT by INT_1:def 1;
then {0.F_Real} c= INT by ZFMISC_1:31;
then rng P0 \/ {0.F_Real} c= INT by A4,XBOOLE_1:8;
then reconsider Q=q as INT-valued Polynomial of 2+n+m,F_Real
by RELAT_1:def 19,A2,XBOOLE_1:1;
take m,Q;
let X be n -element XFinSequence of NAT;
reconsider S = <*>INT as 0-element XFinSequence of NAT;
thus X in A implies
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex Y being m-element XFinSequence of NAT st
(for i be object st i in dom Y holds Y.i <= x) &
eval(Q,@(<%z,x%>^X^Y)) = 0
proof
assume X in A;
then consider x be n-element XFinSequence of NAT,
y be m-element XFinSequence of NAT such that
A5: X = x & eval(P,@(x^y)) = 0 by A1;
reconsider R = (rng y) \/{0} as finite non empty natural-membered set;
reconsider a=max R as Element of NAT by ORDINAL1:def 12;
take a;
let b be Element of NAT such that b <= a;
take y;
thus for i be object st i in dom y holds y.i <= a
proof
let i be object;
assume i in dom y;
then y.i in rng y by FUNCT_1:def 3;
then y.i in R by XBOOLE_0:def 3;
hence thesis by XXREAL_2:def 8;
end;
reconsider A=@(S^(x^y)) as Function of 0+nm,F_Real;
reconsider B=@(S^<%b,a%>^(x^y)) as Function of 0+2+nm,F_Real;
reconsider R = (rng y) \/{0} as finite ext-real-membered set;
A6: A|0 = {}= B|0;
A7: @A/^0 = @A=A = S^(x^y) by AFINSQ_2:10,HILB10_2:def 1,def 2;
@B=B by HILB10_2:def 2;
then
A8: @B = (S^<%b,a%>^(x^y)) by HILB10_2:def 1;
len (S^<%b,a%>) = 0+2 by CARD_1:def 7;
then
A9: @A/^0 = @B/^(0+2) by A7,A8,AFINSQ_2:12;
B= @(<%b,a%>^x^y) by AFINSQ_1:27;
hence thesis by A5,A3,A6,A9;
end;
given a be Element of NAT such that
A10: for z being Element of NAT st z <= a
ex y being m-element XFinSequence of NAT st
(for i be object st i in dom y holds y.i <= a) &
eval(Q,@(<%z,a%>^X^y)) = 0;
consider y be m-element XFinSequence of NAT such that
A11: (for i be object st i in dom y holds y.i <= a) &
eval(Q,@(<%a,a%>^X^y)) = 0 by A10;
reconsider C=@(S^(X^y)) as Function of 0+nm,F_Real;
reconsider B=@(S^<%a,a%>^(X^y)) as Function of 0+2+nm,F_Real;
A12: C|0 = {}= B|0;
A13: @C/^0 = @C=C = S^(X^y) by AFINSQ_2:10,HILB10_2:def 1,def 2;
@B=B by HILB10_2:def 2;
then
A14: @B = (S^<%a,a%>^(X^y)) by HILB10_2:def 1;
len (S^<%a,a%>) = 0+2 by CARD_1:def 7;
then
A15: @C/^0 = @B/^(0+2) by A13,A14,AFINSQ_2:12;
A16: B= @(<%a,a%>^X^y) by AFINSQ_1:27;
eval(P,@(X^y)) =0 by A11,A16,A3,A12,A15;
hence thesis by A1;
end;
begin :: MRDP Theorem
::$N Yuri Matiyasevich, Julia Robinson, Martin Davis, Hilary Putnam Theorem
theorem
for n being Nat
for A being Subset of n -xtuples_of NAT holds
A is recursively_enumerable implies A is diophantine
proof
let n be Nat;
let A be Subset of n -xtuples_of NAT;
assume A is recursively_enumerable;
then consider m be Nat, P be INT -valued Polynomial of 2+n+m,F_Real
such that
A1: for X being n -element XFinSequence of NAT holds X in A iff
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex Y being m-element XFinSequence of NAT st
(for i be object st i in dom Y holds Y.i <= x) &
eval(P,@(<%z,x%>^X^Y)) = 0;
set X = {X where X is n-element XFinSequence of NAT:
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex Y being m-element XFinSequence of NAT st
(for i being Nat st i in m holds Y.i <= x) &
eval(P,@(<%z,x%>^X^Y)) = 0};
A2: A c= X
proof
let a be object such that
A3: a in A;
reconsider a as n-element XFinSequence of NAT by A3,HILB10_2:def 5;
consider x be Element of NAT such that
A4: for z be Element of NAT st z <= x
ex Y being m-element XFinSequence of NAT st
(for i be object st i in dom Y holds Y.i <= x) &
eval(P,@(<%z,x%>^a^Y)) = 0 by A3,A1;
now let z be Element of NAT such that
A5: z <= x;
consider Y be m-element XFinSequence of NAT such that
A6: (for i be object st i in dom Y holds Y.i <= x) &
eval(P,@(<%z,x%>^a^Y)) = 0 by A4,A5;
take Y;
len Y=m by CARD_1:def 7;
hence (for i being Nat st i in m holds Y.i <= x)
& eval(P,@(<%z,x%>^a^Y)) = 0 by A6;
end;
hence thesis;
end;
X c= A
proof
let b be object such that
A7: b in X;
consider X be n-element XFinSequence of NAT such that
A8: b=X &
ex x being Element of NAT st
for z being Element of NAT st z <= x
ex Y being m-element XFinSequence of NAT st
(for i being Nat st i in m holds Y.i <= x) &
eval(P,@(<%z,x%>^X^Y)) = 0 by A7;
consider x be Element of NAT such that
A9: for z being Element of NAT st z <= x
ex Y being m-element XFinSequence of NAT st
(for i being Nat st i in m holds Y.i <= x) &
eval(P,@(<%z,x%>^X^Y)) = 0 by A8;
now let z be Element of NAT such that A10: z <= x;
consider Y being m-element XFinSequence of NAT such that
A11: (for i being Nat st i in m holds Y.i <= x) &
eval(P,@(<%z,x%>^X^Y)) = 0 by A9,A10;
take Y;
m=len Y by CARD_1:def 7;
hence (for i be object st i in dom Y holds Y.i <= x) &
eval(P,@(<%z,x%>^X^Y)) = 0 by A11;
end;
hence thesis by A1,A8;
end;
then X=A by A2,XBOOLE_0:def 10;
hence thesis by Th19;
end;