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 ⊢ A ∈ ℕ → μ ⁡ A = if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A

Proof

Step Hyp Ref Expression
1 breq2 ⊢ x = A → p 2 ∥ x ↔ p 2 ∥ A
2 1 rexbidv ⊢ x = A → ∃ p ∈ ℙ p 2 ∥ x ↔ ∃ p ∈ ℙ p 2 ∥ A
3 breq2 ⊢ x = A → p ∥ x ↔ p ∥ A
4 3 rabbidv ⊢ x = A → p ∈ ℙ | p ∥ x = p ∈ ℙ | p ∥ A
5 4 fveq2d ⊢ x = A → p ∈ ℙ | p ∥ x = p ∈ ℙ | p ∥ A
6 5 oveq2d ⊢ x = A → − 1 p ∈ ℙ | p ∥ x = − 1 p ∈ ℙ | p ∥ A
7 2 6 ifbieq2d ⊢ x = A → if ∃ p ∈ ℙ p 2 ∥ x 0 − 1 p ∈ ℙ | p ∥ x = if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A
8 df-mu ⊢ μ = x ∈ ℕ ⟼ if ∃ p ∈ ℙ p 2 ∥ x 0 − 1 p ∈ ℙ | p ∥ x
9 c0ex ⊢ 0 ∈ V
10 ovex ⊢ − 1 p ∈ ℙ | p ∥ A ∈ V
11 9 10 ifex ⊢ if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A ∈ V
12 7 8 11 fvmpt ⊢ A ∈ ℕ → μ ⁡ A = if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A