:: Pocklington's Theorem and {B}ertrand's Postulate :: by Marco Riccardi :: :: Received May 17, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin theorem Th1: :: NAT_4:1 for r, s being real number st 0 <= r & s * s < r * r holds s < r proofend; theorem Th2: :: NAT_4:2 for r, s being real number st 1 < r & r * r <= s holds r < s proofend; theorem Th3: :: NAT_4:3 for a, n being Nat st a > 1 holds a |^ n > n proofend; theorem Th4: :: NAT_4:4 for n, k, m being Nat st k <= n & m = [\(n / 2)/] holds n choose m >= n choose k proofend; theorem Th5: :: NAT_4:5 for n, m being Nat st m = [\(n / 2)/] & n >= 2 holds n choose m >= (2 |^ n) / n proofend; theorem Th6: :: NAT_4:6 for n being Nat holds (2 * n) choose n >= (4 |^ n) / (2 * n) proofend; theorem Th7: :: NAT_4:7 for n, p being Nat st p > 0 & n divides p & n <> 1 & n <> p holds ( 1 < n & n < p ) proofend; theorem Th8: :: NAT_4:8 for p being Nat st ex n being Element of NAT st ( n divides p & 1 < n & n < p ) holds ex n being Element of NAT st ( n divides p & 1 < n & n * n <= p ) proofend; theorem Th9: :: NAT_4:9 for i, j, k, l being Nat st i = (j * k) + l & l < j & 0 < l holds not j divides i proofend; theorem :: NAT_4:10 for n, q, b being Nat st q gcd b = 1 & q <> 0 & b <> 0 holds (q |^ n) gcd b = 1 proofend; theorem Th11: :: 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 proofend; theorem Th12: :: NAT_4:12 for p being Nat holds ( ( p <= 1 or ex n being Element of NAT st ( n divides p & 1 < n & n < p ) ) iff not p is prime ) proofend; theorem Th13: :: NAT_4:13 for n, k being Nat st n divides k & 1 < n holds ex p being Element of NAT st ( p divides k & p <= n & p is prime ) proofend; Lm1: for p being Nat holds ( ( p <= 1 or ex n being Element of NAT st ( n divides p & 1 < n & n * n <= p & n is prime ) ) iff not p is prime ) proofend; theorem Th14: :: NAT_4:14 for p being Nat holds ( p is prime iff ( p > 1 & ( for n being Element of NAT st 1 < n & n * n <= p & n is prime holds not n divides p ) ) ) proofend; theorem Th15: :: NAT_4:15 for a, p, k being Nat st (a |^ k) mod p = 1 & k >= 1 & p is prime holds a,p are_relative_prime proofend; theorem Th16: :: NAT_4:16 for p being Prime for a being Element of NAT for 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 ) proofend; theorem Th17: :: NAT_4:17 for k, q, n, d being Element of NAT st q is prime & d divides k * (q |^ (n + 1)) & not d divides k * (q |^ n) holds q |^ (n + 1) divides d proofend; theorem Th18: :: 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 proofend; theorem Th19: :: NAT_4:19 for p being Prime for n being Element of NAT st n < p holds not p divides n ! proofend; theorem Th20: :: NAT_4:20 for a, b being non empty Nat st ( for p being Element of NAT st p is prime holds p |-count a <= p |-count b ) holds ex c being Element of NAT st b = a * c proofend; theorem Th21: :: NAT_4:21 for a, b being non empty Nat st ( for p being Element of NAT st p is prime holds p |-count a = p |-count b ) holds a = b proofend; theorem Th22: :: NAT_4:22 for p1, p2 being Prime for m being non empty Element of NAT st p1 |^ (p1 |-count m) = p2 |^ (p2 |-count m) & p1 |-count m > 0 holds p1 = p2 proofend; begin theorem Th23: :: 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 & not p divides (a |^ ((n -' 1) div q)) -' 1 holds p mod (q |^ n1) = 1 proofend; theorem Th24: :: 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 proofend; :: [WP: ] Pocklington's_theorem theorem Th25: :: 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 proofend; Lm2: for n being Element of NAT st 1 < n & n < 5 & n is prime & not n = 2 holds n = 3 proofend; Lm3: for k being Element of NAT st k < 25 holds for n being Element of NAT st 1 < n & n * n <= k & n is prime & not n = 2 holds n = 3 proofend; begin theorem Th26: :: NAT_4:26 7 is prime proofend; theorem :: NAT_4:27 11 is prime proofend; theorem Th28: :: NAT_4:28 13 is prime proofend; Lm4: ( not 6 is prime & not 8 is prime & not 9 is prime & not 10 is prime & not 12 is prime & not 14 is prime & not 15 is prime & not 16 is prime & not 18 is prime & not 20 is prime & not 21 is prime & not 22 is prime & not 24 is prime & not 25 is prime & not 26 is prime & not 27 is prime & not 28 is prime ) proofend; theorem :: NAT_4:29 19 is prime proofend; theorem Th30: :: NAT_4:30 23 is prime proofend; Lm5: for n being Element of NAT st 1 < n & n < 29 & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 holds n = 23 proofend; Lm6: for k being Element of NAT st k < 841 holds for n being Element of NAT st 1 < n & n * n <= k & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 holds n = 23 proofend; theorem Th31: :: NAT_4:31 37 is prime proofend; theorem Th32: :: NAT_4:32 43 is prime proofend; theorem Th33: :: NAT_4:33 83 is prime proofend; theorem Th34: :: NAT_4:34 139 is prime proofend; theorem Th35: :: NAT_4:35 163 is prime proofend; theorem Th36: :: NAT_4:36 317 is prime proofend; theorem Th37: :: NAT_4:37 631 is prime proofend; theorem Th38: :: NAT_4:38 1259 is prime proofend; theorem Th39: :: NAT_4:39 2503 is prime proofend; theorem Th40: :: NAT_4:40 4001 is prime proofend; Lm7: for n being Element of NAT st 1 <= n & n < 4001 holds ex p being Prime st ( n < p & p <= 2 * n ) proofend; begin theorem Th41: :: NAT_4:41 for f, f0, f1 being FinSequence of REAL st f = f0 + f1 holds dom f = (dom f0) /\ (dom f1) proofend; theorem Th42: :: 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 proofend; theorem Th43: :: NAT_4:43 for X1 being set for X2 being finite set st X1 c= X2 & X2 c= NAT & not {} in X2 holds Product (Sgm X1) <= Product (Sgm X2) proofend; theorem Th44: :: NAT_4:44 for a, k being Element of NAT for X being set for F being FinSequence of SetPrimes for 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 ) ) proofend; theorem Th45: :: 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 proofend; theorem Th46: :: 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) proofend; theorem Th47: :: NAT_4:47 for n being Element of NAT for p being Prime st n <> 0 holds 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 implies p |^ k divides n ) & ( p |^ k divides n implies f . k = 1 ) & ( f . k = 0 implies not p |^ k divides n ) & ( not p |^ k divides n implies f . k = 0 ) ) ) & p |-count n = Sum f ) proofend; theorem Th48: :: NAT_4:48 for n being Element of NAT for 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 ) proofend; theorem Th49: :: NAT_4:49 for n being Element of NAT for 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 ) proofend; Lm8: for n, r being Element of NAT for p being Prime for f being FinSequence of REAL st p |^ r <= 2 * n & 2 * n < p |^ (r + 1) & 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))/]) ) holds Sum f <= r proofend; Lm9: for n being Element of NAT for p being Prime st n >= 3 holds ( ( p > 2 * n implies p |-count ((2 * n) choose n) = 0 ) & ( n < p & p <= 2 * n implies p |-count ((2 * n) choose n) <= 1 ) & ( (2 * n) / 3 < p & p <= n implies p |-count ((2 * n) choose n) = 0 ) & ( sqrt (2 * n) < p & p <= (2 * n) / 3 implies p |-count ((2 * n) choose n) <= 1 ) & ( p <= sqrt (2 * n) implies p |^ (p |-count ((2 * n) choose n)) <= 2 * n ) ) proofend; definition let f be FinSequence of NAT ; let p be Prime; funcp |-count f -> FinSequence of NAT means :Def1: :: NAT_4:def 1 ( len it = len f & ( for i being set st i in dom it holds it . i = p |-count (f . i) ) ); existence ex b1 being FinSequence of NAT st ( len b1 = len f & ( for i being set st i in dom b1 holds b1 . i = p |-count (f . i) ) ) proofend; uniqueness for b1, b2 being FinSequence of NAT st len b1 = len f & ( for i being set st i in dom b1 holds b1 . i = p |-count (f . i) ) & len b2 = len f & ( for i being set st i in dom b2 holds b2 . i = p |-count (f . i) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines |-count NAT_4:def_1_:_ for f being FinSequence of NAT for p being Prime for b3 being FinSequence of NAT holds ( b3 = p |-count f iff ( len b3 = len f & ( for i being set st i in dom b3 holds b3 . i = p |-count (f . i) ) ) ); theorem Th50: :: NAT_4:50 for p being Prime for f being FinSequence of NAT st f = {} holds p |-count f = {} proofend; theorem Th51: :: NAT_4:51 for p being Prime for f1, f2 being FinSequence of NAT holds p |-count (f1 ^ f2) = (p |-count f1) ^ (p |-count f2) proofend; theorem Th52: :: NAT_4:52 for p being Prime for n being non empty Element of NAT holds p |-count <*n*> = <*(p |-count n)*> proofend; theorem Th53: :: NAT_4:53 for f being FinSequence of NAT for p being Prime st Product f <> 0 holds p |-count (Product f) = Sum (p |-count f) proofend; theorem Th54: :: 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 proofend; theorem Th55: :: NAT_4:55 for n being Element of NAT for r being Real st r > 0 holds Product (n |-> r) = r to_power n proofend; scheme :: NAT_4:sch 1 scheme1{ P1[ set , set , set ] } : for p being Prime for n being Element of NAT for m being non empty Element of NAT for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P1[n,m,p9] } holds Product (Sgm X) > 0 proofend; scheme :: NAT_4:sch 2 scheme2{ P1[ set , set , set ] } : for p being Prime for n being Element of NAT for m being non empty Element of NAT for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P1[n,m,p9] } & not p |^ (p |-count m) in X holds p |-count (Product (Sgm X)) = 0 proofend; scheme :: NAT_4:sch 3 scheme3{ P1[ set , set , set ] } : for p being Prime for n being Element of NAT for m being non empty Element of NAT for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P1[n,m,p9] } & p |^ (p |-count m) in X holds p |-count (Product (Sgm X)) = p |-count m proofend; Lm10: for n, m being Element of NAT st m = (2 * n) choose n & n >= 3 holds m = ((Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } )) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( sqrt (2 * n) < p & p <= (2 * n) / 3 & p |-count m > 0 ) } ))) * (Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( n < p & p <= 2 * n & p |-count m > 0 ) } )) proofend; scheme :: NAT_4:sch 4 scheme4{ F1( set , set ) -> set , P1[ set , set ] } : for n, m being Element of NAT for r being Real for X being finite set st X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 holds card X <= [\r/] proofend; Lm11: for n, m being Element of NAT st m = (2 * n) choose n & n >= 3 holds Product (Sgm { (p |^ (p |-count m)) where p is prime Element of NAT : ( p <= sqrt (2 * n) & p |-count m > 0 ) } ) <= (2 * n) to_power (sqrt (2 * n)) proofend; begin :: [WP: ] Bertrand's_postulate theorem :: NAT_4:56 for n being Element of NAT st n >= 1 holds ex p being Prime st ( n < p & p <= 2 * n ) proofend;