begin
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:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
Lm2:
for n, m, l being natural number holds {n,m,l} is finite Subset of
Lm3:
for n, m, l, k being natural number holds {n,m,l,k} is finite Subset of
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
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
begin
theorem
begin
theorem
begin
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
Lm11:
for I, j being set
for f, g being Function of I, NAT
for J, K being finite Subset of st J = {j} holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
theorem Th28:
:: 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:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
:: deftheorem Def5 defines multiplicative NAT_5:def 5 :
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
begin
:: deftheorem Def6 defines perfect NAT_5:def 6 :
theorem
theorem
begin
:: deftheorem Def7 defines Euler_phi NAT_5:def 7 :
theorem