:: Prime Representing Polynomial :: by Karol P\kak :: :: Received November 30, 2021 :: Copyright (c) 2021 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, FUNCT_1, XXREAL_0, NAT_1, INT_1, ARYTM_3, ZFMISC_1, CARD_1, ORDINAL1, ARYTM_1, AFINSQ_1, COMPLEX1, SQUARE_1, NEWTON, HILB10_2, INT_2, REAL_1, CARD_3, REALSET1, PELLS_EQ, PYTHTRIP, MCART_1, HILB10_1, ABSVALUE, POWER; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, XCMPLX_0, FINSEQ_1, XXREAL_0, XREAL_0, INT_1, AFINSQ_1, SQUARE_1, NEWTON, POWER, HILB10_2, RVSUM_1, CARD_1, NAT_D, PELLS_EQ, PYTHTRIP, ABSVALUE, HILB10_1, ZFMISC_1, XTUPLE_0, INT_2; constructors NAT_D, RECDEF_1, RELSET_1, NEWTON, HILB10_2, WSIERP_1, INT_6, PELLS_EQ, DOMAIN_1, PEPIN, ABSVALUE, ABIAN, POWER, HILB10_1; registrations RELAT_1, ORDINAL1, XREAL_0, NAT_1, VALUED_0, INT_1, AFINSQ_1, HILB10_2, XXREAL_0, XCMPLX_0, NEWTON, NEWTON02, NAT_6, FINSEQ_1, NEWTON04, INT_6, NEWTON03, PYTHTRIP, ABIAN, ABSVALUE, POWER, HILB10_1, XTUPLE_0, FOMODEL0; requirements NUMERALS, SUBSET, ARITHM, REAL; begin :: The Prime Number Set as a Diophantine Set reserve n for Nat, i,j,i1,i2,i3,i4,i5,i6 for Element of n, p,q,r for n-element XFinSequence of NAT; theorem :: HILB10_6:1 for i holds {p: p.i > 1} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_6:2 for i,j holds {p: p.i = (p.j-'1)! + 1} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_6:3 for i holds {p: (p.i-'1)! + 1 mod p.i = 0 & p.i > 1} is diophantine Subset of n -xtuples_of NAT; theorem :: HILB10_6:4 for n being Nat,i being Element of n holds {p where p is n-element XFinSequence of NAT: p.i is prime} is diophantine Subset of n -xtuples_of NAT; begin :: Special Case of Pell's Equation - Selected Properties reserve i,j,n,n1,n2,m,k,l,u,e,p,t for Nat, a,b for non trivial Nat, x,y for Integer, r,q for Real; theorem :: HILB10_6:5 2 <= e & (ex i st e^2 *(e *(e+2))* (n+1)^2 +1 = i^2) implies e - 1 + e |^ (e-'2) <= n; theorem :: HILB10_6:6 2 <= e & 0 =k implies n choose k >= (n+1-k) |^k /(k!); theorem :: HILB10_6:8 n >=k implies n choose k <= (n|^k) / (k!); theorem :: HILB10_6:9 i <= j & 2*j <= n+1 implies n choose i <= n choose j; theorem :: HILB10_6:10 k <=n implies n! <= k! * n |^ (n-'k); theorem :: HILB10_6:11 0 < k & (2*k) |^k <=n & n|^k < p implies ((p+1) |^n) mod (p|^(k+1)) >0 & k! < ((n+1) |^ k * p|^k) / ( (p+1) |^n mod p|^(k+1)) < k!+1; theorem :: HILB10_6:12 Px(a,n+2) = 2*a*Px(a,n+1) - Px(a,n) & Py(a,n+2) = 2*a*Py(a,n+1) - Py(a,n); theorem :: HILB10_6:13 Px(a,n), p|^n + Py(a,n)*(a-p) are_congruent_mod 2*a*p-p^2-1; theorem :: HILB10_6:14 0 < p|^n < a implies p|^n + Py(a,n)*(a-p) <= Px(a,n); theorem :: HILB10_6:15 a <= b implies Px(a,n) <= Px(b,n) & Py(a,n) <= Py(b,n); theorem :: HILB10_6:16 a,b are_congruent_mod k implies Px(a,n),Px(b,n) are_congruent_mod k; theorem :: HILB10_6:17 Px(a,|.2*x+y.|),- Px(a,|.y.|) are_congruent_mod Px(a,|.x.|); theorem :: HILB10_6:18 Px(a,|.4*x+y.|), Px(a,|.y.|) are_congruent_mod Px(a,|.x.|); theorem :: HILB10_6:19 k < n implies Px(a,k) < Px(a,n); theorem :: HILB10_6:20 Px(a,k) = Px(a,n) implies k = n; theorem :: HILB10_6:21 i <= j <= 2*n & Px(a,i),Px(a,j) are_congruent_mod Px(a,n) implies (i=0 & j = 2 & a=2 & n=1) or i=j; theorem :: HILB10_6:22 0 < i <= n & 0 <= j < 4*n & Px(a,i),Px(a,j) are_congruent_mod Px(a,n) implies j = i or j + i = 4*n; theorem :: HILB10_6:23 Px(a,|.4*x*n+y.|), Px(a,|.y.|) are_congruent_mod Px(a,|.x.|); theorem :: HILB10_6:24 0 < i <= n & Px(a,i),Px(a,j) are_congruent_mod Px(a,n) implies j,i are_congruent_mod 4*n or j,-i are_congruent_mod 4*n; theorem :: HILB10_6:25 Py(a,2*n) = 2* Py(a,n)*Px(a,n); begin :: Special Case of Pell's Equation - Diophantine Polynomial With 8 Variables theorem :: HILB10_6:26 for a being non trivial Nat for y,n,b,c,d,r,s,t,u,v,x being Nat st 1 <= n & [x,y] is Pell's_solution of a^2-'1 & [u,v] is Pell's_solution of a^2-'1 & [s,t] is Pell's_solution of b^2-'1 & v = 4*r*y^2 & b = a +u^2*(u^2-a) & s = x+c*u & t = n+4*d*y & n <= y holds b is non trivial & u^2 > a & y = Py(a,n); theorem :: HILB10_6:27 for a be non trivial Nat for y,n be Nat st 1 <=n holds y = Py(a,n) implies ex b,c,d,r,s,t,u,v,x be Nat st [x,y] is Pell's_solution of a^2-'1 & [u,v] is Pell's_solution of a^2-'1 & [s,t] is Pell's_solution of b^2-'1 & v = 4*r*y^2 & b =a +u^2*(u^2-a) & s = x+c*u & t = n+4*d*y & n <= y; theorem :: HILB10_6:28 for a for y,n be Nat st 1 <=n holds y= Py(a,n) iff ex c,d,r,u,x be Nat st [x,y] is Pell's_solution of a^2-'1 & u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 & (x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 & n <= y; theorem :: HILB10_6:29 for f,k be positive Nat holds f=k! iff ex j,h,w be Nat, n,p,q,z be positive Nat st q= w*z+h+j & z = f*(h+j) +h & (2*k) |^3 *(2*k+2)*(n+1) |^2+1 is square & p=(n+1) |^k & q=(p+1) |^n & z=p|^(k+1); theorem :: HILB10_6:30 for k be positive Nat holds k+1 is prime iff ex a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat st q = w*z+h+j & z = (g*k+g+k)*(h+j)+h & (2*k) |^3 *(2*k+2)*(n+1) |^2+1 =f^2 & e=p+q+z+2*n & e |^3 *(e+2)*(a+1) |^2+1 =o^2 & [x,y] is Pell's_solution of a^2-'1 & u^2 = 16*(a^2-1)*r^2*y^2*y^2+1 & (x+c*u)^2 = ((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 & [m,l] is Pell's_solution of a^2-'1 & l=k+i*(a-1) & n+l+v=y & m=p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1) & x= q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1) & p*m = z+p*l*(a-p)+t*(2*a*p-p^2-1); begin :: Prime Representing Polynomial with 26 Variables ::$N Prime Representing Polynomial theorem :: HILB10_6:31 for k be positive Nat holds k+1 is prime iff ex a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat st 0 = (w*z+h+j -q)^2 + ((g*k+g+k)*(h+j)+h-z)^2 + ((2*k) |^3 *(2*k+2)*(n+1) |^2+1 - f^2)^2 + (p+q+z+2*n-e)^2 + (e |^3 *(e+2)*(a+1) |^2+1 -o^2)^2 + (x^2-(a^2-'1)*y^2-1)^2 + (16*(a^2-1)*r^2*y^2*y^2+1 -u^2)^2+ (((a+u^2*(u^2-a))^2-1)*(n+4*d*y)^2+1 -(x+c*u)^2)^2 + (m^2-(a^2-'1)*l^2-1)^2 + (k+i*(a-1)-l)^2 + (n+l+v-y)^2 + (p+l*(a-n-1)+b*(2*a*(n+1)-(n+1)^2-1)-m)^2+ (q+y*(a-p-1)+s*(2*a*(p+1)-(p+1)^2-1)-x)^2+ (z+p*l*(a-p)+t*(2*a*p-p^2-1)-p*m)^2;