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