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

Definition df-mu 20354
Description: Define the Möbius function, which is zero for non-squarefree numbers and is  -u 1 or  1 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  |-  mmu  =  ( x  e.  NN  |->  if ( E. p  e. 
Prime  ( p ^ 2 )  ||  x ,  0 ,  ( -u
1 ^ ( # `  { p  e.  Prime  |  p  ||  x }
) ) ) )
Distinct variable group:    x, p

Detailed syntax breakdown of Definition df-mu
StepHypRef Expression
1 cmu 20348 . 2  class  mmu
2 vx . . 3  set  x
3 cn 9762 . . 3  class  NN
4 vp . . . . . . . 8  set  p
54cv 1631 . . . . . . 7  class  p
6 c2 9811 . . . . . . 7  class  2
7 cexp 11120 . . . . . . 7  class  ^
85, 6, 7co 5874 . . . . . 6  class  ( p ^ 2 )
92cv 1631 . . . . . 6  class  x
10 cdivides 12547 . . . . . 6  class  ||
118, 9, 10wbr 4039 . . . . 5  wff  ( p ^ 2 )  ||  x
12 cprime 12774 . . . . 5  class  Prime
1311, 4, 12wrex 2557 . . . 4  wff  E. p  e.  Prime  ( p ^
2 )  ||  x
14 cc0 8753 . . . 4  class  0
15 c1 8754 . . . . . 6  class  1
1615cneg 9054 . . . . 5  class  -u 1
175, 9, 10wbr 4039 . . . . . . 7  wff  p  ||  x
1817, 4, 12crab 2560 . . . . . 6  class  { p  e.  Prime  |  p  ||  x }
19 chash 11353 . . . . . 6  class  #
2018, 19cfv 5271 . . . . 5  class  ( # `  { p  e.  Prime  |  p  ||  x }
)
2116, 20, 7co 5874 . . . 4  class  ( -u
1 ^ ( # `  { p  e.  Prime  |  p  ||  x }
) )
2213, 14, 21cif 3578 . . 3  class  if ( E. p  e.  Prime  ( p ^ 2 ) 
||  x ,  0 ,  ( -u 1 ^ ( # `  {
p  e.  Prime  |  p 
||  x } ) ) )
232, 3, 22cmpt 4093 . 2  class  ( x  e.  NN  |->  if ( E. p  e.  Prime  ( p ^ 2 ) 
||  x ,  0 ,  ( -u 1 ^ ( # `  {
p  e.  Prime  |  p 
||  x } ) ) ) )
241, 23wceq 1632 1  wff  mmu  =  ( x  e.  NN  |->  if ( E. p  e. 
Prime  ( p ^ 2 )  ||  x ,  0 ,  ( -u
1 ^ ( # `  { p  e.  Prime  |  p  ||  x }
) ) ) )
Colors of variables: wff set class
This definition is referenced by:  muval  20386  muf  20394
  Copyright terms: Public domain W3C validator