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

Metamath Proof Explorer

Definition df-mu

Description: Define the Möbius function, which is zero for non-squarefree numbers and is -u 1 or 1 for squarefree numbers according as to the number of prime divisors of the number is even or odd, see definition in ApostolNT p. 24. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion df-mu μ = ( 𝑥 ∈ ℕ ↦ if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmu ⊢ μ
1 vx ⊢ 𝑥
2 cn ⊢ ℕ
3 vp ⊢ 𝑝
4 cprime ⊢ ℙ
5 3 cv ⊢ 𝑝
6 cexp ⊢ ↑
7 c2 ⊢ 2
8 5 7 6 co ⊢ ( 𝑝 ↑ 2 )
9 cdvds ⊢ ∥
10 1 cv ⊢ 𝑥
11 8 10 9 wbr ⊢ ( 𝑝 ↑ 2 ) ∥ 𝑥
12 11 3 4 wrex ⊢ ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥
13 cc0 ⊢ 0
14 c1 ⊢ 1
15 14 cneg ⊢ - 1
16 chash ⊢ ♯
17 5 10 9 wbr ⊢ 𝑝 ∥ 𝑥
18 17 3 4 crab ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 }
19 18 16 cfv ⊢ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } )
20 15 19 6 co ⊢ ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) )
21 12 13 20 cif ⊢ if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) )
22 1 2 21 cmpt ⊢ ( 𝑥 ∈ ℕ ↦ if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ) )
23 0 22 wceq ⊢ μ = ( 𝑥 ∈ ℕ ↦ if ( ∃ 𝑝 ∈ ℙ ( 𝑝 ↑ 2 ) ∥ 𝑥 , 0 , ( - 1 ↑ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) ) ) )