:: The Perfect Number Theorem and Wilson's Theorem
:: by Marco Riccardi
::
:: Copyright (c) 2009-2021 Association of Mizar Users

Lm1: for p being Nat
for n0, m0 being non zero Nat 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 Nat holds 2 |^ (n + 1) < (2 |^ (n + 2)) - 1
proof end;

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

theorem Th3: :: NAT_5:3
for k, n, m being Nat st n = 2 |^ k & m is odd holds
n,m are_coprime
proof end;

theorem Th4: :: NAT_5:4
for n being Nat holds {n} is finite Subset of NAT by ;

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

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

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

theorem Th6: :: NAT_5:6
for n being Nat
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 Nat
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 Nat
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 f1, f2 being FinSequence of REAL st f2 = f1 * (Sgm X) & (dom f1) \ (f1 " ) c= X & X c= dom f1 holds
Sum f1 = Sum f2
proof end;

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

:: like FINSEQ_3:126
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 Nat st n1 in NatDivisors n & m1 in NatDivisors m & n,m are_coprime holds
n1,m1 are_coprime
proof end;

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

theorem Th16: :: NAT_5:16
for n0, m0 being non zero Nat
for n1, m1 being Nat 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 Nat
for n0, m0 being non zero Nat st n0,m0 are_coprime holds
k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)
proof end;

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

theorem Th19: :: NAT_5:19
for n, p being Nat 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 Nat 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 Nat
for n0, m0 being non zero Nat st p is prime holds
p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) by Lm1;

Lm4: for k, m being Nat 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 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 Nat st n + 2 is prime holds
for l being Nat st l in Seg n & l <> 1 holds
ex k being Nat st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )

proof end;

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

proof end;

:: Number Theory (Andrews) p.61-66
:: Wilson's Theorem
theorem :: NAT_5:22
for n being Nat holds
( n is prime iff ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) )
proof end;

:: Proofs from THE BOOK (Aigner-Ziegler) p.19
:: All Primes (1 mod 4) Equal the Sum of Two Squares
theorem :: NAT_5:23
for p being Nat st p is prime & p mod 4 = 1 holds
ex n, m being Nat st p = (n ^2) + (m ^2)
proof end;

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 ;
correctness
coherence
Sum (f | J) is natural
;
proof end;
end;

theorem Th24: :: NAT_5:24
for f being sequence of NAT
for F being sequence of REAL
for J being finite Subset of NAT st f = F & ex k being Nat 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 being set
for f being Function of I,NAT
for J being finite Subset of I
for j being object st J = {j} holds
Sum (f | J) = f . j
proof end;

Lm11: for I being set
for f, g being Function of I,NAT
for J, K being finite Subset of I
for j being object 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 -> sequence of NAT means :Def1: :: NAT_5:def 1
for n being Nat holds it . n = n |^ k;
existence
ex b1 being sequence of NAT st
for n being Nat holds b1 . n = n |^ k
proof end;
uniqueness
for b1, b2 being sequence of NAT st ( for n being Nat holds b1 . n = n |^ k ) & ( for n being Nat 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 sequence of NAT holds
( b2 = EXP k iff for n being Nat 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 non zero Nat st n = m holds
it = Sum ((EXP k) | ()) 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 non zero Nat st n = m holds
b1 = Sum ((EXP k) | ()) ) & ( 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 non zero Nat st n = m holds
b1 = Sum ((EXP k) | ()) ) & ( for m being non zero Nat st n = m holds
b2 = Sum ((EXP k) | ()) ) 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 non zero Nat st n = m holds
b3 = Sum ((EXP k) | ()) ) ) & ( not n <> 0 implies ( b3 = sigma (k,n) iff b3 = 0 ) ) );

definition
let k be natural Number ;
func Sigma k -> sequence of NAT means :Def3: :: NAT_5:def 3
for n being Nat holds it . n = sigma (k,n);
existence
ex b1 being sequence of NAT st
for n being Nat holds b1 . n = sigma (k,n)
proof end;
uniqueness
for b1, b2 being sequence of NAT st ( for n being Nat holds b1 . n = sigma (k,n) ) & ( for n being Nat 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 sequence of NAT holds
( b2 = Sigma k iff for n being Nat 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 Nat holds sigma (k,1) = 1
proof end;

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

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

theorem Th32: :: NAT_5:32
for k, m being Nat
for n0 being non zero Nat 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 Nat
for n0 being non zero Nat st sigma n0 = n0 + m & m divides n0 & n0 <> m holds
( m = 1 & n0 is prime )
proof end;

definition
let f be sequence of NAT;
attr f is multiplicative means :: NAT_5:def 5
for n0, m0 being non zero Nat st n0,m0 are_coprime holds
f . (n0 * m0) = (f . n0) * (f . m0);
end;

:: deftheorem defines multiplicative NAT_5:def 5 :
for f being sequence of NAT holds
( f is multiplicative iff for n0, m0 being non zero Nat st n0,m0 are_coprime holds
f . (n0 * m0) = (f . n0) * (f . m0) );

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

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

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

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

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

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

:: Fundamentals of Number Theory (LeVeque) p.123
:: Euclid
theorem :: NAT_5:38
for p being Nat
for n0 being non zero Nat st (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) holds
n0 is perfect
proof end;

:: Euler
:: The Perfect Number Theorem
theorem :: NAT_5:39
for n0 being non zero Nat st n0 is even & n0 is perfect holds
ex p being Nat st
( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) )
proof end;

definition
func Euler_phi -> sequence of NAT means :Def7: :: NAT_5:def 7
for k being Element of NAT holds it . k = Euler k;
existence
ex b1 being sequence of NAT st
for k being Element of NAT holds b1 . k = Euler k
proof end;
uniqueness
for b1, b2 being sequence of 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 sequence of NAT holds
( b1 = Euler_phi iff for k being Element of NAT holds b1 . k = Euler k );

:: Number Theory (Andrews) p.76
theorem :: NAT_5:40
for n0 being non zero Nat holds Sum () = n0
proof end;