:: The Perfect Number Theorem and Wilson's Theorem
:: by Marco Riccardi
::
:: Received March 3, 2009
:: Copyright (c) 2009 Association of Mizar Users
Lm1:
for p being natural number
for n0, m0 being non zero natural number st p is prime holds
p |-count (n0 gcd m0) = min (p |-count n0),(p |-count m0)
theorem Th1: :: NAT_5:1
theorem Th2: :: NAT_5:2
theorem Th3: :: NAT_5:3
theorem Th4: :: NAT_5:4
theorem Th5: :: NAT_5:5
Lm2:
for n, m, l being natural number holds {n,m,l} is finite Subset of NAT
Lm3:
for n, m, l, k being natural number holds {n,m,l,k} is finite Subset of NAT
theorem Th6: :: NAT_5:6
theorem Th7: :: NAT_5:7
theorem Th8: :: NAT_5:8
theorem Th9: :: NAT_5:9
theorem Th10: :: NAT_5:10
theorem Th11: :: NAT_5:11
theorem Th12: :: NAT_5:12
theorem Th13: :: NAT_5:13
theorem Th14: :: NAT_5:14
theorem Th15: :: NAT_5:15
theorem Th16: :: NAT_5:16
theorem Th17: :: NAT_5:17
theorem Th18: :: NAT_5:18
theorem Th19: :: NAT_5:19
theorem Th20: :: NAT_5:20
theorem :: NAT_5:21
Lm4:
for k, m being natural number holds
( k < m iff k <= m - 1 )
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 )
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
Lm7:
for fs being FinSequence st 1 <= len fs holds
( fs = <*(fs . 1)*> ^ (Del fs,1) & fs = (Del fs,(len fs)) ^ <*(fs . (len fs))*> )
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
Lm9:
for n being natural number st n + 2 is prime holds
for l being natural number st l in Seg n & l <> 1 holds
ex k being natural number st
( k in Seg n & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 )
Lm10:
for n being natural number
for f being FinSequence of NAT st n + 2 is prime & rng f c= Seg n & f is one-to-one & ( for l being natural number st l in rng f & l <> 1 holds
ex k being natural number st
( k in rng f & k <> 1 & k <> l & (l * k) mod (n + 2) = 1 ) ) holds
(Product f) mod (n + 2) = 1
theorem :: NAT_5:22
theorem :: NAT_5:23
theorem Th24: :: NAT_5:24
theorem Th25: :: NAT_5:25
theorem Th26: :: NAT_5:26
theorem Th27: :: NAT_5:27
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))
theorem Th28: :: NAT_5:28
:: deftheorem Def1 defines EXP NAT_5:def 1 :
:: deftheorem Def2 defines sigma NAT_5:def 2 :
:: deftheorem Def3 defines Sigma NAT_5:def 3 :
:: deftheorem defines sigma NAT_5:def 4 :
theorem Th29: :: NAT_5:29
theorem Th30: :: NAT_5:30
theorem Th31: :: NAT_5:31
theorem Th32: :: NAT_5:32
theorem Th33: :: NAT_5:33
:: deftheorem Def5 defines multiplicative NAT_5:def 5 :
theorem Th34: :: NAT_5:34
theorem Th35: :: NAT_5:35
theorem Th36: :: NAT_5:36
theorem Th37: :: NAT_5:37
:: deftheorem Def6 defines perfect NAT_5:def 6 :
theorem :: NAT_5:38
theorem :: NAT_5:39
:: deftheorem Def7 defines Euler_phi NAT_5:def 7 :
theorem :: NAT_5:40