Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mu Structured version   Unicode version

Definition df-mu 20885
 Description: Define the Möbius function, which is zero for non-squarefree numbers and is or for squarefree numbers according as to the number of prime divisors of the number is even or odd. (Contributed by Mario Carneiro, 22-Sep-2014.)
Assertion
Ref Expression
df-mu
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-mu
StepHypRef Expression
1 cmu 20879 . 2
2 vx . . 3
3 cn 10002 . . 3
4 vp . . . . . . . 8
54cv 1652 . . . . . . 7
6 c2 10051 . . . . . . 7
7 cexp 11384 . . . . . . 7
85, 6, 7co 6083 . . . . . 6
92cv 1652 . . . . . 6
10 cdivides 12854 . . . . . 6
118, 9, 10wbr 4214 . . . . 5
12 cprime 13081 . . . . 5
1311, 4, 12wrex 2708 . . . 4
14 cc0 8992 . . . 4
15 c1 8993 . . . . . 6
1615cneg 9294 . . . . 5
175, 9, 10wbr 4214 . . . . . . 7
1817, 4, 12crab 2711 . . . . . 6
19 chash 11620 . . . . . 6
2018, 19cfv 5456 . . . . 5
2116, 20, 7co 6083 . . . 4
2213, 14, 21cif 3741 . . 3
232, 3, 22cmpt 4268 . 2
241, 23wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  muval  20917  muf  20925
 Copyright terms: Public domain W3C validator