:: 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;