Metamath Proof Explorer

Theorem muf

Description: The Möbius function is a function into the integers. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion muf 
|- mmu : NN --> ZZ

Proof

Step Hyp Ref Expression
1 df-mu 
 |-  mmu = ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )
2 0z 
 |-  0 e. ZZ
3 neg1z 
 |-  -u 1 e. ZZ
4 prmdvdsfi 
 |-  ( x e. NN -> { p e. Prime | p || x } e. Fin )
5 hashcl 
 |-  ( { p e. Prime | p || x } e. Fin -> ( # ` { p e. Prime | p || x } ) e. NN0 )
6 4 5 syl 
 |-  ( x e. NN -> ( # ` { p e. Prime | p || x } ) e. NN0 )
7 zexpcl 
 |-  ( ( -u 1 e. ZZ /\ ( # ` { p e. Prime | p || x } ) e. NN0 ) -> ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) e. ZZ )
8 3 6 7 sylancr 
 |-  ( x e. NN -> ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) e. ZZ )
9 ifcl 
 |-  ( ( 0 e. ZZ /\ ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) e. ZZ ) -> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) e. ZZ )
10 2 8 9 sylancr 
 |-  ( x e. NN -> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) e. ZZ )
11 1 10 fmpti 
 |-  mmu : NN --> ZZ