:: Diophantine Sets -- Preliminaries :: by Karol P\kak :: :: Received May 27, 2019 :: Copyright (c) 2019 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, QC_LANG1, VECTSP_1, POLYNOM1, POLYNOM2, AFINSQ_1, NEWTON, HILB10_2, INT_2, PARTFUN3, REAL_1, XCMPLX_0, VALUED_0, FINSEQ_2, CARD_3, REALSET1, BINOP_2, FINSOP_1, FUNCOP_1, XREAL_0, RFINSEQ, BINOP_1, FUNCT_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, XCMPLX_0, PARTFUN1, FUNCT_2, BINOP_1, NAT_1, FINSEQ_1, FUNCOP_1, VECTSP_1, XXREAL_0, RECDEF_1, POLYNOM1, XREAL_0, INT_1, POLYNOM2, AFINSQ_1, AFINSQ_2, NEWTON, HILB10_2, VALUED_0, FINSEQ_2, RVSUM_1, VALUED_1, BINOP_2, PARTFUN3, CARD_1, NAT_D, RVSUM_4; constructors NAT_D, RECDEF_1, BINOP_2, RELSET_1, GROUP_4, POLYNOM2, AFINSQ_2, NEWTON, HILB10_2, WSIERP_1, INT_6, SETWISEO, RVSUM_4; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, CARD_1, VALUED_0, VALUED_1, RELSET_1, INT_1, STRUCT_0, VECTSP_1, MEMBERED, AFINSQ_1, HILB10_2, XXREAL_0, NUMBERS, XCMPLX_0, NEWTON, NEWTON02, NAT_6, FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON04, MOEBIUS2, EUCLID_9, AFINSQ_2, PARTFUN3, BINOP_2, FUNCT_2, RFUNCT_2, RVSUM_4; requirements NUMERALS, SUBSET, ARITHM, REAL; definitions TARSKI, PARTFUN3; equalities FINSEQ_1, VALUED_1, ORDINAL1, AFINSQ_2; expansions FUNCT_2, CARD_1; theorems TARSKI, FUNCT_1, CARD_1, NAT_1, XREAL_1, XXREAL_0, NEWTON, INT_1, FINSEQ_3, FINSEQ_1, XCMPLX_1, XREAL_0, NEWTON02, RVSUM_1, FINSEQ_5, VALUED_0, FINSEQ_2, VALUED_1, IRRAT_1, INT_4, EULER_1, INT_2, NAT_D, ORDINAL1, WSIERP_1, PREPOWER, HILB10_2, HILB10_3, BASEL_1, NEWTON04, NAT_6, AFINSQ_1, XBOOLE_0, CATALAN2, RELAT_1, FUNCT_2, XBOOLE_1, BINOP_2, MEMBERED, PARTFUN3, AFINSQ_2, XCMPLX_0, CARD_FIN; schemes NAT_1, FINSEQ_1, HILB10_3; begin :: Product of zero based finite sequences reserve i,j,n,n1,n2,m,k,l,u for Nat, r,r1,r2 for Real, x,y for Integer, a,b for non trivial Nat, F for XFinSequence, cF,cF1,cF2 for complex-valued XFinSequence, c,c1,c2 for Complex; registration let c1,c2; cluster <%c1,c2%> -> complex-valued; coherence proof c1 in COMPLEX & c2 in COMPLEX by XCMPLX_0:def 2; hence thesis; end; end; definition let cF be XFinSequence; ::: same as XProduct from RVSUM_4 func Product cF -> Element of COMPLEX equals multcomplex "**" cF; coherence; end; theorem Th1: cF is real-valued implies Product cF = multreal "**" cF proof assume A1: cF is real-valued; per cases by NAT_1:14; suppose A2: len cF=0; hence multreal "**" cF = the_unity_wrt multcomplex by BINOP_2:6,7,AFINSQ_2:def 8,A1 .= Product cF by AFINSQ_2:def 8,A2; end; suppose A3: len cF>=1; A4: REAL = REAL /\ COMPLEX by MEMBERED:1,XBOOLE_1:28; now let x,y be object; assume x in REAL & y in REAL; then reconsider X=x,Y=y as Element of REAL; multreal.(x,y) = X*Y by BINOP_2:def 11; hence multreal.(x,y) =multcomplex.(x,y) & multreal.(x,y) in REAL by BINOP_2:def 5,XREAL_0:def 1; end; hence thesis by AFINSQ_2:47,A3,A4,A1; end; end; theorem cF is INT-valued implies Product cF = multint "**" cF proof assume A1: cF is INT-valued; per cases by NAT_1:14; suppose A2: len cF=0; hence multint "**" cF = the_unity_wrt multcomplex by BINOP_2:6,9,AFINSQ_2:def 8,A1 .= Product cF by AFINSQ_2:def 8,A2; end; suppose A3: len cF>=1; A4: INT = INT /\ COMPLEX by MEMBERED:1,XBOOLE_1:28; now let x,y be object; assume x in INT & y in INT; then reconsider X=x,Y=y as Element of INT; multint.(x,y) = X*Y by BINOP_2:def 22; hence multint.(x,y) = multcomplex.(x,y) & multint.(x,y) in INT by BINOP_2:def 5,INT_1:def 2; end; hence thesis by AFINSQ_2:47,A3,A4,A1; end; end; theorem Th3: cF is natural-valued implies Product cF = multnat "**" cF proof assume cF is natural-valued; then rng cF c= NAT by VALUED_0:def 6; then A1: cF is NAT-valued by RELAT_1:def 19; per cases by NAT_1:14; suppose A2: len cF=0; hence multnat "**" cF = the_unity_wrt multcomplex by BINOP_2:6,10,AFINSQ_2:def 8,A1 .= Product cF by AFINSQ_2:def 8,A2; end; suppose A3: len cF>=1; A4: NAT = NAT /\ COMPLEX by MEMBERED:1,XBOOLE_1:28; now let x,y be object; assume x in NAT & y in NAT; then reconsider X=x,Y=y as Element of NAT; multnat.(x,y) = X*Y by BINOP_2:def 24; hence multnat.(x,y) =multcomplex.(x,y) & multnat.(x,y) in NAT by BINOP_2:def 5,ORDINAL1:def 12; end; hence thesis by AFINSQ_2:47,A3,A4,A1; end; end; registration let F be real-valued XFinSequence; cluster Product F -> real; coherence proof Product F = multreal "**" F by Th1; hence thesis; end; end; registration let F be natural-valued XFinSequence; cluster Product F -> natural; coherence proof Product F = multnat "**" F by Th3; hence thesis; end; end; theorem Th4: cF = {} implies Product cF = 1 proof assume cF={}; then len cF = 0; hence thesis by BINOP_2:6,AFINSQ_2:def 8; end; theorem Th5: Product <%c%> = c proof c in COMPLEX by XCMPLX_0:def 2; hence thesis by AFINSQ_2:37; end; theorem Product <%c1,c2%> = c1 * c2 proof c1 in COMPLEX & c2 in COMPLEX by XCMPLX_0:def 2; then multcomplex "**" <%c1,c2%> = multcomplex.(c1,c2) by AFINSQ_2:38 .= c1*c2 by BINOP_2:def 5; hence thesis; end; theorem Th7: Product(cF1^cF2) = Product(cF1) * Product(cF2) proof thus Product(cF1^cF2)=multcomplex.(Product cF1,Product cF2) by AFINSQ_2:42 .= Product(cF1)*Product(cF2) by BINOP_2:def 5; end; theorem Th8: c+ (cF1^cF2) = (c+cF1) ^ (c+cF2) proof A1: dom (c+cF1) =dom cF1 & dom (c+cF2) =dom cF2 & dom (c+ (cF1^cF2)) = dom (cF1^cF2) by VALUED_1:def 2; A2: len (cF1^cF2) = len cF1+len cF2 & len ((c+cF1)^(c+cF2)) = len (c+cF1)+len (c+cF2) by AFINSQ_1:17; for x be object st x in dom (c+ (cF1^cF2)) holds (c+ (cF1^cF2)).x = ((c+cF1) ^ (c+cF2)).x proof let x be object; assume A3: x in dom (c+ (cF1^cF2)); then reconsider i=x as Nat; per cases by A3,A1,AFINSQ_1:20; suppose A4: i in dom cF1; then A5: (cF1^cF2).i = cF1.i & ((c+cF1) ^ (c+cF2)).i = (c+cF1).i by A1,AFINSQ_1:def 3; hence (c+ (cF1^cF2)).x = c+ (cF1.i) by A3,VALUED_1:def 2 .= ((c+cF1)^(c+cF2)).x by A5,A4,A1,VALUED_1:def 2; end; suppose ex n st n in dom cF2 & i= len cF1 +n; then consider n such that A6: n in dom cF2 & i= len cF1 +n; A7: (cF1^cF2).i = cF2.n & ((c+cF1) ^ (c+cF2)).i = (c+cF2).n by A1,A6,AFINSQ_1:def 3; hence (c+ (cF1^cF2)).x = c +(cF2.n) by A3,VALUED_1:def 2 .= ((c+cF1) ^ (c+cF2)).x by A1,A6,A7,VALUED_1:def 2; end; end; hence thesis by A1,A2,FUNCT_1:2; end; theorem Th9: c1 + <%c2%> = <%c1 + c2%> proof A1: dom <%c1 + c2%> = 1 = dom <%c2%> = dom (c1 + <%c2%>) by VALUED_1:def 2,AFINSQ_1:def 4; <%c1 + c2%>.0 = c1+(<%c2%>.0) .= (c1 + <%c2%>).0 by A1,AFINSQ_1:66,VALUED_1:def 2; hence thesis by A1,AFINSQ_1:def 4; end; theorem Th10: for f1,f2 be XFinSequence,n st n <= len f1 holds (f1^f2)/^n = (f1/^n)^f2 proof let f1,f2 be XFinSequence,n; assume n <= len f1; then A2: len (f1|n) = n by AFINSQ_1:54; f1 = (f1|n)^ (f1/^n); then f1^f2 = (f1|n)^ ((f1/^n)^f2) by AFINSQ_1:27; hence (f1^f2)/^n = ((f1/^n)^f2) by A2,AFINSQ_2:12; end; registration let n; cluster n-element natural-valued for XFinSequence; existence proof take the n-element XFinSequence of NAT; thus thesis; end; end; registration cluster natural-valued positive-yielding for XFinSequence; existence proof take Segm the Nat --> 1; thus thesis; end; end; registration let R be positive-yielding Relation; let X be set; cluster R|X -> positive-yielding; coherence proof A1: rng (R|X) c= rng R by RELAT_1:70; let r be Real; assume r in rng (R|X); hence thesis by A1,PARTFUN3:def 1; end; end; registration let X be positive-yielding real-valued XFinSequence; cluster Product X -> positive; coherence proof defpred P[Nat] means for X be positive-yielding real-valued XFinSequence st len X=\$1 holds Product X is positive; A1: P[0] proof let X be positive-yielding real-valued XFinSequence;assume len X=0; then X={}; hence thesis by Th4; end; A2: P[n] implies P[n+1] proof set n1=n+1; assume A3: P[n]; let X be positive-yielding real-valued XFinSequence; set XX=<%X.n%>; assume A4: len X=n1; then X=(X|n) ^ <%X.n%> by AFINSQ_1:56; then A5: Product X = Product (X|n) * Product XX by Th7 .= Product (X|n) * X.n by Th5; n < n1 by NAT_1:13; then n in dom X & len (X|n) = n by A4,AFINSQ_1:54,66; then A6: Product (X|n) >0 & X.n in rng X by A3,FUNCT_1:def 3; then X.n >0 by PARTFUN3:def 1; hence Product X is positive by A5,A6; end; P[n] from NAT_1:sch 2(A1,A2); then P[len X]; hence thesis; end; end; theorem for X being natural-valued positive-yielding XFinSequence st i in dom X holds X.i <= Product X proof defpred P[Nat] means for X be natural-valued positive-yielding XFinSequence, i be Nat st len X=\$1 & i in dom X holds X.i <= Product X; A1: P[0] by XBOOLE_0:def 1; A2: P[n] implies P[n+1] proof set n1=n+1; assume A3: P[n]; let X be positive-yielding natural-valued XFinSequence, i be Nat; assume A4: len X=n1 & i in dom X; then X=(X|n) ^ <%X.n%> by AFINSQ_1:56; then A5: Product X = Product (X|n) * Product <%X.n%> by Th7 .= Product (X|n) * X.n by Th5; A6: n < n1 by NAT_1:13; then A7: n in dom X & len (X|n) = n by A4,AFINSQ_1:54,66; then Product (X|n) > 0 & X.n in rng X by FUNCT_1:def 3; then A8: X.n >0 & Product (X|n) >=1 by PARTFUN3:def 1,NAT_1:14; then A9: X.n >=1 by NAT_1:14; i < len X by A4,AFINSQ_1:66; then i <=n by A4,NAT_1:13; then per cases by XXREAL_0:1; suppose i =n; then Product X >= X.i*1 by A5,A8,XREAL_1:66; hence thesis; end; suppose A10: i= (X|n).i by A3,A7,AFINSQ_1:66,A10; then Product X >= ((X|n).i)*1 & (X|n).i = X.i by A6,A4,AFINSQ_1:53,A11,A7,A5,A9,XREAL_1:66; hence thesis; end; end; A12: P[n] from NAT_1:sch 2(A1,A2); let X be natural-valued positive-yielding XFinSequence; thus thesis by A12; end; registration let X be natural-valued XFinSequence,n be positive Nat; cluster n + X -> positive-yielding; coherence proof now let r be Real; assume r in rng (n+X); then consider x be object such that A1: x in dom (n+X) & (n+X).x=r by FUNCT_1:def 3; (n+X).x = n+(X.x) by A1,VALUED_1:def 2; hence r>0 by A1; end; hence thesis by PARTFUN3:def 1; end; end; theorem for X1,X2 being natural-valued XFinSequence st len X1=len X2 & for n st n in dom X1 holds X1.n <= X2.n holds Product X1 <= Product X2 proof defpred P[Nat] means for X1,X2 be natural-valued XFinSequence st len X1=\$1 =len X2 & for n st n in dom X1 holds X1.n <= X2.n holds Product X1 <= Product X2; A1: P[0] proof let X1,X2 be natural-valued XFinSequence;assume len X1=0 =len X2; then X1={}=X2; hence thesis; end; A2: P[n] implies P[n+1] proof set n1=n+1; assume A3: P[n]; let X1,X2 be natural-valued XFinSequence; assume that A4: len X1=n1=len X2 and A5: for i st i in dom X1 holds X1.i <= X2.i; X1=(X1|n) ^ <%X1.n%> by A4,AFINSQ_1:56; then A6: Product X1 = Product (X1|n) * Product <%X1.n%> by Th7 .= Product (X1|n) * X1.n by Th5; X2=(X2|n) ^ <%X2.n%> by A4,AFINSQ_1:56; then A7: Product X2 = Product (X2|n) * Product <%X2.n%> by Th7 .= Product (X2|n) * X2.n by Th5; A8: n < n1 by NAT_1:13; then A9: n in dom X1 & len (X1|n) = n = len (X2|n) by A4,AFINSQ_1:54,66; A10: X1.n <= X2.n by A5,A8,A4,AFINSQ_1:66; for i st i in dom (X1|n) holds (X1|n).i <= (X2|n).i proof let i; assume i in dom (X1|n); then (X1|n).i =X1.i & (X2|n).i =X2.i & i in dom X1 by A8,A4,A9,AFINSQ_1:53; hence thesis by A5; end; then Product (X1|n) <= Product (X2|n) by A3,A9; hence thesis by A6,A7,A10,XREAL_1:66; end; P[n] from NAT_1:sch 2(A1,A2); hence thesis; end; begin :: Binomial is Diophantin theorem Th13: k <= n implies n choose k <= n|^k proof defpred P[Nat] means \$1 <= n implies n choose \$1 <= n|^\$1; n choose 0 = 1 by NEWTON:19; then A1: P[0] by NEWTON:4; A2: P[m] implies P[m+1] proof assume A3: P[m]; set m1=m+1; assume A4: m1<=n; then m m-m by XREAL_1:14; A6: n-m <= n-0 by XREAL_1:10; A7: n choose m1 = ((n-m)/m1) * (n choose m) by IRRAT_1:5; (n-m)/m1 <= (n-m)/1 by A5, XREAL_1:118,NAT_1:11; then (n-m)/m1 <= n by A6,XXREAL_0:2; then A8: n choose m1 <= n * (n choose m) by A7,XREAL_1:64; n * (n choose m) <= n * (n|^m) by A3,A4,NAT_1:13,XREAL_1:64; then n choose m1 <= n * (n|^m) by A8,XXREAL_0:2; hence thesis by NEWTON:6; end; P[m] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem Th14: u > n|^k & n >= k & k > i implies (n choose i)*(u |^i) < (u|^k)/n proof assume A1: u > n|^k & n >= k & k > i; then A2: k>=i+1 by NAT_1:13; A3: u >=1 by A1,NAT_1:14; A4: n >0 by A1; then n >=1 by NAT_1:14; then n|^(i+1) <= n|^k by A2,PREPOWER:93; then n|^(i+1) < u by A1,XXREAL_0:2; then A5: n|^(i+1) * u|^i < u * (u|^i) by XREAL_1:68; u*(u|^i) = u|^(i+1) by NEWTON:6; then u*(u|^i) <= u |^k by A3,A2,PREPOWER:93; then n|^(i+1) * u|^i < u|^k & n|^(i+1) = n*n|^i by A5,XXREAL_0:2,NEWTON:6; then n*(n|^i * u|^i) < u|^k; then A6: n|^i * (u|^i)< (u|^k) / n by A4, XREAL_1:81; i <= n by A1,XXREAL_0:2; then n choose i <= n|^i by Th13; then (n choose i) * (u|^i) <= (n|^i)* (u|^i) by XREAL_1:64; hence thesis by A6,XXREAL_0:2; end; theorem Th15: u > n|^k & n >= k implies [\ ((u+1)|^n) / (u|^k) /] mod u = n choose k proof assume A1: u > n|^k & n >= k; set I = (1,u) In_Power n,k1=k+1; consider q be FinSequence such that A2: I = (I|k1) ^ q by FINSEQ_1:80; rng I c= NAT by VALUED_0:def 6; then reconsider I1=I as FinSequence of NAT by FINSEQ_1:def 4; I1 = (I1|k1)^q by A2; then reconsider q as FinSequence of NAT by FINSEQ_1:36; A3:len I1 = n+1 by NEWTON:def 4; A4:len (I1|k1)=k1 by A1,XREAL_1:7,A3,FINSEQ_1:59; 1<= k1 by NAT_1:11; then k1 in dom I by A3,A1,XREAL_1:7,FINSEQ_3:25; then A5: I1|k1 = (I1|k) ^ <* I1.k1*> by FINSEQ_5:10; A6: Sum I1 = Sum (I1|k1) + Sum q by A2,RVSUM_1:75 .= Sum (I1|k) + (I1.k1) + Sum q by A5,RVSUM_1:74; k <= n+1 by A1,NAT_1:13; then A7: I1|k is k -element by A3,FINSEQ_1:59; set kI = k |-> ((u|^k)/n); A8:for i be Nat st i in Seg k holds (I1|k).i < kI.i proof let i be Nat such that A9:i in Seg k; A10: kI.i = (u|^k)/n by A9,FINSEQ_2:57; A11: 1<=i<=k by A9,FINSEQ_1:1; then A12: (I1|k).i = I1.i by FINSEQ_3:112; reconsider i1=i-1 as Nat by A11; set ni = n-'i1; A13: i1+1=i & i <= n by A11,A1,XXREAL_0:2; then A14:i1 < n & i <= n+1 by NAT_1:13; then A15: i in dom I1 by A11,A3,FINSEQ_3:25; ni = n-i1 by A14,XREAL_1:233; then A16: I1.i = (n choose i1)*(1|^ni) * (u|^i1) by A15,NEWTON:def 4; k>i1 by A13,A11,NAT_1:13; hence thesis by Th14,A1,A10,A16,A12; end; then A17:for i be Nat st i in Seg k holds (I1|k).i <= kI.i; 1<=k1 by NAT_1:11; then A18: k1 in dom I1 by A1,XREAL_1:7,A3,FINSEQ_3:25; n-k = n-'k & k=k1-1 by A1,XREAL_1:233; then A19: I1.k1 = (n choose k) * (1|^(n-'k))*(u|^k) by A18,NEWTON:def 4; defpred P[Nat,object] means \$2 in NAT & for i be Nat st i=\$2 holds q.\$1 = (u|^k)*u*i; len I = k1+len q by A2,A4,FINSEQ_1:22; then A20: n=k+len q by A3; A21:for j be Nat st j in Seg len q ex x be object st P[j,x] proof let j be Nat such that A22: j in Seg len q; A23: 1<=j <= len q by FINSEQ_1:1,A22; A24: k1+j-1 = k+j; A25: n>=k+j by A23,A20,XREAL_1:7; A26: n-'(k+j) = n-(k+j) by XREAL_1:233,A23,A20,XREAL_1:7; 1<= k+j+1<= n+1 by NAT_1:11,A25,XREAL_1:7; then k1+j in dom I1 by FINSEQ_3:25,A3; then A27: I1.(k1+j) = (n choose (k+j)) * (1|^(n-'(k+j)))*(u|^(k+j)) by A24,A26,NEWTON:def 4; reconsider j1=j-1 as Nat by A23; A28: u|^(k+j) = (u|^k)*(u|^(j1+1)) by NEWTON:8 .= (u|^k)*((u|^j1)*u) by NEWTON:6; take U=(n choose (k+j)) * (1|^(n-'(k+j)))* u|^j1; thus thesis by A27,A28,A23,FINSEQ_1:65,A2,A4,ORDINAL1:def 12; end; consider Q be FinSequence such that A29: dom Q=Seg len q and A30: for j be Nat st j in Seg len q holds P[j,Q . j] from FINSEQ_1:sch 1(A21); rng Q c= NAT proof let y be object such that A31: y in rng Q; ex x be object st x in dom Q & Q . x=y by FUNCT_1:def 3,A31; hence thesis by A30,A29; end; then reconsider Q as FinSequence of NAT by FINSEQ_1:def 4; A32: len Q=len q & len (((u|^k)*u)*Q)=len Q by CARD_1:def 7,A29,FINSEQ_1:def 3; for i be Nat st 1<= i <= len q holds q.i=(((u|^k)*u)*Q).i proof let i be Nat;assume 1<= i <= len q; then i in dom Q by A29; then q.i = (u|^k)*u*(Q.i) by A29,A30; hence thesis by VALUED_1:6; end; then q=((u|^k)*u)*Q by A32,FINSEQ_1:14; then A33: Sum q = (u|^k)*u*Sum Q by RVSUM_1:87; A34: [\ (Sum I1) / (u|^k) /] = (n choose k) + u*Sum Q proof per cases by NAT_1:14; suppose k=0; then Sum(I1|k)=0 by RVSUM_1:72; then 1* Sum I1= (u|^k) *((n choose k)+u*Sum Q) by A33,A19,A6; then (Sum I1)/(u|^k) = ((n choose k)+u*Sum Q)/1 by A1,XCMPLX_1:94; hence thesis by INT_1:25; end; suppose A35: k >=1; then A36: k in Seg k; then A37: (I1|k).k < kI.k by A8; A38: Sum kI = k*((u|^k)/n) by RVSUM_1:80 .= (u|^k)* (k/n) by XCMPLX_1:75; Sum (I1|k) < (u|^k)* (k/n) by A37,A36,A7,A17,RVSUM_1:83,A38; then A39: Sum (I1|k)+((I1.k1)+Sum q) < (u|^k)* (k/n) + ((I1.k1)+Sum q) by XREAL_1:8; (u|^k)* (k/n) + ((I1.k1)+Sum q) = (u|^k)*((k/n)+ (n choose k) + u*Sum Q) by A33,A19; then A40: (Sum I1) / (u|^k)< ((k/n)+ (n choose k) + u*Sum Q) by A1,A39,A6,XREAL_1:83; k/n <=n/n & n/n = 1 by A35,XREAL_1:72,A1,XCMPLX_1:60; then (k/n)+ ((n choose k) + u*Sum Q) <=1 +((n choose k) + u*Sum Q) by XREAL_1:7; then (Sum I1) / (u|^k) < 1 +((n choose k) + u*Sum Q) by A40,XXREAL_0:2; then A41: (Sum I1) / (u|^k) -1 < (n choose k) + u*Sum Q by XREAL_1:19; A42: 0 +((I1.k1)+Sum q) <= Sum (I1|k)+((I1.k1)+Sum q) by XREAL_1:7; (I1.k1)+Sum q = (u|^k)*((n choose k) + u*Sum Q) by A33,A19; then (Sum I1) / (u|^k) >= (n choose k) + u*Sum Q by A1,A42,A6,XREAL_1:77; hence thesis by A41,INT_1:def 6; end; end; A43: Sum I1 = (1+u)|^n by NEWTON:30; n choose k <= n|^k by Th13,A1; then n choose k < u by A1,XXREAL_0:2; then (n choose k) mod u = n choose k by NAT_D:24; hence thesis by A34,A43,NAT_D:21; end; theorem Th16: for x,y,z being Nat holds x >= z & y = x choose z iff ex u,v,y1,y2,y3 being Nat st y1 = x|^z & y2 = (u+1)|^x & y3 = u|^z & u > y1 & v = [\y2/y3/] & y,v are_congruent_mod u & y < u & x >=z proof let x,y,z be Nat; thus x>=z & y = x choose z implies ex u,v,y1,y2,y3 be Nat st y1 = x|^z & y2 = (u+1)|^x & y3 = u|^z & u > y1 & v = [\y2/y3/] & y,v are_congruent_mod u & y < u & x >=z proof assume A1: x>=z & y = x choose z; set y1 =x|^z, u = y1+1,y2 = (u+1)|^x,y3=u|^z,v=[\y2/y3/]; reconsider v as Element of NAT by INT_1:3,INT_1:54; take u,v,y1,y2,y3; thus A2: y1 = x|^z & y2 = (u+1)|^x & y3 = u|^z & u > y1 & v = [\y2/y3/] by NAT_1:13; A3: v mod u = y by A2,Th15,A1; y < u by A1,NAT_1:13,Th13; then y mod u = y by NAT_D:24; then y-v mod u = 0 by A3,INT_4:22; then u divides y-v by INT_1:62; hence thesis by A1,NAT_1:13,Th13,INT_1:def 4; end; given u,v,y1,y2,y3 be Nat such that A4: y1 = x|^z & y2 = (u+1)|^x & y3 = u|^z and A5: u > y1 & v = [\y2/y3/] & y,v are_congruent_mod u and A6: y < u & x >=z; u divides y-v by A5,INT_1:def 4; then y-v mod u =0 by INT_1:62,A5; then y mod u = v mod u by INT_4:22,A5; then y mod u = x choose z by Th15,A4,A5,A6; hence thesis by A6,NAT_D:24; end; begin :: Factorial is Diophantin Lm1: k < n implies 1- k/n = (n-k)/n & 1/(1- k/n) = n / (n-k) proof assume k < n; then 1 -k/n = (n/n) - k/n by XCMPLX_1:60 .= (n-k)/n by XCMPLX_1:120; hence thesis by XCMPLX_1:57; end; Lm2: for n,k st k < n holds (n|^k) / (n choose k) <= k! * 1 / (1- k/n)|^k proof let n; defpred P[Nat] means \$1 < n implies (n|^\$1) / (n choose \$1) <= \$1! * 1 / (1- \$1/n)|^\$1; n|^0 =1 & n choose 0 =1 by NEWTON:4,19; then A1: P[0] by NEWTON:12; A2: for k st P[k] holds P[k+1] proof let k such that A3: P[k]; set k1=k+1; assume A4: k1 < n; A5: (n|^k1) / (n choose k1) = (n|^k1) / ((n-k)/(k+1)* (n choose k)) by IRRAT_1:5 .= (n|^k1) / (n choose k) / ((n-k)/k1) by XCMPLX_1:78 .= (n|^k1) / (n choose k)*(k1/(n-k)) by XCMPLX_1:79 .= (n* (n|^k)) / (n choose k)*(k1/(n-k)) by NEWTON:6 .= (n|^k) / (n choose k)*n*(k1/(n-k)) by XCMPLX_1:74 .= (n|^k) / (n choose k)*(n*(k1/(n-k))); k < n by A4,NAT_1:13; then A6: n-k > 0 & n-k1 >0 by XREAL_1:50,A4; k < k1 by NAT_1:13; then k/n < k1/n by A4,XREAL_1:74; then A7: 1- k/n > 1 - k1/n by XREAL_1:10; A8: 1-k1/n = (n-k1)/n by Lm1,A4; then A9: (1- k/n)|^k1 > (1-k1/n)|^k1 by NAT_1:11,A7,A6,PREPOWER:10; A10: k < n by A4,NAT_1:13; A11: (n|^k1) / (n choose k1) <= (k! * 1 / (1- k/n)|^k) * (n*(k1/(n-k))) by A3,A5,XREAL_1:64,A6,A4,NAT_1:13; A12: (1 / ( 1- k/n)|^k) * (n/(n-k)) = (1/(1- k/n)|^k) * (1 /(1-k/n)) by A10,Lm1 .= (1*1) /( ( 1- k/n)|^k *(1-k/n) ) by XCMPLX_1:76 .= 1 / (( 1- k/n)|^k1) by NEWTON:6; A13: (k! * 1 / ( 1- k/n)|^k) * (n*(k1/(n-k))) = (k! * 1 / ( 1- k/n)|^k) * (k1 * (n/(n-k))) by XCMPLX_1:75 .= k! * (1 / ( 1- k/n)|^k) * (k1 * (n/(n-k))) by XCMPLX_1:74 .= (k!*k1) * (1 / ( 1- k/n)|^k) * (n/(n-k)) .= k1! * (1 / (1- k/n)|^k) * (n/(n-k)) by NEWTON:15 .= k1! * (1 / ((1- k/n)|^k1)) by A12 .= (k1! * 1) / ((1- k/n)|^k1) by XCMPLX_1:74; (k1! * 1) / (( 1- k/n)|^k1) < (k1! * 1) / (( 1- k1/n)|^k1) by A8,A6,A4,A9,XREAL_1:76; hence thesis by A11,A13,XXREAL_0:2; end; for k holds P[k] from NAT_1:sch 2(A1,A2); hence thesis; end; Lm3: 0<2*k0 by XREAL_1:50; A4: k>0 by A1; n*k > 2*k*k by A4,A1,XREAL_1:68; then 0 < n*k - (2*k*k) by XREAL_1:50; then n*n +0 < n*n +(2*n*k - (k*n) - (2*k*k)) by XREAL_1:6; then n*n< (n+2*k)*(n-k); then A5: n/(n-k) < (n+2*k)/n by A1,A3,XREAL_1:106; (n+2*k)/n = n/n + (2*k)/n by XCMPLX_1:62 .= 1 +(2*k)/n by A1,XCMPLX_1:60; hence thesis by A5,A2,Lm1; end; Lm4: for n,k st k < n holds k! <= (n|^k) / (n choose k) proof let n; defpred P[Nat] means \$1 < n implies \$1! <= (n|^\$1) / (n choose \$1); n|^0 =1 & n choose 0 = 1 by NEWTON:4,19; then A1: P[0] by NEWTON:12; A2: for k st P[k] holds P[k+1] proof let k such that A3: P[k]; set k1=k+1; assume A4: k1 = n-k by XREAL_1:43; n-k >0 by A5,XREAL_1:50; then n/(n-k) >=1 by A7,XREAL_1:181; then A8: k1*(n/(n-k))>= k1*1 by XREAL_1:64; k1*(n/(n-k)) = n*k1 / (n-k) by XCMPLX_1:74 .= n*(k1/(n-k)) by XCMPLX_1:74; then (n|^k) / (n choose k)*(n*(k1/(n-k))) >= k! * k1 by A4,NAT_1:13,A3,A8,XREAL_1:66; hence thesis by A6,NEWTON:15; end; for k holds P[k] from NAT_1:sch 2(A1,A2); hence thesis; end; Lm5: 0< r < 1/2 implies (1+r)|^k < 1+r*(2|^k) proof assume A1: 0< r < 1/2; defpred P[Nat] means (1+r)|^\$1 < 1+r*(2|^\$1); per cases by NAT_1:14; suppose A2: k=0; (1+r)|^0=1 & 2|^0=1 & 1+0 <1+r by NEWTON:4,A1,XREAL_1:8; hence thesis by A2; end; suppose A3: k>=1; 1+r+0 < 1+r+r by A1,XREAL_1:8; then A4: P[1]; A5: for k st 1<= k holds P[k] implies P[k+1] proof let k such that A6: 1<=k and A7: P[k];set k1=k+1; 2|^k >= 2 by A6,PREPOWER:12; then A8: 2|^k*(1/2) >= 2*(1/2) by XREAL_1:64; r*(2|^k) < 1/2* (2|^k) by A1,XREAL_1:68; then 1+r*(2|^k) < 1/2 * (2|^k)+1/2* (2|^k) by A8,XREAL_1:8; then A9: (2|^k) +(1 +r*2|^k) < 2|^k+2|^k by XREAL_1:8; 2|^k1 = 2*(2|^k) by NEWTON:6; then r*((2|^k) +1 +r*2|^k) < r*(2|^k1) by A9,A1,XREAL_1:68; then A10: 1+r*((2|^k) +1 +r*2|^k) < 1+r*(2|^k1) by XREAL_1:8; A11: (1+r)|^k1 = (1+r)|^k * (1+r) by NEWTON:6; (1+r)|^k1 < (1+r*(2|^k))*(1+r) by A7,A1,A11,XREAL_1:68; hence thesis by A10,XXREAL_0:2; end; for k st 1<= k holds P[k] from NAT_1:sch 8(A4,A5); hence thesis by A3; end; end; theorem Th17: k >0 & n > (2*k)|^(k+1) implies k! = [\(n|^k) / (n choose k) /] proof set k1=k+1; assume A1: k>0 & n > (2*k)|^k1; A2: 2*k >=1 & k >=1 by A1,NAT_1:14; k1 >=1 by NAT_1:11; then (2*k)|^k1 >= 2*k by A2,PREPOWER:12; then A3: n > 2*k by A1,XXREAL_0:2; k1>1+0 by A1,XREAL_1:6; then k1>=1+1 by NAT_1:13; then A4: (2*k)|^k1 >= (2*k)|^(1+1) by A1,NAT_6:1; (2*k)|^(1+1) = (2*k)|^1 * (2*k) by NEWTON:6 .= (2*k) * (2*k); then A5: n > 4*k*k by A1,A4,XXREAL_0:2; (4*k)*k >= (4*k)*1 by A1,NAT_1:14,XREAL_1:64; then A6: 1* n > 2*(2*k) by A5,XXREAL_0:2; k+k >=k by NAT_1:11; then A7: n> k by A3,XXREAL_0:2; then A8: (n|^k) / (n choose k) <= k! * 1 / (1- k/n)|^k by Lm2; A9: 1 / (1- k/n)|^k = (1 / (1- k/n))|^k by PREPOWER:7; A10: n-k>0 by A7,XREAL_1:50; A11: 1/(1- k/n) = n / (n-k) by A7,Lm1; (1 / (1- k/n)) <= 1+(2*k)/n by A1,A3,Lm3; then A12: 1 / (1- k/n)|^k <= (1+(2*k)/n)|^k by A9,A11,A1,A10, PREPOWER:9; (1+(2*k)/n)|^k < 1+((2*k)/n)*(2|^k) by A6,XREAL_1:106,A1,Lm5; then 1 / (1- k/n)|^k < 1+((2*k)/n)*(2|^k) by A12,XXREAL_0:2; then k! * (1 / (1- k/n)|^k) < k! * (1+((2*k)/n)*(2|^k)) by XREAL_1:68; then k! * 1 / (1- k/n)|^k < k! * (1+((2*k)/n)*(2|^k)) by XCMPLX_1:74; then A13: (n|^k) / (n choose k) < k! * (1+((2*k)/n)*(2|^k)) by A8,XXREAL_0:2; ((2*k)/n)*(2|^k) = (2*k)* (2|^k) / n by XCMPLX_1:74; then A14: k! * ((2*k)/n)*(2|^k) = k!* (((2*k)* (2|^k)) / n) .=( k!* ((2*k)* (2|^k))) / n by XCMPLX_1:74 .= (k! * (2*k)* (2|^k)) / n; (k! * (2*k)* (2|^k)) / n < (k! * (2*k)* (2|^k)) / ((2*k)|^k1) by A1,XREAL_1:76; then k! + (k! * (2*k)* (2|^k)) / n < k!+ (k! * (2*k)* (2|^k)) / ((2*k)|^k1) by XREAL_1:6; then A15: (n|^k) / (n choose k) < k! + (k! * (2*k)* (2|^k)) / ((2*k)|^k1) by A13,XXREAL_0:2,A14; A16: (2*k)* (2|^k) = k * (2* 2|^k) .= k*2|^k1 by NEWTON:6; A17: ((2*k)* (2|^k)) / ((2*k)|^k1) = (k*2|^k1) / ((2|^k1) * (k|^k1)) by A16,NEWTON:7 .= k / (k|^k1) by XCMPLX_1:91 .= k / (k* k|^k) by NEWTON:6; A18: k! * (2*k)* (2|^k) / ((2*k)|^k1) = k! * ((2*k)* (2|^k)) / ((2*k)|^k1) .= k! * (k / (k* k|^k)) by A17,XCMPLX_1:74 .= (k! * k) / (k* k|^k) by XCMPLX_1:74 .= k! / (k|^k) by A1,XCMPLX_1:91; k! /(k|^k) <=1 by XREAL_1:183,NEWTON02:124; then k! + k! * (2*k)* (2|^k) / ((2*k)|^k1) <= k!+1 by A18,XREAL_1:6; then (n|^k) / (n choose k) < k!+1 by A15,XXREAL_0:2; then A19: (n|^k) / (n choose k)-1 y1 & y = [\y2/y3/] proof let x,y be Nat; thus y=x! implies ex n,y1,y2,y3 be Nat st y1=(2*x) |^(x+1) & y2 = n|^x & y3 = n choose x & n > y1 & y=[\y2/y3/] proof assume A1: y =x!; per cases; suppose A2: x=0; take n=1,y1=0,y2=1,y3=1; thus y1 = (2*x)|^(x+1) & y2 = n|^x & y3 = n choose x & n > y1 by A2,NEWTON:19; thus thesis by INT_1:25,NEWTON:12,A2,A1; end; suppose A3: x>0; take n = (2*x)|^(x+1)+1,y1 = (2*x)|^(x+1); take y2 = n|^x,y3 = n choose x; n > y1 by NAT_1:13; hence thesis by A1,A3,Th17; end; end; given n,y1,y2,y3 be Nat such that A4: y1=(2*x) |^(x+1) & y2 = n|^x & y3 = n choose x & n > y1 and A5: y=[\y2/y3/]; per cases; suppose A6: x=0; then y1= 0 & y2 = 1 & y3 = 1 by A4,NEWTON:4,19; hence thesis by NEWTON:12,A6,A5,INT_1:25; end; suppose x>0; hence thesis by A4,A5,Th17; end; end; begin :: Diophanticity of selected products reserve x,y,x1,u,w for Nat; theorem Th19: for x1,w,u being Nat st x1*w,1 are_congruent_mod u for x being Nat holds Product (1+(x1 * idseq x)), x1|^x * (x!) * ((w+x) choose x) are_congruent_mod u proof let x1,w,u be Nat such that A1: x1*w,1 are_congruent_mod u; consider b be Integer such that A2: u*b = x1*w-1 by A1, INT_1:def 5; defpred P[Nat] means Product (1+(x1*(idseq \$1))), x1|^\$1 * (\$1!) * ((w+\$1) choose \$1) are_congruent_mod u; x1|^0=1 & 0! =1 & (w+0) choose 0 =1 by NEWTON:4,12,19; then A3: P[0] by RVSUM_1:94,INT_1:11; A4: P[n] implies P[n+1] proof set n1=n+1; set P = Product (1+(x1*(idseq n))); set L=x1|^n * (n!) * ((w+n) choose n); assume P[n]; then consider a be Integer such that A5: u*a = P - L by INT_1:def 5; A6: (1+x1*<*n1*>) = 1+<*x1*n1*> by RVSUM_1:47 .= <*1+x1*n1*> by BASEL_1:2; idseq n1 = (idseq n)^<*n+1*> by FINSEQ_2:51; then x1*(idseq n1) = (x1*(idseq n))^(x1*<*n+1*>) by NEWTON04:43; then A7: 1+ x1*(idseq n1) = (1+x1*(idseq n))^(1+x1*<*n+1*>) by BASEL_1:3; w+n>= n & w+n-n=w by NAT_1:11; then (w+n) choose n = (w+n)! / ((n!)*(w!)) by NEWTON:def 3; then A8: n! * ((w+n) choose n) = (n!)*((w+n)!) / ((n!) *(w!)) by XCMPLX_1:74 .= ((w+n)!) / (w!) by XCMPLX_1:91; w+n1>= n1 & w+n1-n1=w by NAT_1:11; then (w+n1) choose n1 = (w+n1)! / ((n1!)*(w!)) by NEWTON:def 3; then A9: n1! * ((w+n1) choose n1) = (n1!)*((w+n1)!) / ((n1!) *(w!)) by XCMPLX_1:74 .= ((w+n+1)!) / (w!) by XCMPLX_1:91 .= ((w+n)!*(w+n+1)) / (w!) by NEWTON:15 .= (w+n+1)* (((w+n)!)/ (w!)) by XCMPLX_1:74 .= (w+n1) * (n!) * ((w+n) choose n) by A8; x1|^n1 = x1 |^n * x1 by NEWTON:6; then x1|^n1 * (n1!) * ((w+n1) choose n1) = x1|^n*x1 * ((n1!) * ((w+n1) choose n1)) .= x1|^n*x1 * ((w+n+1) * (n!) * ((w+n) choose n)) by A9 .= (w+n1) * x1 * L; then Product (1+(x1*(idseq n1))) - x1|^n1 * (n1!) * ((w+n1) choose n1) = P * (1+x1*n1) - x1*(w+n1) * L by A7,A6,RVSUM_1:96 .= P * (1+x1*n1) - (x1*w*L) -( x1*n1*L) .= P * (1+x1*n1) - (u*b+1)*L -( x1*n1*L) by A2 .= (P -L )* (1+x1*n1) - (u*b*1)*L .= u*a*(1+x1*n1)- u*b*L by A5 .= u*(a*(1+x1*n1)- b*L); hence thesis by INT_1:def 5; end; P[n] from NAT_1:sch 2(A3,A4); hence thesis; end; theorem Th20: for x,y,x1 being Nat st x1 >= 1 holds y = Product (1+(x1 * idseq x)) iff ex u,w,y1,y2,y3,y4,y5 being Nat st u > y & x1*w, 1 are_congruent_mod u & y1 = x1|^x & y2 = x! & y3 = (w+x) choose x & y1*y2*y3, y are_congruent_mod u & y4 = 1+x1*x & y5 = y4|^x & u > y5 proof let x,y,x1 be Nat; assume A1: x1>=1; defpred P[Nat] means (1+x1*\$1)|^\$1 >= Product (1+(x1 * idseq \$1)); A2: P[0] by RVSUM_1:94; A3: P[n] implies P[n+1] proof assume A4: P[n]; set n1=n+1; A5: (1+x1*<*n1*>) = 1+<*x1*n1*> by RVSUM_1:47 .= <*1+x1*n1*> by BASEL_1:2; idseq n1 = (idseq n)^<*n+1*> by FINSEQ_2:51; then x1*(idseq n1) = (x1*(idseq n))^(x1*<*n+1*>) by NEWTON04:43; then 1+ x1*(idseq n1) = (1+x1*(idseq n))^(1+x1*<*n+1*>) by BASEL_1:3; then A6: Product (1+(x1*(idseq n1)))= Product (1+(x1*(idseq n))) * (1+x1*n1) by A5,RVSUM_1:96; x1*n <= x1*n1 by NAT_1:11,XREAL_1:64; then (1+x1*n) <= (1+x1*n1) by XREAL_1:7; then (1+x1*n)|^n <= (1+x1*n1)|^n by PREPOWER:9; then (1+x1*n)|^n * (1+x1*n1) <= (1+x1*n1)|^n * (1+x1*n1) by XREAL_1:64; then A7: (1+x1*n)|^n * (1+x1*n1) <= (1+x1*n1)|^n1 by NEWTON:6; Product (1+(x1*(idseq n))) * (1+x1*n1) <= (1+x1*n)|^n * (1+x1*n1) by A4,XREAL_1:64; hence thesis by A7,A6,XXREAL_0:2; end; A8:P[n] from NAT_1:sch 2(A2,A3); thus y = Product (1+(x1 * idseq x)) implies ex u,w,y1,y2,y3,y4,y5 be Nat st u > y & x1*w,1 are_congruent_mod u & y1 = x1|^x & y2= x! & y3 = (w+x) choose x & y1*y2*y3,y are_congruent_mod u & y4=1+x1*x & y5 = y4|^x & u > y5 proof assume A9: y = Product (1+(x1 * idseq x)); set u = x1 *(1+x1*x)|^x +1; u gcd x1 = 1 gcd x1 by EULER_1:16 .= 1 by WSIERP_1:8; then consider w be Nat such that A10: (x1*w - 1) mod u = 0 by INT_4:16,INT_2:def 3; take u,w, y1 = x1|^x, y2= x!, y3 = (w+x) choose x, y4 = 1+x1*x, y5 = y4|^x; A11: x1*w - 1 = ((x1*w - 1) div u) * u +0 by A10,INT_1:59; then y, x1|^x * (x!) * ((w+x) choose x) are_congruent_mod u by A9,Th19,INT_1:def 5; then consider e be Integer such that A12: x1|^x * (x!) * ((w+x) choose x)-y = u*e by INT_1:def 5,14; (1+x1*x)|^x >= Product (1+(x1 * idseq x)) by A8; then x1* (1+x1*x)|^x >= 1* Product (1+(x1 * idseq x)) by A1,XREAL_1:66; hence u > y by A9,NAT_1:13; thus x1*w,1 are_congruent_mod u by A11,INT_1:def 5; A13: x1 *(1+x1*x)|^x+1> x1 *(1+x1*x)|^x+0 by XREAL_1:6; x1 *(1+x1*x)|^x >= 1*(1+x1*x)|^x by A1,XREAL_1:66; hence thesis by A12,INT_1:def 5,A13,XXREAL_0:2; end; given u,w,y1,y2,y3,y4,y5 be Nat such that A14: u > y & x1*w,1 are_congruent_mod u and A15: y1 = x1|^x & y2= x! & y3 = (w+x) choose x and A16: y1*y2*y3,y are_congruent_mod u and A17: y4=1+x1*x & y5 = y4|^x & u > y5; set U = x1|^x * (x!) * ((w+x) choose x); Product (1+(x1 * idseq x)),U are_congruent_mod u by A14,Th19; then A18: U,Product (1+(x1 * idseq x)) are_congruent_mod u by INT_1:14; A19: Product (1+(x1 * idseq x)) is Nat by TARSKI:1; Product (1+(x1 * idseq x)) <=(1+x1*x)|^x by A8; then Product (1+(x1 * idseq x)) < u by A17,XXREAL_0:2; hence thesis by A19,A18,A15,A16,A14,NAT_6:14; end; theorem Th21: c1 + (n|->c2) = n|->(c1+c2) proof A1: len (c1+(n|->c2)) = len (n|->c2)=n=len (n|->(c1+c2)) by CARD_1:def 7; now let i such that A2: 1<= i <= n; A3: i in dom (c1 + (n|->c2)) by A2,A1,FINSEQ_3:25; A4: i in Seg n by A2; hence (n|->(c1+c2)).i = c1+c2 by FINSEQ_2:57 .= c1 + ((n|->c2).i) by A4,FINSEQ_2:57 .= (c1 + (n|->c2)).i by A3,VALUED_1:def 2; end; hence thesis by FINSEQ_1:14,A1; end; theorem for x,y,x1 being Nat st x1 = 0 holds y = Product (1+(x1 * idseq x)) iff y = 1 proof let x,y,x1 be Nat such that A1: x1 = 0; A2: len (idseq x) =x; rng (idseq x) c= REAL; then idseq x is FinSequence of REAL by FINSEQ_1:def 4; then idseq x is Element of x-tuples_on REAL by A2,FINSEQ_2:92; then x1 * idseq x = x|->0 by A1,RVSUM_1:53; then 1+(x1 * idseq x) = x|->(1+0) by Th21; hence thesis by RVSUM_1:102; end; theorem Th23: n >= k implies Product ((n+1)+(-idseq k)) = k!*(n choose k) proof defpred P[Nat] means \$1 <= n implies Product ( (n+1)+(-idseq \$1)) = \$1!*(n choose \$1); A1: P[0] by RVSUM_1:94,NEWTON:12,19; A2: P[i] implies P[i+1] proof set i1=i+1; assume A3: P[i] & i1 <= n; A4: (-1)*<*i1*> = -<*i1*> .= <*-i1*> by RVSUM_1:20; -idseq i1 = (-1) * ((idseq i) ^<*i1*>) by FINSEQ_2:51 .= (- idseq i) ^<*-i1*> by A4,NEWTON04:43; then (n+1)+(-idseq i1) = ((n+1)+ - idseq i) ^((n+1)+<*-i1*>) by BASEL_1:3 .= ((n+1)+ - idseq i) ^<*(n+1)+-i1*> by BASEL_1:2; then A5: Product ( (n+1)+(-idseq i1)) = Product ( (n+1)+(-idseq i)) * ((n+1)+-i1) by RVSUM_1:96; reconsider l=n-i1 as Element of NAT by A3,NAT_1:21; A6: i <=n &n-i = l+1 by NAT_1:13,A3; n choose i1 = n! / ((i1!)*(l!)) by A3,NEWTON:def 3; then i1! * (n choose i1) = (i1!)*(n!) / ((i1!) *(l!)) by XCMPLX_1:74 .= (n!) / (l!) by XCMPLX_1:91 .= (n!*(l+1)) / (l!*(l+1)) by XCMPLX_1:91 .= (n!*(l+1)) / ((l+1)!) by NEWTON:15 .= (n!*(l+1)*(i!)) / ((l+1)!*(i!)) by XCMPLX_1:91 .= ((l+1)*(i!)*(n!)) / ((l+1)!*(i!)) .= ((l+1)*(i!))* ((n!) / ((l+1)!*(i!))) by XCMPLX_1:74 .= ((n+1)+-i1)*(i!)* (n choose i) by NEWTON:def 3,A6; hence thesis by NAT_1:13,A3,A5; end; P[i] from NAT_1:sch 2(A1,A2); hence thesis; end; theorem for y,x1,x2 being Nat holds y = Product ( (x2+1)+(-idseq x1)) & x2 > x1 iff y = x1!*(x2 choose x1) & x2 > x1 by Th23; begin :: Selected subsets of zero based finite sequences of NAT :: as Diophantine sets reserve n,m,k for Nat, p,q for n-element XFinSequence of NAT, i1,i2,i3,i4,i5,i6 for Element of n, a,b,d,f for Integer; theorem Th25: for a,b being Nat,i1,i2,i3 holds {p: p.i1 = (a*p.i2+b) * p.i3} is diophantine Subset of n -xtuples_of NAT proof let a,b be Nat; deffunc F1(Nat,Nat,Nat) = a*\$1+ b; A1: 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*\$1 = 1 * \$3 *\$2; A2: for n,i1,i2,i3,i4,i5,i6 holds {p : P1[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]} is diophantine Subset of n -xtuples_of NAT by HILB10_3:9; A3: for n,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(A2,A1); let i1,i2,i3; defpred Q1[XFinSequence of NAT] means P1[\$1.i1,\$1.i3,a*\$1.i2+b,\$1.i3,\$1.i3,\$1.i3]; defpred Q2[XFinSequence of NAT] means \$1.i1 = (a*\$1.i2+b) * \$1.i3; A4: for p holds Q1[p] iff Q2[p]; {p : Q1[p]} = {q :Q2[q]} from HILB10_3:sch 2(A4); hence thesis by A3; end; theorem for a,i1,i2,i3 holds {p: p.i1 = a*p.i2*p.i3} is diophantine Subset of n -xtuples_of NAT proof let a,i1,i2,i3; defpred Q1[XFinSequence of NAT] means 1*\$1.i1 = a*\$1.i2*\$1.i3; defpred Q2[XFinSequence of NAT] means \$1.i1 = a*\$1.i2*\$1.i3; A1:for p holds Q1[p] iff Q2[p]; {p:Q1[p]} = {q:Q2[q]} from HILB10_3:sch 2(A1); hence thesis by HILB10_3:9; end; theorem for A being diophantine Subset of n -xtuples_of NAT for k,nk being Nat st k+nk = n holds {p/^nk : p in A} is diophantine Subset of k -xtuples_of NAT proof let A be diophantine Subset of n -xtuples_of NAT; let k,nk be Nat such that A1: k+nk=n; consider nA be Nat, pA be INT -valued Polynomial of n+nA,F_Real such that A2: for s be object holds s in A iff ex x be n-element XFinSequence of NAT, y be nA-element XFinSequence of NAT st s=x & eval(pA,@(x^y)) = 0 by HILB10_2:def 6; dom (id (n+nA))=n+nA; then reconsider I=id (n+nA) as XFinSequence by AFINSQ_1:5; set I1 = I|nk, I2= (I|n)/^nk,I3 = I/^n; Segm nk c= Segm n by NAT_1:39,NAT_1:11,A1; then A3: (I|n)|nk = I1 by RELAT_1:74; then A4: I = (I|n)^I3 & I|n = I1^I2; then A5: rng (I|n) misses rng I3 by HILB10_2:1; A6: len I = n+nA; A7: n <= n+nA by NAT_1:11; A8: len I3 = n+nA-'n =n+nA-n & len (I|n) = n by A6,AFINSQ_2:def 2,AFINSQ_1:54,NAT_1:11; A9: len I2 = n-'nk =n-nk & len I1 = nk by A1,NAT_1:11,A8,AFINSQ_2:def 2,AFINSQ_1:54,A3; A10: len (I2^I1^I3) = len (I2^I1) + len I3 & len (I2^I1) = len I2 + len I1 by AFINSQ_1:17; A11: rng I1 misses rng I2 by A4,HILB10_2:1; A12: rng (I|n)\/ rng I3 = rng I by A4,AFINSQ_1:26; A13: rng I1 \/rng I2= rng (I|n) & rng (I2^I1) = rng I2\/ rng I1 by A4,AFINSQ_1:26; then rng (I2^I1^I3)=n+nA by A12,AFINSQ_1:26; then reconsider J = I2^I1^I3 as Function of n+nA,n+nA by A10,A8,A9,FUNCT_2:1; A14: J is onto by A13,A12,AFINSQ_1:26; A15: I2^I1 is one-to-one by A11,CARD_FIN:52; J is one-to-one by A13,A5,A15,CARD_FIN:52; then reconsider J as Permutation of (n+nA) by A14; A16: J=J"" by FUNCT_1:43; set h= pA permuted_by J"; reconsider H=h as Polynomial of k+(nk+nA),F_Real by A1; rng h = rng pA c= INT by HILB10_2:26,RELAT_1:def 19; then reconsider H as INT -valued Polynomial of k+(nk+nA),F_Real by RELAT_1:def 19; set Y={p/^nk : p in A}; Y c= k -xtuples_of NAT proof let y be object; assume y in Y; then consider p such that A17: y =p/^nk & p in A; len p=n by CARD_1:def 7; then p/^nk is k-element by A1,A9,AFINSQ_2:def 2; hence thesis by A17,HILB10_2:def 5; end; then reconsider Y as Subset of k -xtuples_of NAT; for s be object holds s in Y iff ex x be k-element XFinSequence of NAT, y be (nk+nA)-element XFinSequence of NAT st s=x & eval(H,@(x^y)) = 0 proof let s be object; thus s in Y implies ex x be k-element XFinSequence of NAT, y be (nk+nA)-element XFinSequence of NAT st s=x & eval(H,@(x^y)) = 0 proof assume s in Y; then consider w be n-element XFinSequence of NAT such that A18: s= w/^nk & w in A; consider x be n-element XFinSequence of NAT, y be nA-element XFinSequence of NAT such that A19: w=x & eval(pA,@(x^y)) = 0 by A2,A18; A20: eval(pA,@(x^y)) = eval(h,@(x^y)*J"") by HILB10_2:25; A21: len x = n & len y = nA by CARD_1:def 7; then A22: len (x/^nk) = k by A1,A9,AFINSQ_2:def 2; x/^nk is k-element by A21,A1,A9,AFINSQ_2:def 2; then reconsider S = x/^nk as k-element XFinSequence of NAT; A23: len (x|nk) = nk by CARD_1:def 7,A1; reconsider XnkY=(x|nk)^y as (nk+nA)-element XFinSequence of NAT by A1; A26: len (S^ XnkY) = n+nA by A1,CARD_1:def 7; A27: dom (@(x^y)*J) = n+nA by FUNCT_2:def 1; (x|nk)^(x/^nk)=x; then A28: x^y = (x|nk)^(S^y) by AFINSQ_1:27; for i be object st i in dom (S^ XnkY) holds (@(x^y)*J).i = (S^ XnkY).i proof let j be object; assume A29: j in dom (S^ XnkY); then reconsider j as Nat; A30: j in dom (J) & (@(x^y)*J).j = (@(x^y)).(J.j) by A29,A26,A27,FUNCT_1:11,12; per cases by A30,AFINSQ_1:20; suppose A31: j in dom (I2^I1); then A32: J.j = (I2^I1).j by AFINSQ_1:def 3; per cases by A31,AFINSQ_1:20; suppose A33: j in dom I2; then A34: (I2^I1).j = I2.j & I2.j = (I|n).(nk+j) & j < k by A9,A1,AFINSQ_2:def 2,AFINSQ_1:66,def 3; A35: nk+j in n by A1,A33,A9,AFINSQ_1:66,HILB10_3:3; then A36: (I|n).(nk+j) = I.(nk+j) by FUNCT_1:49; A37: dom S c= dom (S^y) by AFINSQ_1:21; A38: len S = k =len I2 by CARD_1:def 7,A1,A9; Segm n =n; then nk+j < n+nA by NAT_1:44,A35,A7,XXREAL_0:2; then nk+j in Segm (n+nA) by NAT_1:44; then (@(x^y)*J).j = (@(x^y)).(nk+j) by FUNCT_1:17,A32,A30,A36,A34 .=(x^y).(nk+j) by HILB10_2:def 1 .= (S^y).j by A23,A37,A22,A33,A1,A9,A28,AFINSQ_1:def 3 .= S.j by A22,A33,A1,A9,AFINSQ_1:def 3 .= (S^ XnkY).j by A33,A38,AFINSQ_1:def 3; hence thesis; end; suppose ex k st k in dom I1 & j=len I2 + k; then consider w such that A39: w in dom I1 & j=len I2 + w; A40: (I2^I1).j = I1.w & I1.w = I.w & w < nk by A39,A9,AFINSQ_1:66,def 3,FUNCT_1:49; A41: dom (x|nk) c= dom ((x|nk)^y) by AFINSQ_1:21; nk <= nk+ (k + nA) by NAT_1:11; then w < n+nA by A1,A39,A9,AFINSQ_1:66,XXREAL_0:2; then A42: w in Segm (n+nA) by NAT_1:44; J.j = w by A42,A40,A32,FUNCT_1:17; then (@(x^y)*J).j =((x|nk)^(S^y)).w by A30,A28,HILB10_2:def 1 .= (x|nk).w by AFINSQ_1:def 3,A39,A23,A9 .= ((x|nk)^y).w by A39,A23,A9,AFINSQ_1:def 3 .= (S^ XnkY).j by A22,A39,A1,A9,A41,A23,AFINSQ_1:def 3; hence thesis; end; end; suppose ex n st n in dom I3 & j=len (I2^I1) + n; then consider w such that A43: w in dom I3 & j=len (I2^I1) + w; A44: len (S^(x|nk))= n by CARD_1:def 7,A1; J.j = I3.w by A43,AFINSQ_1:def 3 .= I.j by A9,A10,A43,AFINSQ_2:def 2 .= j by A29,A26,FUNCT_1:17; then (@(x^y)*J).j =(x^y).j by A30,HILB10_2:def 1 .= y.w by A9,A10,A43,A8,A21,AFINSQ_1:def 3 .= ((S^(x|nk))^y).j by A44,A9,A10,A43,A8,A21,AFINSQ_1:def 3 .= (S^ XnkY).j by AFINSQ_1:27; hence thesis; end; end; then @(x^y)*J = (S^ XnkY) by CARD_1:def 7,A1,A27,FUNCT_1:2; then @(x^y)*J = @(S^ XnkY) by HILB10_2:def 1; hence thesis by A19,A18,A20,A16; end; given S be k-element XFinSequence of NAT, XnkY be (nk+nA)-element XFinSequence of NAT such that A45: s=S & eval(H,@(S^XnkY)) = 0; set Xnk=XnkY|nk; set y=XnkY /^ nk; set X = Xnk ^ S; A46: len S = k & len XnkY = (nk+nA) & nk+nA >= nk by NAT_1:11,CARD_1:def 7; then A47: len Xnk = nk & len y = nk+nA-'nk = nk+nA-nk by AFINSQ_1:54,AFINSQ_2:def 2; reconsider y as nA -element XFinSequence of NAT by A47,CARD_1:def 7; reconsider X as n-element XFinSequence of NAT by A1; A48: X|nk = Xnk by A47,AFINSQ_1:57; Xnk ^ S = (X|nk) ^ (X/^nk); then A49: X/^nk = S by A48,AFINSQ_1:28; A50: XnkY = Xnk ^ y; A51: len X = n & len y = nA by CARD_1:def 7; A52: len (X|nk) = nk by A47,AFINSQ_1:57; A53: len (S^ XnkY) = n+nA by CARD_1:def 7,A1; A54: dom (@(X^y)*J) = n+nA by FUNCT_2:def 1; A55: X^y = (X|nk)^(S^y) by A48,AFINSQ_1:27; for i be object st i in dom (S^ XnkY) holds (@(X^y)*J).i = (S^ XnkY).i proof let j be object; assume A56: j in dom (S^ XnkY); then reconsider j as Nat; A57: j in dom J & (@(X^y)*J).j = (@(X^y)).(J.j) by A56,A53,A54,FUNCT_1:11,12; per cases by A57,AFINSQ_1:20; suppose A58: j in dom (I2^I1); then A59: J.j = (I2^I1).j by AFINSQ_1:def 3; per cases by A58,AFINSQ_1:20; suppose A60: j in dom I2; then A61: (I2^I1).j = I2.j & I2.j = (I|n).(nk+j) & j < k by A9,A1,AFINSQ_2:def 2,AFINSQ_1:66,def 3; then A63: (I|n).(nk+j) = I.(nk+j) by A1,HILB10_3:3,FUNCT_1:49; A62: nk+j in n by A60,A1,HILB10_3:3,A9,AFINSQ_1:66; A64: dom S c= dom (S^y) by AFINSQ_1:21; A65: len S = k =len I2 by CARD_1:def 7,A1,A9; Segm n =n; then nk+j < n+nA by NAT_1:44,A62,A7,XXREAL_0:2; then nk+j in Segm (n+nA) by NAT_1:44; then I.(nk+j) = nk+j by FUNCT_1:17; then (@(X^y)*J).j =((X|nk)^(S^y)).(nk+j) by A55,HILB10_2:def 1,A59,A57,A63,A61 .= (S^y).j by A52,A64,A60,A1,A46,A9,AFINSQ_1:def 3 .= S.j by A60,A1,A46,A9,AFINSQ_1:def 3 .= (S^ XnkY).j by A60,A65,AFINSQ_1:def 3; hence thesis; end; suppose ex k st k in dom I1 & j=len I2 + k; then consider w such that A66: w in dom I1 & j=len I2 + w; A67: (I2^I1).j = I1.w & I1.w = I.w & w < nk by A66,A9,AFINSQ_1:66,def 3,FUNCT_1:49; A68: dom (X|nk) c= dom ((X|nk)^y) by AFINSQ_1:21; nk <= nk+ (k + nA) by NAT_1:11; then w < n+nA by A1,A66,A9,AFINSQ_1:66,XXREAL_0:2; then A69: w in Segm (n+nA) by NAT_1:44; J.j = w by A59,A69,FUNCT_1:17,A67; then (@(X^y)*J).j =(X^y).w by HILB10_2:def 1,A57 .=(X|nk).w by AFINSQ_1:def 3,A66,A52,A9,A55 .= ((X|nk)^y).w by A66,A52,A9,AFINSQ_1:def 3 .= (S^ XnkY).j by A48,A46,A1,A9,A68,A47,A66,AFINSQ_1:def 3; hence thesis; end; end; suppose ex n st n in dom I3 & j=len (I2^I1) + n; then consider w such that A70: w in dom I3 & j=len (I2^I1) + w; A71: len (S^(X|nk)) = n by A1,CARD_1:def 7; J.j = I3.w by A70,AFINSQ_1:def 3 .= I.j by A9,A10,A70,AFINSQ_2:def 2 .= j by A56,A53,FUNCT_1:17; then (@(X^y)*J).j =(X^y).j by HILB10_2:def 1,A57 .= y.w by A9,A10,A70,A8,A51,AFINSQ_1:def 3 .= ((S^(X|nk))^y).j by A71,A9,A10,A70,A8,A51,AFINSQ_1:def 3 .= (S^ XnkY).j by AFINSQ_1:27,A48,A50; hence thesis; end; end; then @(X^y)*J = (S^XnkY) by CARD_1:def 7,A1,A54,FUNCT_1:2; then @(X^y)*J = @(S^XnkY) by HILB10_2:def 1; then eval(H,@(S^XnkY)) = eval(pA,@(X^y)) by A16,HILB10_2:25; then X in A by A2,A45; hence s in Y by A49,A45; end; hence thesis by HILB10_2:def 6; end; theorem Th28: for a,b being Integer,c being Nat, i1,i2,i3 holds {p: a*p.i1 = [\ (b*p.i2) / (c*p.i3)/] & (c*p.i3 <> 0) } is diophantine Subset of n -xtuples_of NAT proof let a,b be Integer,c be Nat; let i1,i2,i3; deffunc F2(Nat,Nat,Nat) = c*\$3 + (a*c)* \$1 * \$3; A1: for n,i1,i2,i3,i4,d holds {p: F2(p.i1,p.i2,p.i3) = d*(p.i4)} is diophantine Subset of n -xtuples_of NAT proof let n,i1,i2,i3,i4,d; defpred P1[Nat,Nat,Integer] means d*\$1 = c*\$2 + \$3+0; A2: for n,i1,i2,i3,f holds {p: P1[p.i1,p.i2,f*(p.i3)]} is diophantine Subset of n -xtuples_of NAT by HILB10_3:11; deffunc F1(Nat,Nat,Nat) = (a*c)*\$1*\$3; A3: for n,i1,i2,i3,i4,f holds {p: F1(p.i1,p.i2,p.i3) = f*(p.i4)} is diophantine Subset of n -xtuples_of NAT by HILB10_3:9; A4: for n,i1,i2,i3,i4,i5 holds {p: P1[p.i1,p.i2,F1(p.i3,p.i4,p.i5)]} is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 5(A2,A3); defpred R1[XFinSequence of NAT] means F2(\$1.i1,\$1.i2,\$1.i3) = d*(\$1.i4); defpred R2[XFinSequence of NAT] means P1[\$1.i4,\$1.i3,F1(\$1.i1,\$1.i2,\$1.i3)]; A5: for p holds R1[p] iff R2[p]; {p: R1[p]} = {q: R2[q]} from HILB10_3:sch 2(A5); hence thesis by A4; end; defpred P2[Nat,Nat,Integer] means b*\$1+0 < \$3; A6: for n,i1,i2,i3,d holds {p: P2[p.i1,p.i2,d*(p.i3)]} is diophantine Subset of n -xtuples_of NAT by HILB10_3:7; A7: for n,i1,i2,i3,i4,i5 holds {p: P2[p.i1,p.i2,F2(p.i3,p.i4,p.i5)]} is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 5(A6,A1); defpred P3[Nat,Nat,Integer] means b*\$1 >= \$3+0; A8: for n,i1,i2,i3,d holds {p:P3[p.i1,p.i2,d*(p.i3)]} is diophantine Subset of n -xtuples_of NAT by HILB10_3:8; deffunc F3(Nat,Nat,Nat) = (a*c)* \$1 * \$3; A9: for n,i1,i2,i3,i4,d holds {p: F3(p.i1,p.i2,p.i3) = d*(p.i4)} is diophantine Subset of n -xtuples_of NAT by HILB10_3:9; A10:for n,i1,i2,i3,i4,i5 holds {p: P3[p.i1,p.i2,F3(p.i3,p.i4,p.i5)]} is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 5(A8,A9); defpred Q1[XFinSequence of NAT] means P2[\$1.i2,\$1.i2,F2(\$1.i1,\$1.i1,\$1.i3)]; defpred Q2[XFinSequence of NAT] means P3[\$1.i2,\$1.i2,F3(\$1.i1,\$1.i1,\$1.i3)]; defpred Q12[XFinSequence of NAT] means Q1[\$1] & Q2[\$1]; defpred Q3[XFinSequence of NAT] means c*\$1.i3 <> 0 * \$1.i3+0; defpred Q123[XFinSequence of NAT] means Q12[\$1] & Q3[\$1]; defpred T[XFinSequence of NAT] means a*\$1.i1 = [\ (b*\$1.i2) / (c*\$1.i3)/] & c*\$1.i3 <> 0; A11:{p:Q1[p]} is diophantine Subset of n -xtuples_of NAT by A7; A12:{p:Q2[p]} is diophantine Subset of n -xtuples_of NAT by A10; {p:Q1[p] & Q2[p]} is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 3(A11,A12); then A13: {p:Q12[p]} is diophantine Subset of n -xtuples_of NAT; A14: {p: Q3[p]} is diophantine Subset of n -xtuples_of NAT by HILB10_3:16; A15: {p:Q12[p] & Q3[p]} is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 3(A13,A14); A16: for p holds T[p] iff Q123[p] proof let p; thus T[p] implies Q123[p] proof assume A17: T[p]; then A18: (a*p.i1) * (c*p.i3) <= b*p.i2 by XREAL_1:83,INT_1:def 6; (b*p.i2) / (c*p.i3)* (c*p.i3) = (c*p.i3) / (c*p.i3)* (b*p.i2) by XCMPLX_1:75 .= 1*(b*p.i2) by A17,XCMPLX_1:60; then A19: ((b*p.i2) / (c*p.i3) -1)* (c*p.i3) = b*p.i2 - c*p.i3; (b*p.i2) / (c*p.i3)- 1 < a*p.i1 by A17,INT_1:def 6; then ((b*p.i2) / (c*p.i3)- 1)*(c*p.i3) < a*p.i1*(c*p.i3) by A17,XREAL_1:68; hence thesis by A18,A19,XREAL_1:19; end; assume A20: Q123[p]; then A21: a*p.i1 * (c*p.i3) > b*p.i2 - c*p.i3 by XREAL_1:19; (b*p.i2) / (c*p.i3)* (c*p.i3) = (c*p.i3) / (c*p.i3)* (b*p.i2) by XCMPLX_1:75 .= 1*(b*p.i2) by A20,XCMPLX_1:60; then ((b*p.i2) / (c*p.i3) -1)* (c*p.i3) = b*p.i2 - c*p.i3; then A22: a*p.i1 > (b*p.i2) / (c*p.i3)-1 by A21,XREAL_1:64; (a*p.i1) * (c*p.i3) <= b*p.i2 by A20; then a*p.i1 <= (b*p.i2) / (c*p.i3) by A20,XREAL_1:77; hence thesis by A20,A22,INT_1:def 6; end; {p: T[p] } = {q:Q123[q]} from HILB10_3:sch 2(A16); hence thesis by A15; end; theorem Th29: for i1,i2,i3 st n <> 0 holds {p: p.i1 >= p.i3 & p.i2 = p.i1 choose p.i3} is diophantine Subset of n -xtuples_of NAT proof let i1,i2,i3;set n6=n+6; defpred R[XFinSequence of NAT] means \$1.i1 >= \$1.i3 & \$1.i2 = \$1.i1 choose \$1.i3; set RR = {p: R[p]}; assume A1: n<>0; n=n+0;then reconsider X=i1,Y=i2,Z=i3,U=n,V=n+1,Y1=n+2,Y2=n+3,Y3=n+4,U1=n+5 as Element of n+6 by HILB10_3:2,3; defpred P1[XFinSequence of NAT] means \$1.Y1 = (\$1.X) |^ (\$1.Z); A2: {p where p is n6-element XFinSequence of NAT:P1[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:24; defpred P2[XFinSequence of NAT] means \$1.Y2 = (\$1.U1) |^ (\$1.X); A3: {p where p is n6-element XFinSequence of NAT:P2[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:24; defpred P3[XFinSequence of NAT] means \$1.Y3 = (\$1.U) |^ (\$1.Z); A4: {p where p is n6-element XFinSequence of NAT:P3[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:24; defpred P4[XFinSequence of NAT] means 1*\$1.U > 1*\$1.Y1+0; A5: {p where p is n6-element XFinSequence of NAT:P4[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:7; defpred P5[XFinSequence of NAT] means 1*\$1.V = [\ (1*\$1.Y2) / (1*\$1.Y3) /] & (1*\$1.Y3) <> 0; A6: {p where p is n6-element XFinSequence of NAT:P5[p]} is diophantine Subset of n6 -xtuples_of NAT by Th28; defpred P6[XFinSequence of NAT] means 1*\$1.Y, 1*\$1.V are_congruent_mod 1*\$1.U; A7: {p where p is n6-element XFinSequence of NAT:P6[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:21; defpred P7[XFinSequence of NAT] means 1*\$1.U > 1*\$1.Y+0; A8: {p where p is n6-element XFinSequence of NAT:P7[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:7; defpred P8[XFinSequence of NAT] means 1*\$1.X >= 1*\$1.Z+0; A9:{p where p is n6-element XFinSequence of NAT:P8[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:8; defpred P9[XFinSequence of NAT] means 1*\$1.U1 = 1*\$1.U+1; A10:{p where p is n6-element XFinSequence of NAT:P9[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:6; defpred P12[XFinSequence of NAT] means P1[\$1] & P2[\$1]; A11:{p where p is n6-element XFinSequence of NAT:P12[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A2,A3); defpred P123[XFinSequence of NAT] means P12[\$1] & P3[\$1]; A12:{p where p is n6-element XFinSequence of NAT:P123[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A11,A4); defpred P1234[XFinSequence of NAT] means P123[\$1] & P4[\$1]; A13:{p where p is n6-element XFinSequence of NAT:P1234[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A12,A5); defpred P12345[XFinSequence of NAT] means P1234[\$1] & P5[\$1]; A14:{p where p is n6-element XFinSequence of NAT:P12345[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A13,A6); defpred P123456[XFinSequence of NAT] means P12345[\$1] & P6[\$1]; A15:{p where p is n6-element XFinSequence of NAT:P123456[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A14,A7); defpred P1234567[XFinSequence of NAT] means P123456[\$1] & P7[\$1]; A16:{p where p is n6-element XFinSequence of NAT:P1234567[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A15,A8); defpred P12345678[XFinSequence of NAT] means P1234567[\$1] & P8[\$1]; A17:{p where p is n6-element XFinSequence of NAT:P12345678[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A16,A9); defpred P123456789[XFinSequence of NAT] means P12345678[\$1] & P9[\$1]; set PP = {p where p is n6-element XFinSequence of NAT:P123456789[p]}; A18:PP is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A17,A10); reconsider PPn = {p|n where p is n6-element XFinSequence of NAT: p in PP} as diophantine Subset of n -xtuples_of NAT by NAT_1:11,HILB10_3:5,A18; A19: PPn c= RR proof let x be object; assume x in PPn; then consider p be n6-element XFinSequence of NAT such that A20: x = p|n & p in PP; ex q be n6-element XFinSequence of NAT st q=p & P123456789[q] by A20; then A21: p.X>=p.Z & p.Y = p.X choose p.Z by Th16; (p|n).X = p.i1 & (p|n).Y = p.i2 & (p|n).Z = p.i3 by A1,HILB10_3:4; hence thesis by A21,A20; end; RR c= PPn proof let x be object; assume x in RR; then consider p such that A22: x=p & R[p]; consider u,v,y1,y2,y3 be Nat such that A23: y1 = (p.i1)|^p.i3 & y2 = (u+1)|^p.i1 & y3 = u|^(p.i3) & u > y1 & v = [\y2/y3/] & p.i2,v are_congruent_mod u & p.i2 < u & p.i1 >=p.i3 by A22,Th16; reconsider u1=u+1 as Element of NAT; reconsider u,v,y1,y2,y3 as Element of NAT by ORDINAL1:def 12; set Y = <%u%>^<%v%>^<%y1%>^<%y2%>^<%y3%>^<%u1%>; set PY = p ^ Y; A24: len p = n & len Y = 6 by CARD_1:def 7; A25: PY|n =p by A24,AFINSQ_1:57; A26: PY.i3 = (PY|n).i3 by A1,HILB10_3:4 .= p.i3 by A24,AFINSQ_1:57; 0 in dom Y by AFINSQ_1:66; then A27: PY.(n+0) = Y.0 by A24,AFINSQ_1:def 3 .= u by AFINSQ_1:47; 1 in dom Y by A24,AFINSQ_1:66; then A28: PY.(n+1) = Y.1 by A24,AFINSQ_1:def 3 .= v by AFINSQ_1:47; 2 in dom Y by A24,AFINSQ_1:66; then A29: PY.(n+2) = Y.2 by A24,AFINSQ_1:def 3 .= y1 by AFINSQ_1:47; 3 in dom Y by A24,AFINSQ_1:66; then A30: PY.(n+3) = Y.3 by A24,AFINSQ_1:def 3 .= y2 by AFINSQ_1:47; 4 in dom Y by A24,AFINSQ_1:66; then A31: PY.(n+4) = Y.4 by A24,AFINSQ_1:def 3 .= y3 by AFINSQ_1:47; 5 in dom Y by A24,AFINSQ_1:66; then A32: PY.(n+5) = Y.5 by A24,AFINSQ_1:def 3 .= u1 by AFINSQ_1:47; P123456789[PY] by A23,A25,A1,HILB10_3:4,A26,A27,A28,A29,A30,A31,A32; then PY in PP; hence thesis by A25,A22; end; hence thesis by A19,XBOOLE_0:def 10; end; theorem Th30: for i1,i2,i3 holds {p: p.i1 >= p.i3 & p.i2 = p.i1 choose p.i3} is diophantine Subset of n -xtuples_of NAT proof let i1,i2,i3;set n6=n+6; defpred R[XFinSequence of NAT] means \$1.i1 >= \$1.i3 & \$1.i2 = \$1.i1 choose \$1.i3; set RR = {p: R[p]}; per cases; suppose A1: n=0; RR c= n -xtuples_of NAT proof let x be object;assume x in RR; then ex p be n-element XFinSequence of NAT st x= p & R[p]; hence thesis by HILB10_2:def 5; end; hence thesis by A1; end; suppose n<>0; hence thesis by Th29; end; end; theorem Th31: for i1,i2 st n<>0 holds {p: p.i1 = p.i2!} is diophantine Subset of n -xtuples_of NAT proof let i1,i2;set n6=n+6; defpred R[XFinSequence of NAT] means \$1.i1 = \$1.i2!; set RR = {p: R[p] }; assume A1: n<>0; n=n+0;then reconsider Y=i1,X=i2,N=n,Y1=n+1,Y2=n+2,Y3=n+3,X1=n+4,X2=n+5 as Element of n+6 by HILB10_3:2,3; defpred P1[XFinSequence of NAT] means \$1.Y1=(\$1.X2) |^(\$1.X1); A2: {p where p is n6-element XFinSequence of NAT:P1[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:24; defpred P2[XFinSequence of NAT] means \$1.Y2=(\$1.N) |^(\$1.X); A3: {p where p is n6-element XFinSequence of NAT:P2[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:24; defpred P3[XFinSequence of NAT] means \$1.N >= \$1.X & \$1.Y3=(\$1.N) choose (\$1.X); A4: {p where p is n6-element XFinSequence of NAT:P3[p]} is diophantine Subset of n6 -xtuples_of NAT by Th30; defpred P4[XFinSequence of NAT] means 1*\$1.Y=[\(1*\$1.Y2)/(1*\$1.Y3)/] & 1*\$1.Y3 <>0; A5: {p where p is n6-element XFinSequence of NAT:P4[p]} is diophantine Subset of n6 -xtuples_of NAT by Th28; defpred P5[XFinSequence of NAT] means 1*\$1.X2=2 * \$1.X+0; A6: {p where p is n6-element XFinSequence of NAT:P5[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:6; defpred P6[XFinSequence of NAT] means 1*\$1.X1= 1*\$1.X+1; A7: {p where p is n6-element XFinSequence of NAT:P6[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:6; defpred P7[XFinSequence of NAT] means 1*\$1.N > 1*\$1.Y1+0; A8: {p where p is n6-element XFinSequence of NAT:P7[p]} is diophantine Subset of n6 -xtuples_of NAT by HILB10_3:7; defpred P12[XFinSequence of NAT] means P1[\$1] & P2[\$1]; A9: {p where p is n6-element XFinSequence of NAT:P12[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A2,A3); defpred P123[XFinSequence of NAT] means P12[\$1] & P3[\$1]; A10: {p where p is n6-element XFinSequence of NAT:P123[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A9,A4); defpred P1234[XFinSequence of NAT] means P123[\$1] & P4[\$1]; A11: {p where p is n6-element XFinSequence of NAT:P1234[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A10,A5); defpred P12345[XFinSequence of NAT] means P1234[\$1] & P5[\$1]; A12: {p where p is n6-element XFinSequence of NAT:P12345[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A11,A6); defpred P123456[XFinSequence of NAT] means P12345[\$1] & P6[\$1]; A13: {p where p is n6-element XFinSequence of NAT:P123456[p]} is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A12,A7); defpred P1234567[XFinSequence of NAT] means P123456[\$1] & P7[\$1]; set PP = {p where p is n6-element XFinSequence of NAT:P1234567[p]}; A14: PP is diophantine Subset of n6 -xtuples_of NAT from HILB10_3:sch 3(A13,A8); reconsider PPn = {p | n where p is n6-element XFinSequence of NAT: p in PP} as diophantine Subset of n -xtuples_of NAT by NAT_1:11,HILB10_3:5,A14; A15: PPn c= RR proof let x be object; assume x in PPn; then consider p be n6-element XFinSequence of NAT such that A16: x= p|n & p in PP; ex q be n6-element XFinSequence of NAT st q=p & P1234567[q] by A16; then A17: p.Y = (p.X)! by Th18; (p|n).X = p.i2 & (p|n).Y = p.i1 by A1,HILB10_3:4; hence thesis by A17,A16; end; RR c= PPn proof let x be object; assume x in RR; then consider p such that A18: x=p & R[p]; consider N,y1,y2,y3 be Nat such that A19: y1=(2*p.i2) |^(p.i2+1) & y2 = N|^(p.i2) & y3 = N choose (p.i2) & N > y1 & p.i1=[\y2/y3/] by Th18,A18; A20: p.i2 <>0 implies N>= p.i2 proof assume p.i2 <>0; then A21: 2* p.i2 >=1 by NAT_1:14; p.i2+1 >=1 by NAT_1:11; then A22: (2*p.i2) |^(p.i2+1) >= (2*p.i2)|^1 by A21,PREPOWER:93; N > 2*p.i2 & p.i2+p.i2 >= p.i2 by A22,A19,XXREAL_0:2,NAT_1:11; hence thesis by XXREAL_0:2; end; reconsider x1=p.i2+1,x2=2*p.i2 as Element of NAT; reconsider N,y1,y2,y3 as Element of NAT by ORDINAL1:def 12; set Y = <%N%>^<%y1%>^<%y2%>^<%y3%>^<%x1%>^<%x2%>; set PY = p ^ Y; A23: len p = n & len Y = 6 by CARD_1:def 7; A24: PY|n =p by A23,AFINSQ_1:57; 0 in dom Y by AFINSQ_1:66; then A25: PY.(n+0) = Y.0 by A23,AFINSQ_1:def 3 .= N by AFINSQ_1:47; 1 in dom Y by A23,AFINSQ_1:66; then A26: PY.(n+1) = Y.1 by A23,AFINSQ_1:def 3 .= y1 by AFINSQ_1:47; 2 in dom Y by A23,AFINSQ_1:66; then A27: PY.(n+2) = Y.2 by A23,AFINSQ_1:def 3 .= y2 by AFINSQ_1:47; 3 in dom Y by A23,AFINSQ_1:66; then A28: PY.(n+3) = Y.3 by A23,AFINSQ_1:def 3 .= y3 by AFINSQ_1:47; 4 in dom Y by A23,AFINSQ_1:66; then A29: PY.(n+4) = Y.4 by A23,AFINSQ_1:def 3 .= x1 by AFINSQ_1:47; 5 in dom Y by A23,AFINSQ_1:66; then A30: PY.(n+5) = Y.5 by A23,AFINSQ_1:def 3 .= x2 by AFINSQ_1:47; P1234567[PY] by A20,A19,CATALAN2:26,A24,A1,HILB10_3:4,A25,A26,A27,A28,A29,A30; then PY in PP; hence thesis by A24,A18; end; hence thesis by A15,XBOOLE_0:def 10; end; theorem Th32: for i1,i2 holds {p: p.i1 = p.i2!} is diophantine Subset of n -xtuples_of NAT proof let i1,i2;set n6=n+6; defpred R[XFinSequence of NAT] means \$1.i1 = \$1.i2!; set RR = {p: R[p] }; per cases; suppose A1: n=0; RR c= n -xtuples_of NAT proof let x be object; assume x in RR; then ex p be n-element XFinSequence of NAT st x= p & R[p]; hence thesis by HILB10_2:def 5; end; hence thesis by A1; end; suppose n<>0; hence thesis by Th31; end; end; theorem for n,i1,i2,i3 holds {p: 1+(p.i1+1)*(p.i2!) = p.i3} is diophantine Subset of n -xtuples_of NAT proof deffunc F1(Nat,Nat,Nat) = 1*\$1+ (-1); A1: for i1,i2,i3,i4,a holds {p: F1(p.i1,p.i2,p.i3) = a* p.i4} is diophantine Subset of n -xtuples_of NAT by HILB10_3:6; defpred P1[Nat,Nat,Integer] means 1*\$1*\$2 = \$3; A2: for i1,i2,i3,a holds {p: P1[p.i1,p.i2,a* p.i3]} is diophantine Subset of n -xtuples_of NAT by HILB10_3:9; A3: for i1,i2,i3,i4,i5 holds {p: P1[p.i1,p.i2,F1(p.i3,p.i4,p.i5)]} is diophantine Subset of n -xtuples_of NAT from HILB10_3:sch 5(A2,A1); deffunc F2(Nat,Nat,Nat) = \$1!; A4: for i1,i2,i3,i4 holds {p : F2(p.i1,p.i2,p.i3) = p.i4} is diophantine Subset of n -xtuples_of NAT by Th32; defpred P2[Nat,Nat,natural object,Nat,Nat,Nat] means 1*\$1*\$3 = (1*\$2-1); A5: now let n,i1,i3,i2,i4,i5,i6; defpred Q1[XFinSequence of NAT] means P1[\$1.i1,\$1.i2,1*(\$1.i3)+-1]; defpred Q2[XFinSequence of NAT] means P2[\$1.i1,\$1.i3,\$1.i2,\$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 : P2[p.i1,p.i3,p.i2,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: 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(A5,A4); defpred P3[Nat,Nat,natural object,Nat,Nat,Nat] means 1*\$3*(\$1!) = (1*\$2-1); A8:for n,i1,i4,i2,i3,i5,i6 holds {p : P3[p.i1,p.i4,p.i2,p.i3,p.i5,p.i6]} is diophantine Subset of n -xtuples_of NAT by A7; deffunc F3(Nat,Nat,Nat) = 1*\$1+1; A9: for n for i1,i2,i3,i4 holds {p : F3(p.i1,p.i2,p.i3) = p.i4} is diophantine Subset of n -xtuples_of NAT by HILB10_3:15; A10: for n for i1,i2,i3,i4,i5 holds {p : P3[p.i1,p.i2,F3(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(A8,A9); let n,i1,i2,i3; defpred Q1[XFinSequence of NAT] means P3[\$1.i2,\$1.i3,1*\$1.i1+1,\$1.i3,\$1.i3,\$1.i3]; defpred Q2[XFinSequence of NAT] means 1+ (\$1.i1+1)*(\$1.i2!) = \$1.i3; A11: for p holds Q1[p] iff Q2[p]; {p : Q1[p]} = {q :Q2[q]} from HILB10_3:sch 2(A11); hence thesis by A10; end; theorem Th34: for i1,i2,i3 st n<>0 holds {p: p.i3 = Product (1+((p.i1) * idseq (p.i2))) & p.i1 >= 1} is diophantine Subset of n -xtuples_of NAT proof let i1,i2,i3;set n12=n+13; defpred R[XFinSequence of NAT] means \$1.i3 = Product (1+((\$1.i1) * idseq (\$1.i2))) & \$1.i1 >= 1; set RR = {p: R[p] }; assume A1: n<>0; n=n+0;then reconsider X1=i1,X=i2,Y=i3, U=n,W=n+1,Y1=n+2,Y2=n+3,Y3=n+4,Y4=n+5, Y5 = n+6,X1W=n+7,WX=n+8,Y1Y2=n+9,Y1Y2Y3=n+10,X1X=n+11,ONE=n+12 as Element of n12 by HILB10_3:2,3; defpred P0[XFinSequence of NAT] means 1* \$1.X1 >= 0* \$1.Y+1; A2: {p where p is n12-element XFinSequence of NAT:P0[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:8; defpred P1[XFinSequence of NAT] means 1* \$1.U > 1* \$1.Y+0; A3: {p where p is n12-element XFinSequence of NAT:P1[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:7; defpred P2[XFinSequence of NAT] means 1* \$1.X1W = 1* \$1.X1 * \$1.W; A4: {p where p is n12-element XFinSequence of NAT:P2[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:9; defpred P3[XFinSequence of NAT] means \$1.ONE = 1; A5: {p where p is n12-element XFinSequence of NAT:P3[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:14; defpred P4[XFinSequence of NAT] means 1*\$1.X1W,1*\$1.ONE are_congruent_mod 1*\$1.U; A6: {p where p is n12-element XFinSequence of NAT:P4[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:21; defpred P5[XFinSequence of NAT] means \$1.Y1= (\$1.X1) |^ (\$1.X); A7: {p where p is n12-element XFinSequence of NAT:P5[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:24; defpred P6[XFinSequence of NAT] means \$1.Y2= (\$1.X)!; A8: {p where p is n12-element XFinSequence of NAT:P6[p]} is diophantine Subset of n12 -xtuples_of NAT by Th32; defpred P7[XFinSequence of NAT] means 1*\$1.WX= 1*\$1.W+1*\$1.X+0; A9: {p where p is n12-element XFinSequence of NAT:P7[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:11; defpred P8[XFinSequence of NAT] means \$1.WX >= \$1.X & \$1.Y3= \$1.WX choose \$1.X; A10: {p where p is n12-element XFinSequence of NAT:P8[p]} is diophantine Subset of n12 -xtuples_of NAT by Th30; defpred P9[XFinSequence of NAT] means 1* \$1.Y1Y2 = 1* \$1.Y1 * \$1.Y2; A11: {p where p is n12-element XFinSequence of NAT:P9[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:9; defpred PA[XFinSequence of NAT] means 1* \$1.Y1Y2Y3 = 1* \$1.Y1Y2 * \$1.Y3; A12: {p where p is n12-element XFinSequence of NAT:PA[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:9; defpred PB[XFinSequence of NAT] means 1*\$1.Y1Y2Y3,1*\$1.Y are_congruent_mod 1*\$1.U; A13: {p where p is n12-element XFinSequence of NAT:PB[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:21; defpred PC[XFinSequence of NAT] means 1* \$1.X1X = 1* \$1.X1 * \$1.X; A14: {p where p is n12-element XFinSequence of NAT:PC[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:9; defpred PD[XFinSequence of NAT] means 1* \$1.Y4 = 1* \$1.X1X +1; A15: {p where p is n12-element XFinSequence of NAT:PD[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:6; defpred PE[XFinSequence of NAT] means \$1.Y5= (\$1.Y4) |^ (\$1.X); A16: {p where p is n12-element XFinSequence of NAT:PE[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:24; defpred PF[XFinSequence of NAT] means 1* \$1.U > 1* \$1.Y5+0; A17: {p where p is n12-element XFinSequence of NAT:PF[p]} is diophantine Subset of n12 -xtuples_of NAT by HILB10_3:7; defpred C1[XFinSequence of NAT] means P0[\$1] & P1[\$1]; A18: {p where p is n12-element XFinSequence of NAT:C1[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A2,A3); defpred C2[XFinSequence of NAT] means C1[\$1] & P2[\$1]; A19: {p where p is n12-element XFinSequence of NAT:C2[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A18,A4); defpred C3[XFinSequence of NAT] means C2[\$1] & P3[\$1]; A20: {p where p is n12-element XFinSequence of NAT:C3[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A19,A5); defpred C4[XFinSequence of NAT] means C3[\$1] & P4[\$1]; A21: {p where p is n12-element XFinSequence of NAT:C4[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A20,A6); defpred C5[XFinSequence of NAT] means C4[\$1] & P5[\$1]; A22: {p where p is n12-element XFinSequence of NAT:C5[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A21,A7); defpred C6[XFinSequence of NAT] means C5[\$1] & P6[\$1]; A23: {p where p is n12-element XFinSequence of NAT:C6[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A22,A8); defpred C7[XFinSequence of NAT] means C6[\$1] & P7[\$1]; A24: {p where p is n12-element XFinSequence of NAT:C7[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A23,A9); defpred C8[XFinSequence of NAT] means C7[\$1] & P8[\$1]; A25: {p where p is n12-element XFinSequence of NAT:C8[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A24,A10); defpred C9[XFinSequence of NAT] means C8[\$1] & P9[\$1]; A26: {p where p is n12-element XFinSequence of NAT:C9[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A25,A11); defpred CA[XFinSequence of NAT] means C9[\$1] & PA[\$1]; A27: {p where p is n12-element XFinSequence of NAT:CA[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A26,A12); defpred CB[XFinSequence of NAT] means CA[\$1] & PB[\$1]; A28: {p where p is n12-element XFinSequence of NAT:CB[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A27,A13); defpred CC[XFinSequence of NAT] means CB[\$1] & PC[\$1]; A29: {p where p is n12-element XFinSequence of NAT:CC[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A28,A14); defpred CD[XFinSequence of NAT] means CC[\$1] & PD[\$1]; A30: {p where p is n12-element XFinSequence of NAT:CD[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A29,A15); defpred CE[XFinSequence of NAT] means CD[\$1] & PE[\$1]; A31: {p where p is n12-element XFinSequence of NAT:CE[p]} is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A30,A16); defpred CF[XFinSequence of NAT] means CE[\$1] & PF[\$1]; set PP = {p where p is n12-element XFinSequence of NAT:CF[p]}; A32: PP is diophantine Subset of n12 -xtuples_of NAT from HILB10_3:sch 3(A31,A17); reconsider PPn = {p|n where p is n12-element XFinSequence of NAT:p in PP} as diophantine Subset of n -xtuples_of NAT by NAT_1:11,HILB10_3:5,A32; A33: PPn c= RR proof let x be object; assume x in PPn; then consider p be n12-element XFinSequence of NAT such that A34: x= p|n & p in PP; ex q be n12-element XFinSequence of NAT st q=p & CF[q] by A34; then A35: R[p] by Th20; (p|n).X1 = p.i1 & (p|n).X = p.i2 & (p|n).Y = p.i3 by A1,HILB10_3:4; hence thesis by A35,A34; end; RR c= PPn proof let x be object; assume x in RR; then consider p such that A36: x=p & R[p]; consider u,w,y1,y2,y3,y4,y5 be Nat such that A37: u > p.i3 & (p.i1)*w,1 are_congruent_mod u & y1 = (p.i1)|^(p.i2) & y2= (p.i2)! & y3 = (w+(p.i2)) choose (p.i2) & y1*y2*y3,p.i3 are_congruent_mod u & y4=1+(p.i1)*(p.i2) & y5 = y4|^(p.i2) & u > y5 by A36,Th20; reconsider u,w,n,y1,y2,y3,y4,y5 as Element of NAT by ORDINAL1:def 12; reconsider x1w = (p.i1)*w,wx=w+(p.i2), y12=y1*y2,y123=y1*y2*y3, x1x=(p.i1)*(p.i2),One=1 as Element of NAT; set Y1 = <%u%>^<%w%>^<%y1%>^<%y2%>^<%y3%>^<%y4%>^<%y5%>^<%x1w%>^<%wx%>, Y2=<%y12%>^<%y123%>^<%x1x%>^<%One%>; set Y = Y1 ^Y2; set PY = p ^ Y; reconsider PY as XFinSequence of NAT; A38: len p = n & len Y = 13 & len Y1=9 & len Y2=4 by CARD_1:def 7; A39: PY|n =p by A38,AFINSQ_1:57; A40: PY.i2 = (PY|n).i2 by A1,HILB10_3:4 .= p.i2 by A38,AFINSQ_1:57; 0 in dom Y by AFINSQ_1:66; then A41: PY.(n+0) = Y.0 by A38,AFINSQ_1:def 3 .= Y1.0 by A38,AFINSQ_1:51 .= u by AFINSQ_1:50; 1 in dom Y by A38,AFINSQ_1:66; then A42: PY.(n+1) = Y.1 by A38,AFINSQ_1:def 3 .= Y1.1 by A38,AFINSQ_1:51 .= w by AFINSQ_1:50; 2 in dom Y by A38,AFINSQ_1:66; then A43: PY.(n+2) = Y.2 by A38,AFINSQ_1:def 3 .= Y1.2 by A38,AFINSQ_1:51 .= y1 by AFINSQ_1:50; 3 in dom Y by A38,AFINSQ_1:66; then A44: PY.(n+3) = Y.3 by A38,AFINSQ_1:def 3 .= Y1.3 by A38,AFINSQ_1:51 .= y2 by AFINSQ_1:50; 4 in dom Y by A38,AFINSQ_1:66; then A45: PY.(n+4) = Y.4 by A38,AFINSQ_1:def 3 .= Y1.4 by A38,AFINSQ_1:51 .= y3 by AFINSQ_1:50; 5 in dom Y by A38,AFINSQ_1:66; then A46: PY.(n+5) = Y.5 by A38,AFINSQ_1:def 3 .= Y1.5 by A38,AFINSQ_1:51 .= y4 by AFINSQ_1:50; 6 in dom Y by A38,AFINSQ_1:66; then A47: PY.(n+6) = Y.6 by A38,AFINSQ_1:def 3 .= Y1.6 by A38,AFINSQ_1:51 .= y5 by AFINSQ_1:50; 7 in dom Y by A38,AFINSQ_1:66; then A48: PY.(n+7) = Y.7 by A38,AFINSQ_1:def 3 .= Y1.7 by A38,AFINSQ_1:51 .= x1w by AFINSQ_1:50; 8 in dom Y by A38,AFINSQ_1:66; then A49: PY.(n+8) = Y.8 by A38,AFINSQ_1:def 3 .= Y1.8 by A38,AFINSQ_1:51 .= wx by AFINSQ_1:50; A50: 9 in dom Y & 0 in dom Y2 by A38,AFINSQ_1:66; then A51: PY.(n+9) = Y.(9+0) by A38,AFINSQ_1:def 3 .= Y2.0 by A38,A50,AFINSQ_1:def 3 .= y12 by AFINSQ_1:45; A52: 10 in dom Y & 1 in dom Y2 by A38,AFINSQ_1:66; then A53: PY.(n+10) = Y.(9+1) by A38,AFINSQ_1:def 3 .= Y2.1 by A38,A52,AFINSQ_1:def 3 .= y123 by AFINSQ_1:45; A54: 11 in dom Y & 2 in dom Y2 by A38,AFINSQ_1:66; then A55: PY.(n+11) = Y.(9+2) by A38,AFINSQ_1:def 3 .= Y2.2 by A38,A54,AFINSQ_1:def 3 .= x1x by AFINSQ_1:45; A56: 12 in dom Y & 3 in dom Y2 by A38,AFINSQ_1:66; then A57: PY.(n+12) = Y.(9+3) by A38,AFINSQ_1:def 3 .= Y2.3 by A38,A56,AFINSQ_1:def 3 .= One by AFINSQ_1:45; CF[PY] by A36,A37,A39,A1,HILB10_3:4,A40,A41,A42,A43,A44,A45,A46,A47, A48,A49,A51,A53,A55,A57,NAT_1:11; then PY in PP; hence thesis by A39,A36; end; hence thesis by A33,XBOOLE_0:def 10; end; theorem Th35: for i1,i2,i3 holds {p: p.i3 = Product (1+((p.i1) * idseq (p.i2))) & p.i1 >= 1} is diophantine Subset of n -xtuples_of NAT proof let i1,i2,i3;set n12=n+13; defpred R[XFinSequence of NAT] means \$1.i3 = Product (1+((\$1.i1) * idseq (\$1.i2))) & \$1.i1 >= 1; set RR = {p: R[p] }; per cases; suppose A1:n=0; RR c= n -xtuples_of NAT proof let x be object; assume x in RR; then ex p be n-element XFinSequence of NAT st x= p & R[p]; hence thesis by HILB10_2:def 5; end; hence thesis by A1; end; suppose n<>0; hence thesis by Th34; end; end; theorem for n,i1,i2,i3 holds {p: p.i3 = Product (1+((p.i1)! * idseq (1+p.i2)))} is diophantine Subset of n -xtuples_of NAT proof deffunc F1(Nat,Nat,Nat) = \$1!; A1: for i1,i2,i3,i4 holds {p : F1(p.i1,p.i2,p.i3) = p.i4} is diophantine Subset of n -xtuples_of NAT by Th32; defpred P1[Nat,Nat,natural object,Nat,Nat,Nat] means \$1 = Product (1+((\$3) * idseq (\$2))) & \$3 >= 1; A2: for i1,i2,i3,i4,i5,i6 holds {p : P1[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]} is diophantine Subset of n -xtuples_of NAT by Th35; A3: 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(A2,A1); deffunc F2(Nat,Nat,Nat) = 1*\$1+1; A4: for 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_3:15; defpred P2[Nat,Nat,natural object,Nat,Nat,Nat] means \$1 = Product (1+((\$2!) * idseq (\$3))) & \$2! >= 1; A5: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 A3; A6: 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(A5,A4); let n,i1,i2,i3; defpred Q1[XFinSequence of NAT] means P2[\$1.i3,\$1.i1,1*\$1.i2+1,1*\$1.i3,\$1.i3,\$1.i3]; defpred Q2[XFinSequence of NAT] means \$1.i3 = Product (1+((\$1.i1)! * idseq (1+\$1.i2))); A7: for p holds Q1[p] iff Q2[p] by NAT_1:14; {p : Q1[p]} = {q :Q2[q]} from HILB10_3:sch 2(A7); hence thesis by A6; end; theorem Th37: for i1,i2,i3 st n<>0 holds {p: p.i3 = Product ( (p.i2+1)+(-idseq (p.i1))) & p.i2 > p.i1} is diophantine Subset of n -xtuples_of NAT proof let i1,i2,i3;set n2=n+2; defpred R[XFinSequence of NAT] means \$1.i3 = Product(((\$1.i2)+1)+(-idseq (\$1.i1))) & \$1.i2 > \$1.i1; set RR = {p: R[p] }; assume A1: n<>0; n=n+0;then reconsider Y=i3,X2=i2,X1=i1,C=n,F=n+1 as Element of n2 by HILB10_3:2,3; defpred P1[XFinSequence of NAT] means \$1.X2 >= \$1.X1 & \$1.C = (\$1.X2) choose (\$1.X1); A2: {p where p is n2-element XFinSequence of NAT:P1[p]} is diophantine Subset of n2 -xtuples_of NAT by Th30; defpred P2[XFinSequence of NAT] means \$1.F=(\$1.X1)!; A3: {p where p is n2-element XFinSequence of NAT:P2[p]} is diophantine Subset of n2 -xtuples_of NAT by Th32; defpred P3[XFinSequence of NAT] means 1*\$1.X2 > 1*\$1.X1+0; A4: {p where p is n2-element XFinSequence of NAT:P3[p]} is diophantine Subset of n2 -xtuples_of NAT by HILB10_3:7; defpred P4[XFinSequence of NAT] means 1*\$1.Y = 1* (\$1 .F) * (\$1 .C); A5: {p where p is n2-element XFinSequence of NAT:P4[p]} is diophantine Subset of n2 -xtuples_of NAT by HILB10_3:9; defpred P12[XFinSequence of NAT] means P1[\$1] & P2[\$1]; A6: {p where p is n2-element XFinSequence of NAT:P12[p]} is diophantine Subset of n2 -xtuples_of NAT from HILB10_3:sch 3(A2,A3); defpred P123[XFinSequence of NAT] means P12[\$1] & P3[\$1]; A7: {p where p is n2-element XFinSequence of NAT:P123[p]} is diophantine Subset of n2 -xtuples_of NAT from HILB10_3:sch 3(A6,A4); defpred P1234[XFinSequence of NAT] means P123[\$1] & P4[\$1]; set PP = {p where p is n2-element XFinSequence of NAT:P1234[p]}; A8: PP is diophantine Subset of n2 -xtuples_of NAT from HILB10_3:sch 3(A7,A5); reconsider PPn = {p | n where p is n2-element XFinSequence of NAT: p in PP} as diophantine Subset of n -xtuples_of NAT by NAT_1:11,HILB10_3:5,A8; A9: PPn c= RR proof let x be object; assume x in PPn; then consider p be n2-element XFinSequence of NAT such that A10: x= p|n & p in PP; ex q be n2-element XFinSequence of NAT st q=p & P1234[q] by A10; then A11: R[p] by Th23; (p|n).X2 = p.i2 & (p|n).X1 = p.i1 & (p|n).Y=p.i3 by A1,HILB10_3:4; hence thesis by A11,A10; end; RR c= PPn proof let x be object; assume x in RR; then consider p such that A12: x=p & R[p]; reconsider F=(p.i1)!,C=(p.i2) choose (p.i1) as Element of NAT; set Y = <%C,F%>;set PY = p ^ Y; A13: len p = n & len Y = 2 by CARD_1:def 7; A14: PY|n =p by A13,AFINSQ_1:57; A15: PY.i2 = (PY|n).i2 by A1,HILB10_3:4 .= p.i2 by A13,AFINSQ_1:57; A16: PY.i3 = (PY|n).i3 by A1,HILB10_3:4 .= p.i3 by A13,AFINSQ_1:57; 0 in dom Y by AFINSQ_1:66; then A17: PY.(n+0) = Y.0 by A13,AFINSQ_1:def 3 .= C; 1 in dom Y by A13,AFINSQ_1:66; then A18:PY.(n+1) = Y.1 by A13,AFINSQ_1:def 3 .= F; P1234[PY] by A12,A14,A1,HILB10_3:4,A16,A15,A17,A18, Th23; then PY in PP; hence thesis by A14,A12; end; hence thesis by A9,XBOOLE_0:def 10; end; theorem for i1,i2,i3 holds {p: p.i3 = Product ( (p.i2+1)+(-idseq (p.i1))) & p.i2 > p.i1} is diophantine Subset of n -xtuples_of NAT proof let i1,i2,i3;set n2=n+2; defpred R[XFinSequence of NAT] means \$1.i3 = Product(((\$1.i2)+1)+(-idseq (\$1.i1))) & \$1.i2 > \$1.i1; set RR = {p: R[p] }; per cases; suppose A1:n=0; RR c= n -xtuples_of NAT proof let x be object;assume x in RR; then ex p be n-element XFinSequence of NAT st x= p & R[p]; hence thesis by HILB10_2:def 5; end; hence thesis by A1; end; suppose n<>0; hence thesis by Th37; end; end; theorem for i,n1,n2,n,i1 holds {p: p.i1 = Product (i+((p/^n1) | n2))} is diophantine Subset of n -xtuples_of NAT proof let i,n1,n2; defpred P[Nat] means for n st \$1 +n1 <= n for i1 holds{p: p.i1 = Product (i+((p/^n1) | \$1))} is diophantine Subset of n -xtuples_of NAT; A1: P[0] proof let n; assume 0 +n1 <= n; let i1; defpred Q1[XFinSequence of NAT] means \$1.i1 = Product (i+((\$1/^n1) | 0)); defpred Q2[XFinSequence of NAT] means \$1.i1 = 1; A2: for p holds Q1[p] iff Q2[p] by Th4; {p : Q1[p]} = {q :Q2[q]} from HILB10_3:sch 2(A2); hence thesis by HILB10_3:14; end; A3: P[m] implies P[m+1] proof assume A4: P[m]; let n such that A5: m+1 +n1 <= n; set m1=m+1,X=n+1; let i1; m < m1 by NAT_1:13; then n1 + m < n1 + m1 by XREAL_1:8; then A6: n1 + m < n by A5,XXREAL_0:2; then n1+m in Segm n by NAT_1:44; then reconsider n1m=n1+m as Element of n; A7: n < X by NAT_1:13; then n in Segm X by NAT_1:44; then reconsider N=n,I1=i1,N1M=n1m as Element of X by HILB10_3:2; defpred P[XFinSequence of NAT] means \$1.N = Product (i+((\$1/^n1) | m)); defpred Q[XFinSequence of NAT] means \$1.I1 = (1*\$1.N1M + i)*(\$1.N); n1+m <= X by A6,NAT_1:13; then A8: {p where p is X-element XFinSequence of NAT:P[p]} is diophantine Subset of X -xtuples_of NAT by A4; A9: {p where p is X-element XFinSequence of NAT:Q[p]} is diophantine Subset of X -xtuples_of NAT by Th25; set PQ={p where p is X-element XFinSequence of NAT:P[p]&Q[p]}; A10:PQ is diophantine Subset of X -xtuples_of NAT from HILB10_3:sch 3(A8,A9); set PQr = {p|n where p is X-element XFinSequence of NAT: p in PQ}; set S={p: p.i1 = Product (i+((p/^n1) | m1))}; A11: PQr is diophantine Subset of n -xtuples_of NAT by HILB10_3:5,A7,A10; A12: n1 <= n1 + m1 <= n by A5,NAT_1:11; then A13: n-'n1 = n-n1 by XXREAL_0:2,XREAL_1:233; A14: m1 <= n-n1 by A5,XREAL_1:19; m= m1 by A14,A13,AFINSQ_2:def 2; then len ((p/^n1) | m1)=m1 by AFINSQ_1:54; then A20: (p/^n1) | m1 = (((p/^n1) | m1)|m) ^<%((p/^n1) | m1).m%> by AFINSQ_1:56; ((p/^n1) | m1)|m= (p/^n1)|m & ((p/^n1) | m1).m = (p/^n1).m & m in dom (p/^n1) by A19,AFINSQ_1:53, RELAT_1:74,A15; then (p/^n1) | m1 = ((p/^n1)|m) ^<%p.n1m%> by A20,AFINSQ_2:def 2; then i+((p/^n1) | m1) = (i+((p/^n1)|m)) ^(i+<%p.n1m%>) by Th8 .= (i+((p/^n1)|m)) ^<%i+p.n1m%> by Th9; then A21: Product(i+((p/^n1) | m1)) = Product(i+((p/^n1) | m)) * Product<%i+p.n1m%> by Th7 .= Product(i+((p/^n1) | m))* (i+p.n1m) by Th5; reconsider P=Product(i+((p/^n1) |m)) as Element of NAT by ORDINAL1:def 12; reconsider pP = p^<%P%> as X-element XFinSequence of NAT; A22: len (p/^n1) >m by A19,NAT_1:13; A23: (pP/^n1)|m = ((p/^n1)^<%P%>)|m by Th10,A18,A12,XXREAL_0:2 .= (p/^n1)|m by AFINSQ_1:58,A22; A24: pP|n = p by A18,AFINSQ_1:57; A25: pP.I1 = p.i1 & pP.N1M = p.n1m by A5,A24,HILB10_3:4; P[pP] & Q[pP] by A23,A25,A21,A18,AFINSQ_1:36,A17; then pP in PQ; hence thesis by A17,A24; end; PQr c= S proof let y be object; assume y in PQr; then consider pP be X-element XFinSequence of NAT such that A26: y=pP|n & pP in PQ; A27: ex q be X-element XFinSequence of NAT st pP=q & P[q] & Q[q] by A26; A28: len pP=X by CARD_1:def 7; A29: len (pP|n) = n by CARD_1:def 7; set p=pP|n; A30: len (p/^n1) >= m1 by A14,A13,A29,AFINSQ_2:def 2; then len ((p/^n1) | m1)=m1 by AFINSQ_1:54; then A31: (p/^n1) | m1 = (((p/^n1) | m1)|m) ^<%((p/^n1) | m1).m%> by AFINSQ_1:56; ((p/^n1) | m1)|m= (p/^n1)|m & ((p/^n1) | m1).m = (p/^n1).m & m in dom (p/^n1) by A30,AFINSQ_1:53,RELAT_1:74,A15; then (p/^n1) | m1 = ((p/^n1)|m) ^<%p.n1m%> by A31,AFINSQ_2:def 2; then i+((p/^n1) | m1) = (i+((p/^n1)|m)) ^(i+<%p.n1m%>) by Th8 .= (i+((p/^n1)|m)) ^<%i+p.n1m%> by Th9; then A32: Product(i+((p/^n1) | m1)) = Product(i+((p/^n1) | m)) * Product<%i+p.n1m%> by Th7 .= Product(i+((p/^n1) | m))* (i+p.n1m) by Th5; set P = Product(i+((p/^n1) | m)); A33: pP = p ^<%pP.n%> by A28,AFINSQ_1:56; A34: len (p/^n1) >m by A30,NAT_1:13; A35: (pP/^n1)|m = ((p/^n1)^<%pP.n%>)|m by A33,Th10,A29,A12,XXREAL_0:2 .= (p/^n1)|m by AFINSQ_1:58,A34; pP.I1 = p.i1 & pP.N1M = p.n1m by A5,HILB10_3:4; hence thesis by A26,A35,A32,A27; end; hence thesis by A11,A16,XBOOLE_0:def 10; end; A36: P[m] from NAT_1:sch 2(A1,A3); let n,i1; per cases; suppose n1+n2 <= n; hence thesis by A36; end; suppose n1+n2 > n; then A37: n-n1 < n2 by XREAL_1:19; per cases; suppose A38: n1 >=n; defpred Q1[XFinSequence of NAT] means \$1.i1 = Product (i+((\$1/^n1) |n2)); defpred Q2[XFinSequence of NAT] means \$1.i1 = 1; A39: for p holds Q1[p] iff Q2[p] proof let p; len p = n by CARD_1:def 7; then p/^n1={} by A38,AFINSQ_2:6; then i+((p/^n1) | n2) ={}; hence thesis by Th4; end; {p:Q1[p]} = {q:Q2[q]} from HILB10_3:sch 2(A39); hence thesis by HILB10_3:14; end; suppose A40: n1 < n; then reconsider N = n-n1 as Nat by NAT_1:21; defpred Q1[XFinSequence of NAT] means \$1.i1 = Product (i+((\$1/^n1) |n2)); defpred Q2[XFinSequence of NAT] means \$1.i1 = Product (i+((\$1/^n1) | N)); A41: for p holds Q1[p] iff Q2[p] proof let p; len p = n by CARD_1:def 7; then len (p/^n1) = n-n1 by A40,AFINSQ_2:7; hence thesis by A37,AFINSQ_1:52; end; A42: {p:Q1[p]} = {q:Q2[q]} from HILB10_3:sch 2(A41); n1+N=n; hence thesis by A42,A36; end; end; end;