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

Definition df-mu 22453
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 22447 . 2  class  mmu
2 vx . . 3  setvar  x
3 cn 10337 . . 3  class  NN
4 vp . . . . . . . 8  setvar  p
54cv 1368 . . . . . . 7  class  p
6 c2 10386 . . . . . . 7  class  2
7 cexp 11880 . . . . . . 7  class  ^
85, 6, 7co 6106 . . . . . 6  class  ( p ^ 2 )
92cv 1368 . . . . . 6  class  x
10 cdivides 13550 . . . . . 6  class  ||
118, 9, 10wbr 4307 . . . . 5  wff  ( p ^ 2 )  ||  x
12 cprime 13778 . . . . 5  class  Prime
1311, 4, 12wrex 2731 . . . 4  wff  E. p  e.  Prime  ( p ^
2 )  ||  x
14 cc0 9297 . . . 4  class  0
15 c1 9298 . . . . . 6  class  1
1615cneg 9611 . . . . 5  class  -u 1
175, 9, 10wbr 4307 . . . . . . 7  wff  p  ||  x
1817, 4, 12crab 2734 . . . . . 6  class  { p  e.  Prime  |  p  ||  x }
19 chash 12118 . . . . . 6  class  #
2018, 19cfv 5433 . . . . 5  class  ( # `  { p  e.  Prime  |  p  ||  x }
)
2116, 20, 7co 6106 . . . 4  class  ( -u
1 ^ ( # `  { p  e.  Prime  |  p  ||  x }
) )
2213, 14, 21cif 3806 . . 3  class  if ( E. p  e.  Prime  ( p ^ 2 ) 
||  x ,  0 ,  ( -u 1 ^ ( # `  {
p  e.  Prime  |  p 
||  x } ) ) )
232, 3, 22cmpt 4365 . 2  class  ( x  e.  NN  |->  if ( E. p  e.  Prime  ( p ^ 2 ) 
||  x ,  0 ,  ( -u 1 ^ ( # `  {
p  e.  Prime  |  p 
||  x } ) ) ) )
241, 23wceq 1369 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 setvar class
This definition is referenced by:  muval  22485  muf  22493
  Copyright terms: Public domain W3C validator