:: The Perfect Number Theorem and Wilson's Theorem
:: by Marco Riccardi
::
:: Received March 3, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDINAL1, XCMPLX_0, INT_2, NAT_3, XXREAL_0, XBOOLE_0,
NEWTON, ARYTM_3, ARYTM_1, NAT_1, RELAT_1, CARD_1, ABIAN, SUBSET_1,
FINSET_1, FINSEQ_1, FUNCT_1, FINSEQ_3, TARSKI, CARD_3, ORDINAL4, FUNCT_2,
FINSEQ_2, FUNCOP_1, MOEBIUS1, COMPLEX1, INT_1, REALSET1, SQUARE_1, INT_5,
ZFMISC_1, POWER, REAL_1, PRE_POLY, UPROOTS, BHSP_5, CLASSES1, PARTFUN1,
RFUNCT_3, BINOP_2, PROB_1, WAYBEL29, MSSUBFAM, TOPGEN_1, EULER_1, NAT_5;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCOP_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, MCART_1, FUNCT_2, ORDINAL1, CARD_1, NUMBERS,
FINSEQ_1, FINSEQ_3, EXTREAL1, XCMPLX_0, XREAL_0, NAT_1, INT_1, INT_2,
NAT_D, RVSUM_1, REAL_1, SQUARE_1, XXREAL_0, NEWTON, FINSEQ_2, ABIAN,
PEPIN, INT_5, FINSEQOP, ENUMSET1, FINSET_1, COMPLEX1, NAT_3, DOMAIN_1,
POWER, MOEBIUS1, BHSP_5, EULER_1, WSIERP_1, BINOP_1, RECDEF_1, UPROOTS,
BINOP_2, FUNCT_3, RFUNCT_3, CLASSES1, PRE_POLY;
constructors WELLORD2, REAL_1, NAT_D, BINOP_2, WSIERP_1, ABIAN, EULER_1,
PEPIN, INT_5, RECDEF_1, MOEBIUS1, FINSEQOP, EXTREAL1, UPROOTS, NAT_3,
REALSET1, POWER, BHSP_5, CALCUL_2, SUPINF_1, RFUNCT_3, CLASSES1, BINOP_1,
NUMBERS;
registrations XBOOLE_0, RELSET_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, RVSUM_1, VALUED_0, NEWTON,
ABIAN, FUNCT_1, ZFMISC_1, SUBSET_1, MOEBIUS1, FUNCT_2, PRE_CIRC, RELAT_1,
SQUARE_1, CARD_1, PREPOWER, NAT_3, PRE_POLY, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve k,n,m,l,p for Nat;
reserve n0,m0 for non zero Nat;
theorem :: NAT_5:1
2|^(n+1) < 2|^(n+2) - 1;
theorem :: NAT_5:2
n0 is even implies ex k,m st m is odd & k > 0 & n0 = 2|^k * m;
theorem :: NAT_5:3
n=2|^k & m is odd implies n,m are_coprime;
theorem :: NAT_5:4
{n} is finite Subset of NAT;
theorem :: NAT_5:5
{n,m} is finite Subset of NAT;
:: FinSequence
reserve f for FinSequence;
reserve x,X,Y for set;
theorem :: NAT_5:6
f is one-to-one implies Del(f,n) is one-to-one;
theorem :: NAT_5:7
f is one-to-one & n in dom f implies not f.n in rng Del(f,n);
theorem :: NAT_5:8
x in rng f & not x in rng Del(f,n) implies x = f.n;
theorem :: NAT_5:9
for f1 being FinSequence of NAT, f2 being FinSequence of X st rng
f1 c= dom f2 holds f2*f1 is FinSequence of X;
reserve f1,f2,f3 for FinSequence of REAL;
theorem :: NAT_5:10
X \/ Y = dom f1 & X misses Y & f2 = f1*Sgm(X) & f3 = f1*Sgm(Y)
implies Sum f1 = Sum f2 + Sum f3;
theorem :: NAT_5:11
f2 = f1*Sgm(X) & dom f1 \ f1"{0} c= X & X c= dom f1 implies Sum f1 = Sum f2;
theorem :: NAT_5:12
f2 = f1 - {0} implies Sum f1 = Sum f2;
:: like FINSEQ_3:126
theorem :: NAT_5:13
for f being FinSequence of NAT holds f is FinSequence of REAL;
:: NatDivisors
reserve n1,n2,m1,m2 for Nat;
theorem :: NAT_5:14
n1 in NatDivisors n & m1 in NatDivisors m & n,m
are_coprime implies n1,m1 are_coprime;
theorem :: NAT_5:15
n1 in NatDivisors n & m1 in NatDivisors m & n2 in NatDivisors n
& m2 in NatDivisors m & n,m are_coprime & n1*m1=n2*m2 implies n1=n2 & m1
=m2;
theorem :: NAT_5:16
n1 in NatDivisors n0 & m1 in NatDivisors m0 implies n1*m1 in
NatDivisors(n0*m0);
theorem :: NAT_5:17
n0,m0 are_coprime implies k gcd n0*m0 = (k gcd n0)*(k gcd m0);
theorem :: NAT_5:18
n0,m0 are_coprime & k in NatDivisors(n0*m0) implies ex n1
,m1 st n1 in NatDivisors n0 & m1 in NatDivisors m0 & k=n1*m1;
theorem :: NAT_5:19
p is prime implies NatDivisors(p|^n) = {p|^k where k is Element
of NAT : k <= n};
theorem :: NAT_5:20
0 <> l & p > l & p > n1 & p > n2 & l*n1 mod p = l*n2 mod p & p
is prime implies n1=n2;
theorem :: NAT_5:21
p is prime implies p |-count(n0 gcd m0) = min(p |-count n0,p |-count
m0);
begin :: Wilson's Theorem
:: Number Theory (Andrews) p.61-66
::$N Wilson's Theorem
theorem :: NAT_5:22
n is prime iff (n-'1)! + 1 mod n = 0 & n>1;
begin :: All Primes (1 mod 4) Equal the Sum of Two Squares
:: Proofs from THE BOOK (Aigner-Ziegler) p.19
::$N All Primes (1 mod 4) Equal the Sum of Two Squares
theorem :: NAT_5:23
p is prime & p mod 4 = 1 implies ex n,m st p = n^2 + m^2;
begin :: The Sum of Divisors Function
definition
let I be set;
let f be Function of I, NAT;
let J be finite Subset of I;
redefine func f|J -> 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;
end;
theorem :: NAT_5:24
for f being sequence of NAT, F being sequence of REAL,
J being finite Subset of NAT st f = F & (ex k st J c= Seg k) holds Sum(f|J) =
Sum Func_Seq(F,Sgm J);
theorem :: NAT_5:25
for I being non empty set, F being PartFunc of I, REAL, f being
Function of I, NAT, J being finite Subset of I st f = F holds Sum(f|J) = Sum(F,
J);
reserve I,j for set;
reserve f,g for Function of I, NAT;
reserve J,K for finite Subset of I;
theorem :: NAT_5:26
J misses K implies Sum(f|(J \/ K)) = Sum(f|J) + Sum(f|K);
theorem :: NAT_5:27
for j being object holds J = {j} implies Sum(f|J) = f.j;
theorem :: NAT_5:28
Sum((multnat*[:f,g:])|[:J,K:]) = Sum(f|J) * Sum(g|K);
definition
let k be natural Number;
func EXP(k) -> sequence of NAT means
:: NAT_5:def 1
for n being Nat holds it.n = n|^k;
end;
definition
let k,n be natural Number;
func sigma(k,n) -> Element of NAT means
:: 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;
end;
definition
let k be natural Number;
func Sigma(k) -> sequence of NAT means
:: NAT_5:def 3
for n being Nat holds it.n = sigma(k,n);
end;
definition
let n be natural Number;
func sigma n -> Element of NAT equals
:: NAT_5:def 4
sigma(1,n);
end;
theorem :: NAT_5:29
sigma(k,1) = 1;
theorem :: NAT_5:30
p is prime implies sigma(p|^n) = (p|^(n+1) - 1)/(p - 1);
theorem :: NAT_5:31
m divides n0 & n0<>m & m<>1 implies 1+m+n0 <= sigma n0;
theorem :: NAT_5:32
m divides n0 & k divides n0 & n0<>m & n0<>k & m<>1 & k<>1 & m<>k
implies 1+m+k+n0 <= sigma n0;
theorem :: NAT_5:33
sigma n0 = n0 + m & m divides n0 & n0<>m implies m = 1 & n0 is prime;
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;
theorem :: NAT_5:34
for f,F being sequence of NAT st f is multiplicative & (for
n0 holds F.n0 = Sum(f|NatDivisors n0)) holds F is multiplicative;
theorem :: NAT_5:35
EXP(k) is multiplicative;
theorem :: NAT_5:36
Sigma(k) is multiplicative;
theorem :: NAT_5:37
n0,m0 are_coprime implies sigma(n0*m0) = sigma(n0) * sigma m0;
begin :: The Perfect Number Theorem
definition
let n0 be non zero natural Number;
attr n0 is perfect means
:: NAT_5:def 6
sigma n0 = 2 * n0;
end;
:: Fundamentals of Number Theory (LeVeque) p.123
:: Euclid
theorem :: NAT_5:38
2|^p -' 1 is prime & n0 = 2|^(p -' 1)*(2|^p -' 1) implies n0 is perfect;
:: Euler
::$N The Perfect Number Theorem
theorem :: NAT_5:39
n0 is even & n0 is perfect implies ex p being Nat st 2|^p
-' 1 is prime & n0 = 2|^(p -' 1)*(2|^p -' 1);
begin :: A Formula involving Euler's Function
definition
func Euler_phi -> sequence of NAT means
:: NAT_5:def 7
for k being Element of NAT holds it.k = Euler(k);
end;
:: Number Theory (Andrews) p.76
theorem :: NAT_5:40
Sum(Euler_phi|NatDivisors n0) = n0;