:: The Perfect Number Theorem and Wilson's Theorem :: by Marco Riccardi :: :: Received March 3, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin 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)) proofend; theorem Th1: :: NAT_5:1 for n being Nat holds 2 |^ (n + 1) < (2 |^ (n + 2)) - 1 proofend; 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 ) proofend; theorem Th3: :: NAT_5:3 for n, k, m being Nat st n = 2 |^ k & m is odd holds n,m are_relative_prime proofend; theorem Th4: :: NAT_5:4 for n being Nat holds {n} is finite Subset of NAT proofend; theorem Th5: :: NAT_5:5 for n, m being Nat holds {n,m} is finite Subset of NAT proofend; Lm2: for n, m, l being Nat holds {n,m,l} is finite Subset of NAT proofend; Lm3: for n, m, l, k being Nat holds {n,m,l,k} is finite Subset of NAT proofend; 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 proofend; 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)) proofend; 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 proofend; 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 proofend; 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) proofend; theorem Th11: :: NAT_5:11 for X being set for f2, f1 being FinSequence of REAL st f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0}) c= X & X c= dom f1 holds Sum f1 = Sum f2 proofend; theorem Th12: :: NAT_5:12 for f2, f1 being FinSequence of REAL st f2 = f1 - {0} holds Sum f1 = Sum f2 proofend; :: like FINSEQ_3:126 theorem Th13: :: NAT_5:13 for f being FinSequence of NAT holds f is FinSequence of REAL proofend; theorem Th14: :: NAT_5:14 for n, m, n1, m1 being Nat st n1 in NatDivisors n & m1 in NatDivisors m & n,m are_relative_prime holds n1,m1 are_relative_prime proofend; theorem Th15: :: NAT_5:15 for n, m, n1, m1, n2, m2 being Nat st n1 in NatDivisors n & m1 in NatDivisors m & n2 in NatDivisors n & m2 in NatDivisors m & n,m are_relative_prime & n1 * m1 = n2 * m2 holds ( n1 = n2 & m1 = m2 ) proofend; 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) proofend; theorem Th17: :: NAT_5:17 for k being Nat for n0, m0 being non zero Nat st n0,m0 are_relative_prime holds k gcd (n0 * m0) = (k gcd n0) * (k gcd m0) proofend; theorem Th18: :: NAT_5:18 for k being Nat for n0, m0 being non zero Nat st n0,m0 are_relative_prime & k in NatDivisors (n0 * m0) holds ex n1, m1 being Nat st ( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 ) proofend; theorem Th19: :: NAT_5:19 for p, n being Nat st p is prime holds NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n } proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 proofend; Lm7: for fs being FinSequence st 1 <= len fs holds ( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> ) proofend; Lm8: for a being Element of NAT for ft being FinSequence of REAL st a in dom ft holds (Product (Del (ft,a))) * (ft . a) = Product ft proofend; 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 ) proofend; 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 proofend; begin :: Number Theory (Andrews) p.61-66 :: [WP: ] Wilson's_Theorem theorem :: NAT_5:22 for n being Nat holds ( n is prime iff ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) ) proofend; begin :: Proofs from THE BOOK (Aigner-Ziegler) p.19 :: [WP: ] 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) proofend; begin definition let I be set ; let f be Function of I,NAT; let J be finite Subset of I; :: original:| redefine funcf | 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 for number ; correctness coherence for b1 being number st b1 = Sum (f | J) holds b1 is natural ; proofend; end; theorem Th24: :: NAT_5:24 for f being Function of NAT,NAT for F being Function of NAT,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))) proofend; 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) proofend; 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)) proofend; theorem Th27: :: NAT_5:27 for I, j being set for f being Function of I,NAT for J being finite Subset of I st J = {j} holds Sum (f | J) = f . j proofend; Lm11: for I, j being set for f, g being Function of I,NAT for J, K being finite Subset of I st J = {j} holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) proofend; 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)) proofend; definition let k be Nat; func EXP k -> Function of NAT,NAT means :Def1: :: NAT_5:def 1 for n being Nat holds it . n = n |^ k; existence ex b1 being Function of NAT,NAT st for n being Nat holds b1 . n = n |^ k proofend; uniqueness for b1, b2 being Function of NAT,NAT st ( for n being Nat holds b1 . n = n |^ k ) & ( for n being Nat holds b2 . n = n |^ k ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines EXP NAT_5:def_1_:_ for k being Nat for b2 being Function of NAT,NAT holds ( b2 = EXP k iff for n being Nat holds b2 . n = n |^ k ); definition let k, n be Nat; 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 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) | (NatDivisors m)) ) & ( 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) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds b2 = Sum ((EXP k) | (NatDivisors m)) ) implies b1 = b2 ) & ( not n <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ); proofend; end; :: deftheorem Def2 defines sigma NAT_5:def_2_:_ for k, n being Nat 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) | (NatDivisors m)) ) ) & ( not n <> 0 implies ( b3 = sigma (k,n) iff b3 = 0 ) ) ); definition let k be Nat; func Sigma k -> Function of NAT,NAT means :Def3: :: NAT_5:def 3 for n being Nat holds it . n = sigma (k,n); existence ex b1 being Function of NAT,NAT st for n being Nat holds b1 . n = sigma (k,n) proofend; uniqueness for b1, b2 being Function of NAT,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 proofend; end; :: deftheorem Def3 defines Sigma NAT_5:def_3_:_ for k being Nat for b2 being Function of NAT,NAT holds ( b2 = Sigma k iff for n being Nat holds b2 . n = sigma (k,n) ); definition let n be Nat; 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 Nat holds sigma n = sigma (1,n); theorem Th29: :: NAT_5:29 for k being Nat holds sigma (k,1) = 1 proofend; theorem Th30: :: NAT_5:30 for p, n being Nat st p is prime holds sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1) proofend; 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 proofend; theorem Th32: :: NAT_5:32 for m, k 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 proofend; 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 ) proofend; definition let f be Function of NAT,NAT; attrf is multiplicative means :Def5: :: NAT_5:def 5 for n0, m0 being non zero Nat st n0,m0 are_relative_prime holds f . (n0 * m0) = (f . n0) * (f . m0); end; :: deftheorem Def5 defines multiplicative NAT_5:def_5_:_ for f being Function of NAT,NAT holds ( f is multiplicative iff for n0, m0 being non zero Nat st n0,m0 are_relative_prime holds f . (n0 * m0) = (f . n0) * (f . m0) ); theorem Th34: :: NAT_5:34 for f, F being Function of NAT,NAT st f is multiplicative & ( for n0 being non zero Nat holds F . n0 = Sum (f | (NatDivisors n0)) ) holds F is multiplicative proofend; theorem Th35: :: NAT_5:35 for k being Nat holds EXP k is multiplicative proofend; theorem Th36: :: NAT_5:36 for k being Nat holds Sigma k is multiplicative proofend; theorem Th37: :: NAT_5:37 for n0, m0 being non zero Nat st n0,m0 are_relative_prime holds sigma (n0 * m0) = (sigma n0) * (sigma m0) proofend; begin definition let n0 be non zero Nat; attrn0 is perfect means :Def6: :: NAT_5:def 6 sigma n0 = 2 * n0; end; :: deftheorem Def6 defines perfect NAT_5:def_6_:_ for n0 being non zero Nat 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 proofend; :: Euler :: [WP: ] 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) ) proofend; begin definition func Euler_phi -> Function of NAT,NAT means :Def7: :: NAT_5:def 7 for k being Element of NAT holds it . k = Euler k; existence ex b1 being Function of NAT,NAT st for k being Element of NAT holds b1 . k = Euler k proofend; uniqueness for b1, b2 being Function of NAT,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 proofend; end; :: deftheorem Def7 defines Euler_phi NAT_5:def_7_:_ for b1 being Function of NAT,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 (Euler_phi | (NatDivisors n0)) = n0 proofend;