:: Pocklington's Theorem and {B}ertrand's Postulate
:: by Marco Riccardi
::
:: Received May 17, 2006
:: Copyright (c) 2006-2011 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

proof end;

theorem Th2: :: NAT_4:2

for r, s being real number 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_relative_prime

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 Element of NAT st n < p holds
not p divides n !

proof end;

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

proof end;

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

proof end;

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

proof end;

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

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;

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 Element of NAT st 1 < n & n < 5 & n is prime & not n = 2 holds
n = 3

proof end;

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

proof end;

begin

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

proof end;

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

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;

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)

proof end;

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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)

proof end;

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 )

proof end;

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 )

proof end;

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 )

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 b₁ being FinSequence of NAT st
( len b₁ = len f & ( for i being set st i in dom b₁ holds
b₁ . i = p |-count (f . i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st len b₁ = len f & ( for i being set st i in dom b₁ holds
b₁ . i = p |-count (f . i) ) & len b₂ = len f & ( for i being set st i in dom b₂ holds
b₂ . i = p |-count (f . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines |-count NAT_4:def 1 :
for f being FinSequence of NAT
for p being Prime
for b₃ being FinSequence of NAT holds
( b₃ = p |-count f iff ( len b₃ = len f & ( for i being set st i in dom b₃ holds
b₃ . 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 = {}

proof end;

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)

proof end;

theorem Th52: :: NAT_4:52

for p being Prime
for n being non empty Element of NAT holds p |-count <*n*> = <*(p |-count n)*>

proof end;

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)

proof end;

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

proof end;

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

proof end;

scheme :: NAT_4:sch 1
scheme1{ P₁[ 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 : P₁[n,m,p9] } holds
Product (Sgm X) > 0

proof end;

scheme :: NAT_4:sch 2
scheme2{ P₁[ 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 : P₁[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{ P₁[ 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 : P₁[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{ F₁( set , set ) -> set , P₁[ set , set ] } :

for n, m being Element of NAT
for r being Real
for X being finite set st X = { F₁(p,m) where p is prime Element of NAT : ( p <= r & P₁[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;

begin

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;