:: The Perfect Number Theorem and Wilson's Theorem
:: by Marco Riccardi
::
:: Received March 3, 2009
:: Copyright (c) 2009-2011 Association of Mizar Users


begin

Lm1: for p being natural number
for n0, m0 being natural non zero number st p is prime holds
p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0))
proof end;

theorem Th1: :: NAT_5:1
for n being natural number holds 2 |^ (n + 1) < (2 |^ (n + 2)) - 1
proof end;

theorem Th2: :: NAT_5:2
for n0 being natural non zero number st n0 is even holds
ex k, m being natural number st
( not m is even & k > 0 & n0 = (2 |^ k) * m )
proof end;

theorem Th3: :: NAT_5:3
for n, k, m being natural number st n = 2 |^ k & not m is even holds
n,m are_relative_prime
proof end;

theorem Th4: :: NAT_5:4
for n being natural number holds {n} is finite Subset of NAT
proof end;

theorem Th5: :: NAT_5:5
for n, m being natural number holds {n,m} is finite Subset of NAT
proof end;

Lm2: for n, m, l being natural number holds {n,m,l} is finite Subset of NAT
proof end;

Lm3: for n, m, l, k being natural number holds {n,m,l,k} is finite Subset of NAT
proof end;

theorem Th6: :: NAT_5:6
for n being natural number
for f being FinSequence st f is one-to-one holds
Del (f,n) is one-to-one
proof end;

theorem Th7: :: NAT_5:7
for n being natural number
for f being FinSequence st f is one-to-one & n in dom f holds
not f . n in rng (Del (f,n))
proof end;

theorem Th8: :: NAT_5:8
for n being natural number
for f being FinSequence
for x being set st x in rng f & not x in rng (Del (f,n)) holds
x = f . n
proof end;

theorem Th9: :: NAT_5:9
for X being set
for f1 being FinSequence of NAT
for f2 being FinSequence of X st rng f1 c= dom f2 holds
f2 * f1 is FinSequence of X
proof end;

theorem Th10: :: NAT_5:10
for X, Y being set
for f1, f2, f3 being FinSequence of REAL st X \/ Y = dom f1 & X misses Y & f2 = f1 * (Sgm X) & f3 = f1 * (Sgm Y) holds
Sum f1 = (Sum f2) + (Sum f3)
proof end;

theorem Th11: :: NAT_5:11
for X being set
for f2, f1 being FinSequence of REAL st f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0}) c= X & X c= dom f1 holds
Sum f1 = Sum f2
proof end;

theorem Th12: :: NAT_5:12
for f2, f1 being FinSequence of REAL st f2 = f1 - {0} holds
Sum f1 = Sum f2
proof end;

theorem Th13: :: NAT_5:13
for f being FinSequence of NAT holds f is FinSequence of REAL
proof end;

theorem Th14: :: NAT_5:14
for n, m, n1, m1 being natural number st n1 in NatDivisors n & m1 in NatDivisors m & n,m are_relative_prime holds
n1,m1 are_relative_prime
proof end;

theorem Th15: :: NAT_5:15
for n, m, n1, m1, n2, m2 being natural number st n1 in NatDivisors n & m1 in NatDivisors m & n2 in NatDivisors n & m2 in NatDivisors m & n,m are_relative_prime & n1 * m1 = n2 * m2 holds
( n1 = n2 & m1 = m2 )
proof end;

theorem Th16: :: NAT_5:16
for n0, m0 being natural non zero number
for n1, m1 being natural number st n1 in NatDivisors n0 & m1 in NatDivisors m0 holds
n1 * m1 in NatDivisors (n0 * m0)
proof end;

theorem Th17: :: NAT_5:17
for k being natural number
for n0, m0 being natural non zero number st n0,m0 are_relative_prime holds
k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)
proof end;

theorem Th18: :: NAT_5:18
for k being natural number
for n0, m0 being natural non zero number st n0,m0 are_relative_prime & k in NatDivisors (n0 * m0) holds
ex n1, m1 being natural number st
( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )
proof end;

theorem Th19: :: NAT_5:19
for p, n being natural number st p is prime holds
NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n }
proof end;

theorem Th20: :: NAT_5:20
for l, p, n1, n2 being natural number st 0 <> l & p > l & p > n1 & p > n2 & (l * n1) mod p = (l * n2) mod p & p is prime holds
n1 = n2
proof end;

theorem :: NAT_5:21
for p being natural number
for n0, m0 being natural non zero number st p is prime holds
p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) by Lm1;

Lm4: for k, m being natural number holds
( k < m iff k <= m - 1 )
proof end;

Lm5: for a being Element of NAT
for fs being FinSequence st a in dom fs holds
ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )
proof end;

Lm6: for a being Element of NAT
for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2
proof end;

Lm7: for fs being FinSequence st 1 <= len fs holds
( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> )
proof end;

Lm8: for a being Element of NAT
for ft being FinSequence of REAL st a in dom ft holds
(Product (Del (ft,a))) * (ft . a) = Product ft
proof end;

Lm9: for n being natural number st n + 2 is prime holds
for l being natural number st l in Seg n & l <> 1 holds
ex k being natural number st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
proof end;

Lm10: for n being natural number
for f being FinSequence of NAT st n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being natural number st l in rng f & l <> 1 holds
ex k being natural number st
( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds
(Product f) mod (n + 2) = 1
proof end;

begin

theorem :: NAT_5:22
for n being natural number holds
( n is prime iff ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) )
proof end;

begin

theorem :: NAT_5:23
for p being natural number st p is prime & p mod 4 = 1 holds
ex n, m being natural number st p = (n ^2) + (m ^2)
proof end;

begin

definition
let I be set ;
let f be Function of I,NAT;
let J be finite Subset of I;
:: original: |
redefine func f | J -> bag of J;
correctness
coherence
f | J is bag of J
;
;
end;

registration
let I be set ;
let f be Function of I,NAT;
let J be finite Subset of I;
cluster Sum (f | J) -> natural number ;
correctness
coherence
for b1 being number st b1 = Sum (f | J) holds
b1 is natural
;
proof end;
end;

theorem Th24: :: NAT_5:24
for f being Function of NAT,NAT
for F being Function of NAT,REAL
for J being finite Subset of NAT st f = F & ex k being natural number st J c= Seg k holds
Sum (f | J) = Sum (Func_Seq (F,(Sgm J)))
proof end;

theorem Th25: :: NAT_5:25
for I being non empty set
for F being PartFunc of I,REAL
for f being Function of I,NAT
for J being finite Subset of I st f = F holds
Sum (f | J) = Sum (F,J)
proof end;

theorem Th26: :: NAT_5:26
for I being set
for f being Function of I,NAT
for J, K being finite Subset of I st J misses K holds
Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))
proof end;

theorem Th27: :: NAT_5:27
for I, j being set
for f being Function of I,NAT
for J being finite Subset of I st J = {j} holds
Sum (f | J) = f . j
proof end;

Lm11: for I, j being set
for f, g being Function of I,NAT
for J, K being finite Subset of I st J = {j} holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
proof end;

theorem Th28: :: NAT_5:28
for I being set
for f, g being Function of I,NAT
for J, K being finite Subset of I holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))
proof end;

definition
let k be natural number ;
func EXP k -> Function of NAT,NAT means :Def1: :: NAT_5:def 1
for n being natural number holds it . n = n |^ k;
existence
ex b1 being Function of NAT,NAT st
for n being natural number holds b1 . n = n |^ k
proof end;
uniqueness
for b1, b2 being Function of NAT,NAT st ( for n being natural number holds b1 . n = n |^ k ) & ( for n being natural number holds b2 . n = n |^ k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines EXP NAT_5:def 1 :
for k being natural number
for b2 being Function of NAT,NAT holds
( b2 = EXP k iff for n being natural number holds b2 . n = n |^ k );

definition
let k, n be natural number ;
func sigma (k,n) -> Element of NAT means :Def2: :: NAT_5:def 2
for m being natural non zero number st n = m holds
it = Sum ((EXP k) | (NatDivisors m)) if n <> 0
otherwise it = 0 ;
correctness
consistency
for b1 being Element of NAT holds verum
;
existence
( ( for b1 being Element of NAT holds verum ) & ( n <> 0 implies ex b1 being Element of NAT st
for m being natural non zero number st n = m holds
b1 = Sum ((EXP k) | (NatDivisors m)) ) & ( not n <> 0 implies ex b1 being Element of NAT st b1 = 0 ) )
;
uniqueness
for b1, b2 being Element of NAT holds
( ( n <> 0 & ( for m being natural non zero number st n = m holds
b1 = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being natural non zero number st n = m holds
b2 = Sum ((EXP k) | (NatDivisors m)) ) implies b1 = b2 ) & ( not n <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
;
proof end;
end;

:: deftheorem Def2 defines sigma NAT_5:def 2 :
for k, n being natural number
for b3 being Element of NAT holds
( ( n <> 0 implies ( b3 = sigma (k,n) iff for m being natural non zero number st n = m holds
b3 = Sum ((EXP k) | (NatDivisors m)) ) ) & ( not n <> 0 implies ( b3 = sigma (k,n) iff b3 = 0 ) ) );

definition
let k be natural number ;
func Sigma k -> Function of NAT,NAT means :Def3: :: NAT_5:def 3
for n being natural number holds it . n = sigma (k,n);
existence
ex b1 being Function of NAT,NAT st
for n being natural number holds b1 . n = sigma (k,n)
proof end;
uniqueness
for b1, b2 being Function of NAT,NAT st ( for n being natural number holds b1 . n = sigma (k,n) ) & ( for n being natural number holds b2 . n = sigma (k,n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Sigma NAT_5:def 3 :
for k being natural number
for b2 being Function of NAT,NAT holds
( b2 = Sigma k iff for n being natural number holds b2 . n = sigma (k,n) );

definition
let n be natural number ;
func sigma n -> Element of NAT equals :: NAT_5:def 4
sigma (1,n);
correctness
coherence
sigma (1,n) is Element of NAT
;
;
end;

:: deftheorem defines sigma NAT_5:def 4 :
for n being natural number holds sigma n = sigma (1,n);

theorem Th29: :: NAT_5:29
for k being natural number holds sigma (k,1) = 1
proof end;

theorem Th30: :: NAT_5:30
for p, n being natural number st p is prime holds
sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1)
proof end;

theorem Th31: :: NAT_5:31
for m being natural number
for n0 being natural non zero number st m divides n0 & n0 <> m & m <> 1 holds
(1 + m) + n0 <= sigma n0
proof end;

theorem Th32: :: NAT_5:32
for m, k being natural number
for n0 being natural non zero number st m divides n0 & k divides n0 & n0 <> m & n0 <> k & m <> 1 & k <> 1 & m <> k holds
((1 + m) + k) + n0 <= sigma n0
proof end;

theorem Th33: :: NAT_5:33
for m being natural number
for n0 being natural non zero number st sigma n0 = n0 + m & m divides n0 & n0 <> m holds
( m = 1 & n0 is prime )
proof end;

definition
let f be Function of NAT,NAT;
attr f is multiplicative means :Def5: :: NAT_5:def 5
for n0, m0 being natural non zero number st n0,m0 are_relative_prime holds
f . (n0 * m0) = (f . n0) * (f . m0);
end;

:: deftheorem Def5 defines multiplicative NAT_5:def 5 :
for f being Function of NAT,NAT holds
( f is multiplicative iff for n0, m0 being natural non zero number st n0,m0 are_relative_prime holds
f . (n0 * m0) = (f . n0) * (f . m0) );

theorem Th34: :: NAT_5:34
for f, F being Function of NAT,NAT st f is multiplicative & ( for n0 being natural non zero number holds F . n0 = Sum (f | (NatDivisors n0)) ) holds
F is multiplicative
proof end;

theorem Th35: :: NAT_5:35
for k being natural number holds EXP k is multiplicative
proof end;

theorem Th36: :: NAT_5:36
for k being natural number holds Sigma k is multiplicative
proof end;

theorem Th37: :: NAT_5:37
for n0, m0 being natural non zero number st n0,m0 are_relative_prime holds
sigma (n0 * m0) = (sigma n0) * (sigma m0)
proof end;

begin

definition
let n0 be natural non zero number ;
attr n0 is perfect means :Def6: :: NAT_5:def 6
sigma n0 = 2 * n0;
end;

:: deftheorem Def6 defines perfect NAT_5:def 6 :
for n0 being natural non zero number holds
( n0 is perfect iff sigma n0 = 2 * n0 );

theorem :: NAT_5:38
for p being natural number
for n0 being natural non zero number st (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) holds
n0 is perfect
proof end;

theorem :: NAT_5:39
for n0 being natural non zero number st n0 is even & n0 is perfect holds
ex p being natural number st
( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) )
proof end;

begin

definition
func Euler_phi -> Function of NAT,NAT means :Def7: :: NAT_5:def 7
for k being Element of NAT holds it . k = Euler k;
existence
ex b1 being Function of NAT,NAT st
for k being Element of NAT holds b1 . k = Euler k
proof end;
uniqueness
for b1, b2 being Function of NAT,NAT st ( for k being Element of NAT holds b1 . k = Euler k ) & ( for k being Element of NAT holds b2 . k = Euler k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Euler_phi NAT_5:def 7 :
for b1 being Function of NAT,NAT holds
( b1 = Euler_phi iff for k being Element of NAT holds b1 . k = Euler k );

theorem :: NAT_5:40
for n0 being natural non zero number holds Sum (Euler_phi | (NatDivisors n0)) = n0
proof end;