This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-mu

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, see definition in ApostolNT p. 24. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion df-mu 
|- mmu = ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmu 
 |-  mmu
1 vx 
 |-  x
2 cn 
 |-  NN
3 vp 
 |-  p
4 cprime 
 |-  Prime
5 3 cv 
 |-  p
6 cexp 
 |-  ^
7 c2 
 |-  2
8 5 7 6 co 
 |-  ( p ^ 2 )
9 cdvds 
 |-  ||
10 1 cv 
 |-  x
11 8 10 9 wbr 
 |-  ( p ^ 2 ) || x
12 11 3 4 wrex 
 |-  E. p e. Prime ( p ^ 2 ) || x
13 cc0 
 |-  0
14 c1 
 |-  1
15 14 cneg 
 |-  -u 1
16 chash 
 |-  #
17 5 10 9 wbr 
 |-  p || x
18 17 3 4 crab 
 |-  { p e. Prime | p || x }
19 18 16 cfv 
 |-  ( # ` { p e. Prime | p || x } )
20 15 19 6 co 
 |-  ( -u 1 ^ ( # ` { p e. Prime | p || x } ) )
21 12 13 20 cif 
 |-  if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) )
22 1 2 21 cmpt 
 |-  ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )
23 0 22 wceq 
 |-  mmu = ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )