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

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 ⊢ μ = ( 𝑥 ∈ ℕ ↦ if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ) )
2 0z ⊢ 0 ∈ ℤ
3 neg1z ⊢ - 1 ∈ ℤ
4 prmdvdsfi ⊢ ( 𝑥 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ∈ Fin )
5 hashcl ⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ∈ Fin → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ∈ ℕ0 )
6 4 5 syl ⊢ ( 𝑥 ∈ ℕ → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ∈ ℕ0 )
7 zexpcl ⊢ ( ( - 1 ∈ ℤ ∧ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ∈ ℕ0 ) → ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ∈ ℤ )
8 3 6 7 sylancr ⊢ ( 𝑥 ∈ ℕ → ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ∈ ℤ )
9 ifcl ⊢ ( ( 0 ∈ ℤ ∧ ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ∈ ℤ ) → if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ) ∈ ℤ )
10 2 8 9 sylancr ⊢ ( 𝑥 ∈ ℕ → if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ) ∈ ℤ )
11 1 10 fmpti ⊢ μ : ℕ ⟶ ℤ