:: Pocklington's Theorem and {B}ertrand's Postulate
:: by Marco Riccardi
::
:: Received May 17, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: NAT_4:1
theorem Th2: :: NAT_4:2
theorem Th3: :: NAT_4:3
for
a,
n being
Nat st
a > 1 holds
a |^ n > n
theorem Th4: :: NAT_4:4
theorem Th5: :: NAT_4:5
theorem Th6: :: NAT_4:6
theorem Th7: :: NAT_4:7
theorem Th8: :: NAT_4:8
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
theorem Th10: :: NAT_4:10
theorem Th11: :: NAT_4:11
theorem Th12: :: NAT_4:12
theorem Th13: :: NAT_4:13
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 )
theorem Th14: :: NAT_4:14
theorem Th15: :: NAT_4:15
theorem Th16: :: NAT_4:16
theorem Th17: :: NAT_4:17
theorem Th18: :: NAT_4:18
theorem Th19: :: NAT_4:19
theorem Th20: :: NAT_4:20
theorem Th21: :: NAT_4:21
theorem Th22: :: NAT_4:22
theorem Th23: :: NAT_4:23
theorem Th24: :: NAT_4:24
theorem Th25: :: NAT_4:25
Lm2:
for n being Element of NAT st 1 < n & n < 5 & n is prime & not n = 2 holds
n = 3
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
theorem Th26: :: NAT_4:26
theorem :: NAT_4:27
theorem Th28: :: NAT_4:28
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 )
theorem :: NAT_4:29
theorem Th30: :: NAT_4:30
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
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
theorem Th31: :: NAT_4:31
theorem Th32: :: NAT_4:32
theorem Th33: :: NAT_4:33
theorem Th34: :: NAT_4:34
theorem Th35: :: NAT_4:35
theorem Th36: :: NAT_4:36
theorem Th37: :: NAT_4:37
theorem Th38: :: NAT_4:38
theorem Th39: :: NAT_4:39
theorem Th40: :: NAT_4:40
Lm7:
for n being Element of NAT st 1 <= n & n < 4001 holds
ex p being Prime st
( n < p & p <= 2 * n )
theorem Th41: :: NAT_4:41
theorem Th42: :: NAT_4:42
theorem Th43: :: NAT_4:43
theorem Th44: :: NAT_4:44
theorem Th45: :: NAT_4:45
theorem Th46: :: NAT_4:46
theorem Th47: :: NAT_4:47
theorem Th48: :: NAT_4:48
theorem Th49: :: NAT_4:49
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
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 ) )
:: deftheorem Def1 defines |-count NAT_4:def 1 :
theorem Th50: :: NAT_4:50
theorem Th51: :: NAT_4:51
theorem Th52: :: NAT_4:52
theorem Th53: :: NAT_4:53
theorem Th54: :: NAT_4:54
theorem Th55: :: NAT_4:55
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 ) } ))
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))
theorem :: NAT_4:56