:: by Marco Riccardi

::

:: Received March 3, 2009

:: Copyright (c) 2009-2017 Association of Mizar Users

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))

proof end;

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 )

ex k, m being Nat st

( m is odd & k > 0 & n0 = (2 |^ k) * m )

proof end;

Lm2: for n, m, l being Nat holds {n,m,l} is finite Subset of NAT

proof end;

Lm3: for k, n, m, l being Nat holds {n,m,l,k} is finite Subset of NAT

proof end;

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))

for f being FinSequence st f is one-to-one & n in dom f holds

not f . n in rng (Del (f,n))

proof end;

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

for f being FinSequence

for x being set st x in rng f & not x in rng (Del (f,n)) holds

x = f . n

proof end;

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

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

proof end;

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)

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)

proof end;

theorem Th11: :: NAT_5:11

for X being set

for f1, f2 being FinSequence of REAL st f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0}) c= X & X c= dom f1 holds

Sum f1 = Sum f2

for f1, f2 being FinSequence of REAL st f2 = f1 * (Sgm X) & (dom f1) \ (f1 " {0}) c= X & X c= dom f1 holds

Sum f1 = Sum f2

proof end;

:: like FINSEQ_3:126

theorem Th14: :: NAT_5:14

for n, m, n1, m1 being Nat st n1 in NatDivisors n & m1 in NatDivisors m & n,m are_coprime holds

n1,m1 are_coprime

n1,m1 are_coprime

proof end;

theorem Th15: :: NAT_5:15

for n, m, n1, n2, m1, m2 being Nat st n1 in NatDivisors n & m1 in NatDivisors m & n2 in NatDivisors n & m2 in NatDivisors m & n,m are_coprime & n1 * m1 = n2 * m2 holds

( n1 = n2 & m1 = m2 )

( n1 = n2 & m1 = m2 )

proof end;

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)

for n1, m1 being Nat st n1 in NatDivisors n0 & m1 in NatDivisors m0 holds

n1 * m1 in NatDivisors (n0 * m0)

proof end;

theorem Th17: :: NAT_5:17

for k being Nat

for n0, m0 being non zero Nat st n0,m0 are_coprime holds

k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)

for n0, m0 being non zero Nat st n0,m0 are_coprime holds

k gcd (n0 * m0) = (k gcd n0) * (k gcd m0)

proof end;

theorem Th18: :: NAT_5:18

for k being Nat

for n0, m0 being non zero Nat st n0,m0 are_coprime & k in NatDivisors (n0 * m0) holds

ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )

for n0, m0 being non zero Nat st n0,m0 are_coprime & k in NatDivisors (n0 * m0) holds

ex n1, m1 being Nat st

( n1 in NatDivisors n0 & m1 in NatDivisors m0 & k = n1 * m1 )

proof end;

theorem Th19: :: NAT_5:19

for n, p being Nat st p is prime holds

NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n }

NatDivisors (p |^ n) = { (p |^ k) where k is Element of NAT : k <= n }

proof end;

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

n1 = n2

proof end;

theorem :: NAT_5:21

Lm4: for k, m being Nat holds

( k < m iff k <= m - 1 )

proof end;

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 )

proof end;

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

proof end;

Lm7: for fs being FinSequence st 1 <= len fs holds

( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> )

proof end;

Lm8: for a being Nat

for ft being FinSequence of REAL st a in dom ft holds

(Product (Del (ft,a))) * (ft . a) = Product ft

proof end;

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 )

proof end;

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

proof end;

definition

let I be set ;

let f be Function of I,NAT;

let J be finite Subset of I;

:: original: |

redefine func f | J -> bag of J;

correctness

coherence

f | J is bag of J;

;

end;
let f be Function of I,NAT;

let J be finite Subset of I;

:: original: |

redefine func f | J -> bag of J;

correctness

coherence

f | J is bag of J;

;

registration

let I be set ;

let f be Function of I,NAT;

let J be finite Subset of I;

correctness

coherence

Sum (f | J) is natural ;

end;
let f be Function of I,NAT;

let J be finite Subset of I;

correctness

coherence

Sum (f | J) is natural ;

proof end;

theorem Th24: :: NAT_5:24

for f being sequence of NAT

for F being sequence of 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)))

for F being sequence of 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)))

proof end;

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)

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)

proof end;

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))

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))

proof end;

theorem Th27: :: NAT_5:27

for I being set

for f being Function of I,NAT

for J being finite Subset of I

for j being object st J = {j} holds

Sum (f | J) = f . j

for f being Function of I,NAT

for J being finite Subset of I

for j being object st J = {j} holds

Sum (f | J) = f . j

proof end;

Lm11: for I being set

for f, g being Function of I,NAT

for J, K being finite Subset of I

for j being object st J = {j} holds

Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))

proof end;

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))

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))

proof end;

definition

let k be natural Number ;

existence

ex b_{1} being sequence of NAT st

for n being Nat holds b_{1} . n = n |^ k

for b_{1}, b_{2} being sequence of NAT st ( for n being Nat holds b_{1} . n = n |^ k ) & ( for n being Nat holds b_{2} . n = n |^ k ) holds

b_{1} = b_{2}

end;
existence

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines EXP NAT_5:def 1 :

for k being natural Number

for b_{2} being sequence of NAT holds

( b_{2} = EXP k iff for n being Nat holds b_{2} . n = n |^ k );

for k being natural Number

for b

( b

definition

let k, n be natural Number ;

consistency

for b_{1} being Element of NAT holds verum;

existence

( ( for b_{1} being Element of NAT holds verum ) & ( n <> 0 implies ex b_{1} being Element of NAT st

for m being non zero Nat st n = m holds

b_{1} = Sum ((EXP k) | (NatDivisors m)) ) & ( not n <> 0 implies ex b_{1} being Element of NAT st b_{1} = 0 ) );

uniqueness

for b_{1}, b_{2} being Element of NAT holds

( ( n <> 0 & ( for m being non zero Nat st n = m holds

b_{1} = Sum ((EXP k) | (NatDivisors m)) ) & ( for m being non zero Nat st n = m holds

b_{2} = Sum ((EXP k) | (NatDivisors m)) ) implies b_{1} = b_{2} ) & ( not n <> 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) );

end;
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 for m being non zero Nat st n = m holds

it = Sum ((EXP k) | (NatDivisors m)) if n <> 0

otherwise it = 0 ;

consistency

for b

existence

( ( for b

for m being non zero Nat st n = m holds

b

uniqueness

for b

( ( n <> 0 & ( for m being non zero Nat st n = m holds

b

b

proof end;

:: deftheorem Def2 defines sigma NAT_5:def 2 :

for k, n being natural Number

for b_{3} being Element of NAT holds

( ( n <> 0 implies ( b_{3} = sigma (k,n) iff for m being non zero Nat st n = m holds

b_{3} = Sum ((EXP k) | (NatDivisors m)) ) ) & ( not n <> 0 implies ( b_{3} = sigma (k,n) iff b_{3} = 0 ) ) );

for k, n being natural Number

for b

( ( n <> 0 implies ( b

b

definition

let k be natural Number ;

ex b_{1} being sequence of NAT st

for n being Nat holds b_{1} . n = sigma (k,n)

for b_{1}, b_{2} being sequence of NAT st ( for n being Nat holds b_{1} . n = sigma (k,n) ) & ( for n being Nat holds b_{2} . n = sigma (k,n) ) holds

b_{1} = b_{2}

end;
func Sigma k -> sequence of NAT means :Def3: :: NAT_5:def 3

for n being Nat holds it . n = sigma (k,n);

existence for n being Nat holds it . n = sigma (k,n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Sigma NAT_5:def 3 :

for k being natural Number

for b_{2} being sequence of NAT holds

( b_{2} = Sigma k iff for n being Nat holds b_{2} . n = sigma (k,n) );

for k being natural Number

for b

( b

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

for n0 being non zero Nat st m divides n0 & n0 <> m & m <> 1 holds

(1 + m) + n0 <= sigma n0

proof end;

theorem Th32: :: NAT_5:32

for k, m 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

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

proof end;

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 )

for n0 being non zero Nat st sigma n0 = n0 + m & m divides n0 & n0 <> m holds

( m = 1 & n0 is prime )

proof end;

definition

let f be sequence of NAT;

end;
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);

for n0, m0 being non zero Nat st n0,m0 are_coprime holds

f . (n0 * m0) = (f . n0) * (f . m0);

:: deftheorem defines multiplicative NAT_5:def 5 :

for f being sequence of NAT holds

( f is multiplicative iff for n0, m0 being non zero Nat st n0,m0 are_coprime holds

f . (n0 * m0) = (f . n0) * (f . m0) );

for f being sequence of NAT holds

( f is multiplicative iff for n0, m0 being non zero Nat st n0,m0 are_coprime holds

f . (n0 * m0) = (f . n0) * (f . m0) );

theorem Th34: :: NAT_5:34

for f, F being sequence of NAT st f is multiplicative & ( for n0 being non zero Nat holds F . n0 = Sum (f | (NatDivisors n0)) ) holds

F is multiplicative

F is multiplicative

proof end;

definition
end;

:: deftheorem defines perfect NAT_5:def 6 :

for n0 being natural non zero Number holds

( n0 is perfect iff sigma n0 = 2 * n0 );

for n0 being natural non zero Number holds

( n0 is perfect iff sigma n0 = 2 * n0 );

:: Fundamentals of Number Theory (LeVeque) p.123

:: Euclid

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

for n0 being non zero Nat st (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) holds

n0 is perfect

proof end;

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) )

ex p being Nat st

( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) )

proof end;

definition

ex b_{1} being sequence of NAT st

for k being Element of NAT holds b_{1} . k = Euler k

for b_{1}, b_{2} being sequence of NAT st ( for k being Element of NAT holds b_{1} . k = Euler k ) & ( for k being Element of NAT holds b_{2} . k = Euler k ) holds

b_{1} = b_{2}
end;

func Euler_phi -> sequence of NAT means :Def7: :: NAT_5:def 7

for k being Element of NAT holds it . k = Euler k;

existence for k being Element of NAT holds it . k = Euler k;

ex b

for k being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines Euler_phi NAT_5:def 7 :

for b_{1} being sequence of NAT holds

( b_{1} = Euler_phi iff for k being Element of NAT holds b_{1} . k = Euler k );

for b

( b

:: Number Theory (Andrews) p.76