:: by Magdalena Jastrz\c{e}bska and Adam Grabowski

::

:: Received March 21, 2006

:: Copyright (c) 2006-2012 Association of Mizar Users

begin

Lm1: for X, Y, Z, x being set st X misses Y & x in X /\ Z holds

not x in Y /\ Z

proof end;

registration

ex b_{1} being Element of NAT st

( not b_{1} is prime & not b_{1} is zero )
by INT_2:29;

end;

cluster non zero epsilon-transitive epsilon-connected ordinal natural V11() real V13() non prime finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() for Element of NAT ;

existence ex b

( not b

Lm2: for n being Nat st n <> 1 holds

ex p being Prime st p divides n

proof end;

theorem Th11: :: MOEBIUS1:11

for p being prime Element of NAT

for m, n being non zero Element of NAT st m,n are_relative_prime & p |^ 2 divides m * n & not p |^ 2 divides m holds

p |^ 2 divides n

for m, n being non zero Element of NAT st m,n are_relative_prime & p |^ 2 divides m * n & not p |^ 2 divides m holds

p |^ 2 divides n

proof end;

theorem :: MOEBIUS1:13

for n being Nat

for p being Prime st p divides n holds

{ d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }

for p being Prime st p divides n holds

{ d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }

proof end;

theorem Th15: :: MOEBIUS1:15

for n being non zero Element of NAT

for p being Prime st not p in support (ppf n) holds

p |-count n = 0

for p being Prime st not p in support (ppf n) holds

p |-count n = 0

proof end;

theorem Th16: :: MOEBIUS1:16

for k being Element of NAT

for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) & not support (ppf n) c= Seg k holds

k + 1 is Prime

for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) & not support (ppf n) c= Seg k holds

k + 1 is Prime

proof end;

theorem Th17: :: MOEBIUS1:17

for m, n being non zero Nat st ( for p being Prime holds p |-count m <= p |-count n ) holds

support (ppf m) c= support (ppf n)

support (ppf m) c= support (ppf n)

proof end;

theorem Th18: :: MOEBIUS1:18

for k being Element of NAT

for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) holds

ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) holds

ex m being non zero Element of NAT ex e being Element of NAT st

( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds

( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

proof end;

theorem Th19: :: MOEBIUS1:19

for m, n being non zero Nat st ( for p being Prime holds p |-count m <= p |-count n ) holds

m divides n

m divides n

proof end;

begin

:: deftheorem Def1 defines square-containing MOEBIUS1:def 1 :

for x being Nat holds

( x is square-containing iff ex p being Prime st p |^ 2 divides x );

for x being Nat holds

( x is square-containing iff ex p being Prime st p |^ 2 divides x );

theorem Th20: :: MOEBIUS1:20

for n being Nat st ex p being non zero Nat st

( p <> 1 & p |^ 2 divides n ) holds

n is square-containing

( p <> 1 & p |^ 2 divides n ) holds

n is square-containing

proof end;

registration
end;

definition

ex b_{1} being Subset of NAT st

for n being Nat holds

( n in b_{1} iff n is square-free )

for b_{1}, b_{2} being Subset of NAT st ( for n being Nat holds

( n in b_{1} iff n is square-free ) ) & ( for n being Nat holds

( n in b_{2} iff n is square-free ) ) holds

b_{1} = b_{2}
end;

func SCNAT -> Subset of NAT means :Def2: :: MOEBIUS1:def 2

for n being Nat holds

( n in it iff n is square-free );

existence for n being Nat holds

( n in it iff n is square-free );

ex b

for n being Nat holds

( n in b

proof end;

uniqueness for b

( n in b

( n in b

b

proof end;

:: deftheorem Def2 defines SCNAT MOEBIUS1:def 2 :

for b_{1} being Subset of NAT holds

( b_{1} = SCNAT iff for n being Nat holds

( n in b_{1} iff n is square-free ) );

for b

( b

( n in b

registration

ex b_{1} being Nat st b_{1} is square-free
by Th22;

ex b_{1} being Nat st b_{1} is square-containing
end;

cluster epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative square-free for set ;

existence ex b

cluster epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative square-containing for set ;

existence ex b

proof end;

registration

coherence

for b_{1} being Nat st b_{1} is square & not b_{1} is trivial holds

b_{1} is square-containing

end;
for b

b

proof end;

theorem Th27: :: MOEBIUS1:27

for p being Prime

for m, d being Nat st m is square-free & p divides m & d divides m div p holds

( d divides m & not p divides d )

for m, d being Nat st m is square-free & p divides m & d divides m div p holds

( d divides m & not p divides d )

proof end;

theorem Th28: :: MOEBIUS1:28

for p being Prime

for m, d being Nat st p divides m & d divides m & not p divides d holds

d divides m div p

for m, d being Nat st p divides m & d divides m & not p divides d holds

d divides m div p

proof end;

theorem :: MOEBIUS1:29

for p being Prime

for m being Nat st m is square-free & p divides m holds

{ d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } = { d where d is Element of NAT : ( 0 < d & d divides m div p ) }

for m being Nat st m is square-free & p divides m holds

{ d where d is Element of NAT : ( 0 < d & d divides m & not p divides d ) } = { d where d is Element of NAT : ( 0 < d & d divides m div p ) }

proof end;

begin

definition

let n be Nat;

for b_{1} being real number holds verum
;

existence

( ( n is square-containing implies ex b_{1} being real number st b_{1} = 0 ) & ( not n is square-containing implies ex b_{1} being real number ex n9 being non zero Nat st

( n9 = n & b_{1} = (- 1) |^ (card (support (ppf n9))) ) ) )

for b_{1}, b_{2} being real number holds

( ( n is square-containing & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) & ( not n is square-containing & ex n9 being non zero Nat st

( n9 = n & b_{1} = (- 1) |^ (card (support (ppf n9))) ) & ex n9 being non zero Nat st

( n9 = n & b_{2} = (- 1) |^ (card (support (ppf n9))) ) implies b_{1} = b_{2} ) )
;

end;
:: Moebius function

func Moebius n -> real number means :Def3: :: MOEBIUS1:def 3

it = 0 if n is square-containing

otherwise ex n9 being non zero Nat st

( n9 = n & it = (- 1) |^ (card (support (ppf n9))) );

consistency it = 0 if n is square-containing

otherwise ex n9 being non zero Nat st

( n9 = n & it = (- 1) |^ (card (support (ppf n9))) );

for b

existence

( ( n is square-containing implies ex b

( n9 = n & b

proof end;

uniqueness for b

( ( n is square-containing & b

( n9 = n & b

( n9 = n & b

:: deftheorem Def3 defines Moebius MOEBIUS1:def 3 :

for n being Nat

for b_{2} being real number holds

( ( n is square-containing implies ( b_{2} = Moebius n iff b_{2} = 0 ) ) & ( not n is square-containing implies ( b_{2} = Moebius n iff ex n9 being non zero Nat st

( n9 = n & b_{2} = (- 1) |^ (card (support (ppf n9))) ) ) ) );

for n being Nat

for b

( ( n is square-containing implies ( b

( n9 = n & b

theorem Th35: :: MOEBIUS1:35

for m, n being non zero Element of NAT st m,n are_relative_prime holds

Moebius (m * n) = (Moebius m) * (Moebius n)

Moebius (m * n) = (Moebius m) * (Moebius n)

proof end;

theorem :: MOEBIUS1:36

for p being Prime

for n being Element of NAT st 1 <= n & n * p is square-free holds

Moebius (n * p) = - (Moebius n)

for n being Element of NAT st 1 <= n & n * p is square-free holds

Moebius (n * p) = - (Moebius n)

proof end;

begin

definition

let n be Nat;

{ k where k is Element of NAT : ( k <> 0 & k divides n ) } is Subset of NAT

end;
func NatDivisors n -> Subset of NAT equals :: MOEBIUS1:def 4

{ k where k is Element of NAT : ( k <> 0 & k divides n ) } ;

coherence { k where k is Element of NAT : ( k <> 0 & k divides n ) } ;

{ k where k is Element of NAT : ( k <> 0 & k divides n ) } is Subset of NAT

proof end;

:: deftheorem defines NatDivisors MOEBIUS1:def 4 :

for n being Nat holds NatDivisors n = { k where k is Element of NAT : ( k <> 0 & k divides n ) } ;

for n being Nat holds NatDivisors n = { k where k is Element of NAT : ( k <> 0 & k divides n ) } ;

registration

let n be non zero Nat;

coherence

( NatDivisors n is finite & NatDivisors n is with_non-empty_elements )

end;
coherence

( NatDivisors n is finite & NatDivisors n is with_non-empty_elements )

proof end;

begin

definition

let X be set ;

ex b_{1} being ManySortedSet of NAT st

( support b_{1} = X /\ SCNAT & ( for k being Element of NAT st k in support b_{1} holds

b_{1} . k = Moebius k ) )

for b_{1}, b_{2} being ManySortedSet of NAT st support b_{1} = X /\ SCNAT & ( for k being Element of NAT st k in support b_{1} holds

b_{1} . k = Moebius k ) & support b_{2} = X /\ SCNAT & ( for k being Element of NAT st k in support b_{2} holds

b_{2} . k = Moebius k ) holds

b_{1} = b_{2}

end;
func SMoebius X -> ManySortedSet of NAT means :Def5: :: MOEBIUS1:def 5

( support it = X /\ SCNAT & ( for k being Element of NAT st k in support it holds

it . k = Moebius k ) );

existence ( support it = X /\ SCNAT & ( for k being Element of NAT st k in support it holds

it . k = Moebius k ) );

ex b

( support b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines SMoebius MOEBIUS1:def 5 :

for X being set

for b_{2} being ManySortedSet of NAT holds

( b_{2} = SMoebius X iff ( support b_{2} = X /\ SCNAT & ( for k being Element of NAT st k in support b_{2} holds

b_{2} . k = Moebius k ) ) );

for X being set

for b

( b

b

registration
end;

theorem :: MOEBIUS1:43

for X, Y being finite Subset of NAT st X misses Y holds

(support (SMoebius X)) \/ (support (SMoebius Y)) = support ((SMoebius X) + (SMoebius Y))

(support (SMoebius X)) \/ (support (SMoebius Y)) = support ((SMoebius X) + (SMoebius Y))

proof end;

theorem :: MOEBIUS1:44

for X, Y being finite Subset of NAT st X misses Y holds

SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y)

SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y)

proof end;

begin

definition

let n be non zero Nat;

ex b_{1} being ManySortedSet of SetPrimes st

( support b_{1} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{1} . p = p ) )

for b_{1}, b_{2} being ManySortedSet of SetPrimes st support b_{1} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{1} . p = p ) & support b_{2} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{2} . p = p ) holds

b_{1} = b_{2}

end;
func PFactors n -> ManySortedSet of SetPrimes means :Def6: :: MOEBIUS1:def 6

( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

it . p = p ) );

existence ( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

it . p = p ) );

ex b

( support b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines PFactors MOEBIUS1:def 6 :

for n being non zero Nat

for b_{2} being ManySortedSet of SetPrimes holds

( b_{2} = PFactors n iff ( support b_{2} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{2} . p = p ) ) );

for n being non zero Nat

for b

( b

b

registration

let n be non zero Nat;

coherence

( PFactors n is finite-support & PFactors n is natural-valued )

end;
coherence

( PFactors n is finite-support & PFactors n is natural-valued )

proof end;

theorem Th50: :: MOEBIUS1:50

for m, n being non zero Element of NAT st m,n are_relative_prime holds

PFactors (m * n) = (PFactors m) + (PFactors n)

PFactors (m * n) = (PFactors m) + (PFactors n)

proof end;

theorem :: MOEBIUS1:51

for n being non zero Element of NAT

for A being finite Subset of NAT st A = { k where k is Element of NAT : ( 0 < k & k divides n & k is square-containing ) } holds

SMoebius A = EmptyBag NAT

for A being finite Subset of NAT st A = { k where k is Element of NAT : ( 0 < k & k divides n & k is square-containing ) } holds

SMoebius A = EmptyBag NAT

proof end;

begin

:: deftheorem defines Radical MOEBIUS1:def 7 :

for n being non zero Nat holds Radical n = Product (PFactors n);

for n being non zero Nat holds Radical n = Product (PFactors n);

registration
end;

theorem :: MOEBIUS1:59

Lm3: for n being non zero Nat

for p being Prime holds not p |^ 2 divides Radical n

proof end;

Lm4: for n being non zero Nat holds Radical n is square-free

proof end;

theorem :: MOEBIUS1:63

for n being non zero Element of NAT

for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } c= Seg n

for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } c= Seg n

proof end;

theorem :: MOEBIUS1:64

for n being non zero Element of NAT

for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } c= Seg n

for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } c= Seg n

proof end;

Lm5: for m, n being non zero Element of NAT st m divides n & m is square-free holds

m divides Radical n

proof end;

theorem :: MOEBIUS1:66

for n being non zero Nat holds { k where k is Element of NAT : ( 0 < k & k divides n & k is square-free ) } = { k where k is Element of NAT : ( 0 < k & k divides Radical n ) }

proof end;