Theorem muval

Description: The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	muval	⊢ ( 𝐴 ∈ ℕ → ( μ ‘ 𝐴 ) = if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑥 = 𝐴 → ( ( 𝑝 ↑ 2 ) ∥ 𝑥 ↔ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
2	1	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 ) )
3		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝐴 ) )
4	3	rabbidv	⊢ ( 𝑥 = 𝐴 → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
5	4	fveq2d	⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) = ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) )
6	5	oveq2d	⊢ ( 𝑥 = 𝐴 → ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) = ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) )
7	2 6	ifbieq2d	⊢ ( 𝑥 = 𝐴 → if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ) = if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) )
8		df-mu	⊢ μ = ( 𝑥 ∈ ℕ ↦ if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ) )
9		c0ex	⊢ 0 ∈ V
10		ovex	⊢ ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ∈ V
11	9 10	ifex	⊢ if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) ∈ V
12	7 8 11	fvmpt	⊢ ( 𝐴 ∈ ℕ → ( μ ‘ 𝐴 ) = if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝐴 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ) ) )