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

Metamath Proof Explorer

Theorem muval2

Description: The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion muval2 ⊢ A ∈ ℕ ∧ μ ⁡ A ≠ 0 → μ ⁡ A = − 1 p ∈ ℙ | p ∥ A

Proof

Step Hyp Ref Expression
1 df-ne ⊢ μ ⁡ A ≠ 0 ↔ ¬ μ ⁡ A = 0
2 ifeqor ⊢ if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A = 0 ∨ if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A = − 1 p ∈ ℙ | p ∥ A
3 muval ⊢ A ∈ ℕ → μ ⁡ A = if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A
4 3 eqeq1d ⊢ A ∈ ℕ → μ ⁡ A = 0 ↔ if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A = 0
5 3 eqeq1d ⊢ A ∈ ℕ → μ ⁡ A = − 1 p ∈ ℙ | p ∥ A ↔ if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A = − 1 p ∈ ℙ | p ∥ A
6 4 5 orbi12d ⊢ A ∈ ℕ → μ ⁡ A = 0 ∨ μ ⁡ A = − 1 p ∈ ℙ | p ∥ A ↔ if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A = 0 ∨ if ∃ p ∈ ℙ p 2 ∥ A 0 − 1 p ∈ ℙ | p ∥ A = − 1 p ∈ ℙ | p ∥ A
7 2 6 mpbiri ⊢ A ∈ ℕ → μ ⁡ A = 0 ∨ μ ⁡ A = − 1 p ∈ ℙ | p ∥ A
8 7 ord ⊢ A ∈ ℕ → ¬ μ ⁡ A = 0 → μ ⁡ A = − 1 p ∈ ℙ | p ∥ A
9 1 8 biimtrid ⊢ A ∈ ℕ → μ ⁡ A ≠ 0 → μ ⁡ A = − 1 p ∈ ℙ | p ∥ A
10 9 imp ⊢ A ∈ ℕ ∧ μ ⁡ A ≠ 0 → μ ⁡ A = − 1 p ∈ ℙ | p ∥ A