:: by Marco Riccardi

::

:: Received May 17, 2006

:: Copyright (c) 2006-2016 Association of Mizar Users

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 )

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

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

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

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

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

q |^ (n + 1) divides d

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

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

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

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

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

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

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;

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;

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;

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;

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

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)

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

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)

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 )

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 )

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 )

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;

ex b_{1} being FinSequence of NAT st

( len b_{1} = len f & ( for i being set st i in dom b_{1} holds

b_{1} . i = p |-count (f . i) ) )

for b_{1}, b_{2} being FinSequence of NAT st len b_{1} = len f & ( for i being set st i in dom b_{1} holds

b_{1} . i = p |-count (f . i) ) & len b_{2} = len f & ( for i being set st i in dom b_{2} holds

b_{2} . i = p |-count (f . i) ) holds

b_{1} = b_{2}

end;
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 ( len it = len f & ( for i being set st i in dom it holds

it . i = p |-count (f . i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines |-count NAT_4:def 1 :

for f being FinSequence of NAT

for p being Prime

for b_{3} being FinSequence of NAT holds

( b_{3} = p |-count f iff ( len b_{3} = len f & ( for i being set st i in dom b_{3} holds

b_{3} . i = p |-count (f . i) ) ) );

for f being FinSequence of NAT

for p being Prime

for b

( b

b

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)

for f1, f2 being FinSequence of NAT holds p |-count (f1 ^ f2) = (p |-count f1) ^ (p |-count f2)

proof end;

theorem Th52: :: 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)

for p being Prime st Product f <> 0 holds

p |-count (Product f) = 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

( f1 . k <= f2 . k & f1 . k > 0 ) ) holds

Product f1 <= Product f2

proof end;

scheme :: NAT_4:sch 2

scheme2{ P_{1}[ set , set , set ] } :

scheme2{ P

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 : P_{1}[n,m,p9] } & not p |^ (p |-count m) in X holds

p |-count (Product (Sgm X)) = 0

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

p |-count (Product (Sgm X)) = 0

proof end;

scheme :: NAT_4:sch 3

scheme3{ P_{1}[ set , set , set ] } :

scheme3{ P

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 : P_{1}[n,m,p9] } & p |^ (p |-count m) in X holds

p |-count (Product (Sgm X)) = p |-count m

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

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;

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;