:: The Perfect Number Theorem and Wilson's Theorem
:: by Marco Riccardi
::
:: Received March 3, 2009
:: 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 ORDINAL1:def 12, ZFMISC_1:31;

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 " {0}) 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 - {0} 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
(Product f) 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 b₁ being sequence of NAT st
for n being Nat holds b₁ . n = n |^ k

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Nat holds b₁ . n = n |^ k ) & ( for n being Nat holds b₂ . n = n |^ k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines EXP NAT_5:def 1 :
for k being natural Number
for b₂ being sequence of NAT holds
( b₂ = EXP k iff for n being Nat holds b₂ . 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) | (NatDivisors m)) if n <> 0
otherwise it = 0 ;

correctness
consistency
for b₁ being Element of NAT holds verum;
existence
( ( for b₁ being Element of NAT holds verum ) & ( n <> 0 implies ex b₁ being Element of NAT st
for m being non zero Nat st n = m holds
b₁ = Sum ((EXP k) | (NatDivisors m)) ) & ( not n <> 0 implies ex b₁ being Element of NAT st b₁ = 0 ) );
uniqueness
for b₁, b₂ being Element of NAT holds
( ( n <> 0 & ( for m being non zero Nat st n = m holds
b₁ = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds
b₂ = Sum ((EXP k) | (NatDivisors m)) ) implies b₁ = b₂ ) & ( not n <> 0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def2 defines sigma NAT_5:def 2 :
for k, n being natural Number
for b₃ being Element of NAT holds
( ( n <> 0 implies ( b₃ = sigma (k,n) iff for m being non zero Nat st n = m holds
b₃ = Sum ((EXP k) | (NatDivisors m)) ) ) & ( not n <> 0 implies ( b₃ = sigma (k,n) iff b₃ = 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 b₁ being sequence of NAT st
for n being Nat holds b₁ . n = sigma (k,n)

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for n being Nat holds b₁ . n = sigma (k,n) ) & ( for n being Nat holds b₂ . n = sigma (k,n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Sigma NAT_5:def 3 :
for k being natural Number
for b₂ being sequence of NAT holds
( b₂ = Sigma k iff for n being Nat holds b₂ . 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 | (NatDivisors n0)) ) 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 b₁ being sequence of NAT st
for k being Element of NAT holds b₁ . k = Euler k

proof end;

uniqueness
for b₁, b₂ being sequence of NAT st ( for k being Element of NAT holds b₁ . k = Euler k ) & ( for k being Element of NAT holds b₂ . k = Euler k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Euler_phi NAT_5:def 7 :
for b₁ being sequence of NAT holds
( b₁ = Euler_phi iff for k being Element of NAT holds b₁ . k = Euler k );

:: Number Theory (Andrews) p.76

theorem :: NAT_5:40

for n0 being non zero Nat holds Sum (Euler_phi | (NatDivisors n0)) = n0

proof end;