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 ⊢ μ : ℕ ⟶ ℤ

Proof

Step Hyp Ref Expression
1 df-mu ⊢ μ = x ∈ ℕ ⟼ if ∃ p ∈ ℙ p 2 ∥ x 0 − 1 p ∈ ℙ | p ∥ x
2 0z ⊢ 0 ∈ ℤ
3 neg1z ⊢ − 1 ∈ ℤ
4 prmdvdsfi ⊢ x ∈ ℕ → p ∈ ℙ | p ∥ x ∈ Fin
5 hashcl ⊢ p ∈ ℙ | p ∥ x ∈ Fin → p ∈ ℙ | p ∥ x ∈ ℕ 0
6 4 5 syl ⊢ x ∈ ℕ → p ∈ ℙ | p ∥ x ∈ ℕ 0
7 zexpcl ⊢ − 1 ∈ ℤ ∧ p ∈ ℙ | p ∥ x ∈ ℕ 0 → − 1 p ∈ ℙ | p ∥ x ∈ ℤ
8 3 6 7 sylancr ⊢ x ∈ ℕ → − 1 p ∈ ℙ | p ∥ x ∈ ℤ
9 ifcl ⊢ 0 ∈ ℤ ∧ − 1 p ∈ ℙ | p ∥ x ∈ ℤ → if ∃ p ∈ ℙ p 2 ∥ x 0 − 1 p ∈ ℙ | p ∥ x ∈ ℤ
10 2 8 9 sylancr ⊢ x ∈ ℕ → if ∃ p ∈ ℙ p 2 ∥ x 0 − 1 p ∈ ℙ | p ∥ x ∈ ℤ
11 1 10 fmpti ⊢ μ : ℕ ⟶ ℤ