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