Metamath Proof Explorer


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 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝𝐴 } ) ) ) )