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

Definition df-mu 23102
 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 23096 . 2
2 vx . . 3
3 cn 10532 . . 3
4 vp . . . . . . . 8
54cv 1378 . . . . . . 7
6 c2 10581 . . . . . . 7
7 cexp 12130 . . . . . . 7
85, 6, 7co 6282 . . . . . 6
92cv 1378 . . . . . 6
10 cdivides 13843 . . . . . 6
118, 9, 10wbr 4447 . . . . 5
12 cprime 14072 . . . . 5
1311, 4, 12wrex 2815 . . . 4
14 cc0 9488 . . . 4
15 c1 9489 . . . . . 6
1615cneg 9802 . . . . 5
175, 9, 10wbr 4447 . . . . . . 7
1817, 4, 12crab 2818 . . . . . 6
19 chash 12369 . . . . . 6
2018, 19cfv 5586 . . . . 5
2116, 20, 7co 6282 . . . 4
2213, 14, 21cif 3939 . . 3
232, 3, 22cmpt 4505 . 2
241, 23wceq 1379 1
 Colors of variables: wff setvar class This definition is referenced by:  muval  23134  muf  23142
 Copyright terms: Public domain W3C validator