:: The Perfect Number Theorem and Wilson's Theorem :: by Marco Riccardi :: :: Received March 3, 2009 :: Copyright (c) 2009-2018 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;