:: Pocklington's Theorem and {B}ertrand's Postulate
:: by Marco Riccardi
::
:: Copyright (c) 2006-2021 Association of Mizar Users

theorem Th1: :: NAT_4:1
for r, s being Real st 0 <= r & s * s < r * r holds
s < r
proof end;

theorem Th2: :: NAT_4:2
for r, s being Real st 1 < r & r * r <= s holds
r < s
proof end;

theorem Th3: :: NAT_4:3
for a, n being Nat st a > 1 holds
a |^ n > n
proof end;

theorem Th4: :: NAT_4:4
for n, k, m being Nat st k <= n & m = [\(n / 2)/] holds
n choose m >= n choose k
proof end;

theorem Th5: :: NAT_4:5
for n, m being Nat st m = [\(n / 2)/] & n >= 2 holds
n choose m >= (2 |^ n) / n
proof end;

theorem Th6: :: NAT_4:6
for n being Nat holds (2 * n) choose n >= (4 |^ n) / (2 * n)
proof end;

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 )
proof end;

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 )
proof end;

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
proof end;

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
proof end;

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
proof end;

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 )
proof end;

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 )
proof end;

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 )

proof end;

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 ) ) )
proof end;

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_coprime
proof end;

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 )
proof end;

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
proof end;

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
proof end;

theorem Th19: :: NAT_4:19
for p being Prime
for n being Nat st n < p holds
not p divides n !
proof end;

theorem Th20: :: NAT_4:20
for a, b being non zero 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
proof end;

theorem Th21: :: NAT_4:21
for a, b being non zero Nat st ( for p being Element of NAT st p is prime holds
p |-count a = p |-count b ) holds
a = b
proof end;

theorem Th22: :: NAT_4:22
for p1, p2 being Prime
for m being non zero Element of NAT st p1 |^ (p1 |-count m) = p2 |^ (p2 |-count m) & p1 |-count m > 0 holds
p1 = p2
proof end;

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
proof end;

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
proof end;

:: 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
proof end;

Lm2: for n being Nat st n < 5 & n is prime & not n = 2 holds
n = 3

proof end;

Lm3: for k being Nat st k < 25 holds
for n being Nat st n * n <= k & n is prime & not n = 2 holds
n = 3

proof end;

theorem Th26: :: NAT_4:26
7 is prime
proof end;

theorem :: NAT_4:27
11 is prime
proof end;

theorem Th28: :: NAT_4:28
13 is prime
proof end;

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 )
proof end;

theorem :: NAT_4:29
19 is prime
proof end;

theorem Th30: :: NAT_4:30
23 is prime
proof end;

Lm5: for n being Nat st 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

proof end;

Lm6: for k being Nat st k < 841 holds
for n being Nat st 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

proof end;

theorem Th31: :: NAT_4:31
37 is prime
proof end;

theorem Th32: :: NAT_4:32
43 is prime
proof end;

theorem Th33: :: NAT_4:33
83 is prime
proof end;

theorem Th34: :: NAT_4:34
139 is prime
proof end;

theorem Th35: :: NAT_4:35
163 is prime
proof end;

theorem Th36: :: NAT_4:36
317 is prime
proof end;

theorem Th37: :: NAT_4:37
631 is prime
proof end;

theorem Th38: :: NAT_4:38
1259 is prime
proof end;

theorem Th39: :: NAT_4:39
2503 is prime
proof end;

theorem Th40: :: NAT_4:40
4001 is prime
proof end;

Lm7: for n being Element of NAT st 1 <= n & n < 4001 holds
ex p being Prime st
( n < p & p <= 2 * n )

proof end;

theorem :: NAT_4:41
canceled;

::\$CT
theorem Th41: :: 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
proof end;

theorem Th42: :: 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)
proof end;

theorem Th43: :: 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 ) )
proof end;

theorem Th44: :: 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
proof end;

theorem Th45: :: 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)
proof end;

theorem Th46: :: 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 )
proof end;

theorem Th47: :: 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 )
proof end;

theorem Th48: :: 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 )
proof end;

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

proof end;

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 ) )

proof end;

definition
let f be FinSequence of NAT ;
let p be Prime;
func p |-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) ) )
proof end;
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
proof end;
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 Th49: :: NAT_4:50
for p being Prime
for f being FinSequence of NAT st f = {} holds
p |-count f = {}
proof end;

theorem Th50: :: 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)
proof end;

theorem Th51: :: NAT_4:52
for p being Prime
for n being non zero Element of NAT holds p |-count <*n*> = <*(p |-count n)*>
proof end;

theorem Th52: :: NAT_4:53
for f being FinSequence of NAT
for p being Prime st Product f <> 0 holds
p |-count () = Sum (p |-count f)
proof end;

theorem Th53: :: 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
proof end;

theorem Th54: :: NAT_4:55
for n being Element of NAT
for r being Real st r > 0 holds
Product (n |-> r) = r to_power n
proof end;

scheme :: NAT_4:sch 1
scheme1{ P1[ set , set , set ] } :
for p being Prime
for n being Element of NAT
for m being non zero 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
proof end;

scheme :: NAT_4:sch 2
scheme2{ P1[ set , set , set ] } :
for p being Prime
for n being Element of NAT
for m being non zero 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
proof end;

scheme :: NAT_4:sch 3
scheme3{ P1[ set , set , set ] } :
for p being Prime
for n being Element of NAT
for m being non zero 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
proof end;

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 ) } ))

proof end;

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/]
proof end;

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))

proof end;

:: 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 )
proof end;

theorem :: NAT_4:57
( 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 ) by Lm4;

theorem :: NAT_4:58
( 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 ) by Lm4;

theorem :: NAT_4:59
for n being Nat st n < 5 & n is prime & not n = 2 holds
n = 3 by Lm2;

theorem :: NAT_4:60
for k being Nat st k < 25 holds
for n being Nat st n * n <= k & n is prime & not n = 2 holds
n = 3 by Lm3;

theorem :: NAT_4:61
for n being Nat st 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 by Lm5;

theorem :: NAT_4:62
for k being Nat st k < 841 holds
for n being Nat st 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 by Lm6;