:: Diophantine Sets -- Preliminaries
:: 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, 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, INT_2;
requirements NUMERALS, SUBSET, ARITHM, REAL;
definitions TARSKI, PARTFUN3;
equalities FINSEQ_1, VALUED_1, ORDINAL1;
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<n;
then
A11: i in dom (X|n) by A7,AFINSQ_1:66;
Product (X|n) >= (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 <n by NAT_1:13;
then
A5: n-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;
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;
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;
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*k<n implies 1 / (1-k/n) <= 1+(2*k)/n
proof
assume
A1: 0 < 2*k < n;
k<=k+k by NAT_1:11;
then
A2: k < n by A1,XXREAL_0:2;
then
A3: n-k >0 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;
then
A5: k < n by NAT_1:13;
A6: (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)));
A7: n >= 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 <k! by XREAL_1:19;
k! <= (n|^k) / (n choose k) by A7,Lm4;
hence thesis by INT_1:def 6,A19;
end;
theorem Th18:
for x,y being Nat holds
y = x! iff
ex n,y1,y2,y3 being Nat st
y1 = (2*x) |^(x+1) &
y2 = n|^x &
y3 = n choose x &
n > 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 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;
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;
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;
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;
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;
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<m+1 by NAT_1:13;
then
A15: Segm m c= Segm m1 & m in Segm m1 by NAT_1:39,44;
A16: S c= PQr
proof
let y be object;
assume y in S;
then consider p such that
A17: y=p & p.i1 = Product (i+((p/^n1) | m1));
A18: len p=n by CARD_1:def 7;
then
A19: len (p/^n1) >= 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,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;