:: Pocklington's Theorem and {B}ertrand's Postulate :: by Marco Riccardi :: :: Received May 17, 2006 :: Copyright (c) 2006-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, XREAL_0, CARD_1, XXREAL_0, RELAT_1, ARYTM_3, NAT_1, NEWTON, INT_1, SUBSET_1, ARYTM_1, REALSET1, ABIAN, FINSEQ_1, FINSEQ_2, ORDINAL4, CARD_3, FUNCT_1, INT_2, NAT_3, XBOOLE_0, PRE_POLY, POWER, PEPIN, SQUARE_1, TARSKI, FINSET_1, MEMBERED, REAL_1, COMPLEX1, PREPOWER, FUNCT_7, XCMPLX_0; notations SUBSET_1, XXREAL_0, PREPOWER, TARSKI, XBOOLE_0, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, INT_1, ABIAN, SQUARE_1, NEWTON, FINSET_1, PEPIN, NAT_3, RELAT_1, FUNCT_1, FINSEQ_1, RVSUM_1, WSIERP_1, TREES_4, XXREAL_2, POWER, MEMBERED, INT_2, FINSEQ_2, RECDEF_1, PRE_POLY, REAL_1, NAT_1, NAT_D; constructors REAL_1, NAT_D, PREPOWER, POWER, WSIERP_1, ABIAN, PEPIN, NAT_3, RECDEF_1, BINOP_2, XXREAL_2, RELSET_1, NUMBERS; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON, NAT_3, VALUED_0, VALUED_1, XXREAL_2, CARD_1, SQUARE_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Some theorems on real and Nats. theorem :: NAT_4:1 for r,s being Real holds 0<=r & s*s1 holds a|^n > n; theorem :: NAT_4:4 for n,k,m being Nat st k <= n & m = [\ n/2 /] holds n choose m >= n choose k; theorem :: NAT_4:5 for n,m being Nat st m=[\ n/2 /] & n>=2 holds n choose m >= 2|^n / n; theorem :: NAT_4:6 for n being Nat holds 2*n choose n >= 4|^n / (2*n); theorem :: NAT_4:7 for n,p being Nat holds p>0 & n divides p & n <> 1 & n <> p implies 1 < n & n < p; theorem :: NAT_4:8 for p being Nat holds (ex n being Element of NAT st n divides p & 10 & b<>0 implies q|^n gcd b = 1; theorem :: NAT_4:11 for a,b,c being Nat holds a|^(2*b) mod c = (a|^b mod c)*(a|^b mod c) mod c; theorem :: NAT_4:12 for p being Nat holds not p is prime iff p<=1 or ex n being Element of NAT st n divides p & 11 & for n being Element of NAT holds 1=1 & p is prime implies a,p are_coprime; theorem :: NAT_4:16 for p being Prime, a being Element of NAT, x being set st a<>0 & x=p |^ ( p |-count a) holds ex b being Element of NAT st b=x & 1 <= b & b <= a; theorem :: NAT_4:17 for k,q,n,d being Element of NAT holds q is prime & d divides k* q|^(n+1) & not d divides k*q|^n implies q|^(n+1) divides d; theorem :: NAT_4:18 for q1,q,n1 being Element of NAT st q1 divides q|^n1 & q is prime & q1 is prime holds q=q1; theorem :: NAT_4:19 for p being Prime, n being Nat st n

0 holds p1=p2; begin :: Pocklington's theorem. theorem :: NAT_4:23 for n,k,q,p,n1,p,a being Element of NAT st n-1=k*q|^n1 & k>0 & n1>0 & q is prime & a|^(n-'1) mod n = 1 & p is prime & p divides n holds p divides (a|^((n-'1) div q) -' 1) or p mod q|^n1 = 1; theorem :: NAT_4:24 for n,f,c being Element of NAT st n-1=f*c & f>c & c>0 & (for q being Element of NAT st q divides f & q is prime holds ex a being Element of NAT st a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1) holds n is prime ; ::$N Pocklington's theorem theorem :: NAT_4:25 for n,f,d,n1,a,q being Element of NAT st n-1=q|^n1*d & q|^n1>d & d>0 & q is prime & a|^(n-'1) mod n = 1 & (a|^((n-'1) div q)-'1) gcd n = 1 holds n is prime; begin :: Some prime numbers. theorem :: NAT_4:26 7 is prime; theorem :: NAT_4:27 11 is prime; theorem :: NAT_4:28 13 is prime; theorem :: NAT_4:29 19 is prime; theorem :: NAT_4:30 23 is prime; theorem :: NAT_4:31 37 is prime; theorem :: NAT_4:32 43 is prime; theorem :: NAT_4:33 83 is prime; theorem :: NAT_4:34 139 is prime; theorem :: NAT_4:35 163 is prime; theorem :: NAT_4:36 317 is prime; theorem :: NAT_4:37 631 is prime; theorem :: NAT_4:38 1259 is prime; theorem :: NAT_4:39 2503 is prime; theorem :: NAT_4:40 4001 is prime; begin :: Some theorems on finite sequence of numbers. ::$CT theorem :: NAT_4:42 for F being FinSequence of REAL st (for k being Element of NAT st k in dom F holds F.k > 0) holds Product F > 0; theorem :: NAT_4:43 for X1 being set, X2 being finite set st X1 c= X2 & X2 c= NAT & not {} in X2 holds Product Sgm X1 <= Product Sgm X2; theorem :: NAT_4:44 for a,k being Element of NAT, X being set, F being FinSequence of SetPrimes, p being Prime st X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F holds (p in rng F implies p |-count a = 1) & (not p in rng F implies p |-count a = 0); theorem :: NAT_4:45 for n being Element of NAT holds Product Sgm{p where p is prime Element of NAT:p<=n+1} <= 4 to_power n; theorem :: NAT_4:46 for x being Real st x>=2 holds Product Sgm{p where p is prime Element of NAT:p<=x} <= 4 to_power (x-1); theorem :: NAT_4:47 for n being Element of NAT, p being Prime st n<>0 ex f being FinSequence of NAT st len f = n & (for k being Element of NAT st k in dom f holds (f.k=1 iff p|^k divides n) & (f.k=0 iff not p|^k divides n)) & p |-count n = Sum f; theorem :: NAT_4:48 for n being Element of NAT, p being Prime ex f being FinSequence of NAT st len f = n & (for k being Element of NAT st k in dom f holds f.k=[\ n/ (p|^k) /]) & p |-count (n!) = Sum f; theorem :: NAT_4:49 for n being Element of NAT, p being Prime ex f being FinSequence of REAL st len f = 2*n & (for k being Element of NAT st k in dom f holds f.k=[\ (2*n)/(p|^k)/] - 2*[\n/(p|^k)/]) & p |-count (2*n choose n) = Sum f; definition let f be FinSequence of NAT,p be Prime; func p |-count f -> FinSequence of NAT means :: NAT_4:def 1 len it = len f & for i being set st i in dom it holds it.i = p |-count f.i; end; theorem :: NAT_4:50 for p being Prime, f being FinSequence of NAT st f={} holds p |-count f = {}; theorem :: NAT_4:51 for p being Prime, f1,f2 being FinSequence of NAT holds p |-count (f1^f2) = (p |-count f1)^(p |-count f2); theorem :: NAT_4:52 for p being Prime, n being non zero Element of NAT holds p |-count <*n*> = <* (p |-count n) *>; theorem :: NAT_4:53 for f being FinSequence of NAT, p being Prime st Product f <> 0 holds p |-count (Product f) = Sum (p |-count f); theorem :: NAT_4:54 for f1,f2 being FinSequence of REAL st len f1 = len f2 & (for k being Element of NAT st k in dom f1 holds f1.k<=f2.k & f1.k>0) holds Product f1 <= Product f2; theorem :: NAT_4:55 for n being Element of NAT, r being Real st r>0 holds Product (n |-> r) = r to_power n; scheme :: NAT_4:sch 1 scheme1 { P[set,set,set] } : for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} holds Product Sgm X > 0; scheme :: NAT_4:sch 2 scheme2 { P[set,set,set] } : for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} & not p|^(p |-count m) in X holds p |-count (Product Sgm X) = 0; scheme :: NAT_4:sch 3 scheme3 { P[set,set,set] } : for p being Prime, n being Element of NAT, m being non zero Element of NAT, X being set st X = {p9|^(p9 |-count m) where p9 is prime Element of NAT: P[n,m,p9]} & p|^(p |-count m) in X holds p |-count ( Product Sgm X) = p |-count m; scheme :: NAT_4:sch 4 scheme4 { A(set,set) -> set, P[set,set] } : for n,m being Element of NAT, r being Real, X being finite set st X = {A(p,m) where p is prime Element of NAT: p <= r & P[p,m]} & r>=0 holds card X <= [\ r /]; begin :: Bertrand's postulate. ::$N Bertrand's postulate theorem :: NAT_4:56 for n being Element of NAT st n>=1 holds ex p being Prime st n