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

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