:: On the Properties of the {M}\"obius Function :: 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 proofend; scheme :: MOEBIUS1:sch 1 LambdaNATC{ F1() -> Element of NAT , F2() -> set , F3( set ) -> set } : ex f being Function of NAT,F2() st ( f . 0 = F1() & ( for x being non zero Element of NAT holds f . x = F3(x) ) ) provided A1: F1() in F2() and A2: for x being non zero Element of NAT holds F3(x) in F2() proofend; registration 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 b1 being Element of NAT st ( not b1 is prime & not b1 is zero ) by INT_2:29; end; theorem Th1: :: MOEBIUS1:1 for n being non zero Nat st n <> 1 holds n >= 2 proofend; theorem :: MOEBIUS1:2 for k, n, i being Nat st 1 <= k holds ( i in Seg n iff k * i in Seg (k * n) ) proofend; theorem :: MOEBIUS1:3 for m, n being Element of NAT holds ( not m,n are_relative_prime or m > 0 or n > 0 ) proofend; Lm2: for n being Nat st n <> 1 holds ex p being Prime st p divides n proofend; theorem Th4: :: MOEBIUS1:4 for n being non prime Element of NAT st n <> 1 holds ex p being Prime st ( p divides n & p <> n ) proofend; theorem Th5: :: MOEBIUS1:5 for n being Nat st n <> 1 holds ex p being Prime st p divides n proofend; theorem Th6: :: MOEBIUS1:6 for p being Prime for n being non zero Nat holds ( p divides n iff p |-count n > 0 ) proofend; theorem Th7: :: MOEBIUS1:7 support (ppf 1) = {} proofend; theorem Th8: :: MOEBIUS1:8 for p being Prime holds support (ppf p) = {p} proofend; theorem Th9: :: MOEBIUS1:9 for n, m being Nat for p being Prime st n <> 0 & m <= p |-count n holds p |^ m divides n proofend; theorem Th10: :: MOEBIUS1:10 for a being Element of NAT for p being Prime st p |^ 2 divides a holds p divides a proofend; 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 proofend; theorem Th12: :: MOEBIUS1:12 for n being Nat for N being Rbag of NAT st support N = {n} holds Sum N = N . n proofend; registration cluster canFS {} -> empty ; coherence canFS {} is empty ; 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 ) } proofend; theorem Th14: :: MOEBIUS1:14 for n being non zero Nat ex k being Element of NAT st support (ppf n) c= Seg k proofend; 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 proofend; 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 proofend; 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) proofend; 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 ) ) ) ) proofend; 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 proofend; begin definition let x be Nat; attrx is square-containing means :Def1: :: MOEBIUS1:def 1 ex p being Prime st p |^ 2 divides x; end; :: 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 ); 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 proofend; notation let x be Nat; antonym square-free x for square-containing ; end; theorem Th21: :: MOEBIUS1:21 0 is square-containing proofend; theorem Th22: :: MOEBIUS1:22 1 is square-free proofend; theorem Th23: :: MOEBIUS1:23 for p being Prime holds p is square-free proofend; registration cluster prime -> square-free for Element of NAT ; coherence for b1 being Element of NAT st b1 is prime holds b1 is square-free by Th23; end; definition func SCNAT -> Subset of NAT means :Def2: :: MOEBIUS1:def 2 for n being Nat holds ( n in it iff n is square-free ); existence ex b1 being Subset of NAT st for n being Nat holds ( n in b1 iff n is square-free ) proofend; uniqueness for b1, b2 being Subset of NAT st ( for n being Nat holds ( n in b1 iff n is square-free ) ) & ( for n being Nat holds ( n in b2 iff n is square-free ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines SCNAT MOEBIUS1:def_2_:_ for b1 being Subset of NAT holds ( b1 = SCNAT iff for n being Nat holds ( n in b1 iff n is square-free ) ); registration cluster epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative square-free for set ; existence ex b1 being Nat st b1 is square-free by Th22; cluster epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative square-containing for set ; existence ex b1 being Nat st b1 is square-containing proofend; end; registration cluster non trivial natural square -> square-containing for set ; coherence for b1 being Nat st b1 is square & not b1 is trivial holds b1 is square-containing proofend; end; theorem Th24: :: MOEBIUS1:24 for n being Nat st n is square-free holds for p being Prime holds p |-count n <= 1 proofend; theorem Th25: :: MOEBIUS1:25 for m, n being Nat st m * n is square-free holds m is square-free proofend; theorem Th26: :: MOEBIUS1:26 for m, n being Nat st m is square-free & n divides m holds n is square-free proofend; 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 ) proofend; 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 proofend; 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 ) } proofend; begin definition let n be Nat; 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 for b1 being real number holds verum ; existence ( ( n is square-containing implies ex b1 being real number st b1 = 0 ) & ( not n is square-containing implies ex b1 being real number ex n9 being non zero Nat st ( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) ) ) proofend; uniqueness for b1, b2 being real number holds ( ( n is square-containing & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not n is square-containing & ex n9 being non zero Nat st ( n9 = n & b1 = (- 1) |^ (card (support (ppf n9))) ) & ex n9 being non zero Nat st ( n9 = n & b2 = (- 1) |^ (card (support (ppf n9))) ) implies b1 = b2 ) ) ; end; :: deftheorem Def3 defines Moebius MOEBIUS1:def_3_:_ for n being Nat for b2 being real number holds ( ( n is square-containing implies ( b2 = Moebius n iff b2 = 0 ) ) & ( not n is square-containing implies ( b2 = Moebius n iff ex n9 being non zero Nat st ( n9 = n & b2 = (- 1) |^ (card (support (ppf n9))) ) ) ) ); theorem Th30: :: MOEBIUS1:30 Moebius 1 = 1 proofend; theorem :: MOEBIUS1:31 Moebius 2 = - 1 proofend; theorem :: MOEBIUS1:32 Moebius 3 = - 1 proofend; theorem Th33: :: MOEBIUS1:33 for n being Nat st n is square-free holds Moebius n <> 0 proofend; registration let n be square-free Nat; cluster Moebius n -> non zero real ; coherence not Moebius n is empty by Th33; end; theorem Th34: :: MOEBIUS1:34 for p being Prime holds Moebius p = - 1 proofend; 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) proofend; 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) proofend; theorem :: MOEBIUS1:37 for m, n being non zero Element of NAT st not m,n are_relative_prime holds Moebius (m * n) = 0 proofend; theorem Th38: :: MOEBIUS1:38 for n being Nat holds ( n in SCNAT iff Moebius n <> 0 ) proofend; begin definition let n be Nat; 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 ) } is Subset of NAT proofend; 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 ) } ; theorem :: MOEBIUS1:39 for n, k being Nat holds ( k in NatDivisors n iff ( 0 < k & k divides n ) ) proofend; theorem Th40: :: MOEBIUS1:40 for n being non zero Nat holds NatDivisors n c= Seg n proofend; registration let n be non zero Nat; cluster NatDivisors n -> finite with_non-empty_elements ; coherence ( NatDivisors n is finite & NatDivisors n is with_non-empty_elements ) proofend; end; theorem Th41: :: MOEBIUS1:41 NatDivisors 1 = {1} proofend; begin definition let X be set ; 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 ex b1 being ManySortedSet of NAT st ( support b1 = X /\ SCNAT & ( for k being Element of NAT st k in support b1 holds b1 . k = Moebius k ) ) proofend; uniqueness for b1, b2 being ManySortedSet of NAT st support b1 = X /\ SCNAT & ( for k being Element of NAT st k in support b1 holds b1 . k = Moebius k ) & support b2 = X /\ SCNAT & ( for k being Element of NAT st k in support b2 holds b2 . k = Moebius k ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines SMoebius MOEBIUS1:def_5_:_ for X being set for b2 being ManySortedSet of NAT holds ( b2 = SMoebius X iff ( support b2 = X /\ SCNAT & ( for k being Element of NAT st k in support b2 holds b2 . k = Moebius k ) ) ); registration let X be set ; cluster SMoebius X -> real-valued ; coherence SMoebius X is real-valued proofend; end; registration let X be finite set ; cluster SMoebius X -> finite-support ; coherence SMoebius X is finite-support proofend; end; theorem :: MOEBIUS1:42 Sum (SMoebius (NatDivisors 1)) = 1 proofend; 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)) proofend; theorem :: MOEBIUS1:44 for X, Y being finite Subset of NAT st X misses Y holds SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y) proofend; begin definition let n be non zero Nat; 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 ex b1 being ManySortedSet of SetPrimes st ( support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds b1 . p = p ) ) proofend; uniqueness for b1, b2 being ManySortedSet of SetPrimes st support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds b1 . p = p ) & support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds b2 . p = p ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines PFactors MOEBIUS1:def_6_:_ for n being non zero Nat for b2 being ManySortedSet of SetPrimes holds ( b2 = PFactors n iff ( support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds b2 . p = p ) ) ); registration let n be non zero Nat; cluster PFactors n -> natural-valued finite-support ; coherence ( PFactors n is finite-support & PFactors n is natural-valued ) proofend; end; theorem Th45: :: MOEBIUS1:45 PFactors 1 = EmptyBag SetPrimes proofend; theorem Th46: :: MOEBIUS1:46 for p being Prime holds (PFactors p) * <*p*> = <*p*> proofend; theorem Th47: :: MOEBIUS1:47 for p being Prime for n being non zero Nat holds (PFactors (p |^ n)) * <*p*> = <*p*> proofend; theorem Th48: :: MOEBIUS1:48 for p being Prime for n being non zero Nat st p |-count n = 0 holds (PFactors n) . p = 0 proofend; theorem Th49: :: MOEBIUS1:49 for n being non zero Nat for p being Prime st p |-count n <> 0 holds (PFactors n) . p = p proofend; 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) proofend; 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 proofend; begin definition let n be non zero Nat; func Radical n -> Element of NAT equals :: MOEBIUS1:def 7 Product (PFactors n); coherence Product (PFactors n) is Element of NAT ; end; :: deftheorem defines Radical MOEBIUS1:def_7_:_ for n being non zero Nat holds Radical n = Product (PFactors n); theorem Th52: :: MOEBIUS1:52 for n being non zero Nat holds Radical n > 0 proofend; registration let n be non zero Nat; cluster Radical n -> non zero ; coherence not Radical n is empty by Th52; end; theorem :: MOEBIUS1:53 for p being Prime holds p = Radical p proofend; theorem Th54: :: MOEBIUS1:54 for p being Prime for n being non zero Element of NAT holds Radical (p |^ n) = p proofend; theorem Th55: :: MOEBIUS1:55 for n being non zero Nat holds Radical n divides n proofend; theorem Th56: :: MOEBIUS1:56 for p being Prime for n being non zero Nat holds ( p divides n iff p divides Radical n ) proofend; theorem Th57: :: MOEBIUS1:57 for k being non zero Nat st k is square-free holds Radical k = k proofend; theorem :: MOEBIUS1:58 for n being non zero Nat holds Radical n <= n by Th55, NAT_D:7; theorem :: MOEBIUS1:59 for p being Prime for n being non zero Nat holds p |-count (Radical n) <= p |-count n by Th55, NAT_3:30; theorem :: MOEBIUS1:60 for n being non zero Nat holds ( Radical n = 1 iff n = 1 ) proofend; theorem Th61: :: MOEBIUS1:61 for p being Prime for n being non zero Nat holds p |-count (Radical n) <= 1 proofend; Lm3: for n being non zero Nat for p being Prime holds not p |^ 2 divides Radical n proofend; Lm4: for n being non zero Nat holds Radical n is square-free proofend; registration let n be non zero Nat; cluster Radical n -> square-free ; coherence not Radical n is square-containing by Lm4; end; theorem :: MOEBIUS1:62 for n being non zero Nat holds Radical (Radical n) = Radical n by Th57; 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 proofend; 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 proofend; Lm5: for m, n being non zero Element of NAT st m divides n & m is square-free holds m divides Radical n proofend; theorem Th65: :: MOEBIUS1:65 for k, n being non zero Nat holds ( ( k divides n & k is square-free ) iff k divides Radical n ) proofend; 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 ) } proofend;