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