Definition df-mu 27145

Description: Define the Möbius function, which is zero for non-squarefree numbers and is -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.)

Assertion

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

Distinct variable group:   𝑥,𝑝

Detailed syntax breakdown of Definition df-mu

Step	Hyp	Ref	Expression
1		cmu 27139	. 2 class μ
2		vx	. . 3 setvar 𝑥
3		cn 12267	. . 3 class ℕ
4		vp	. . . . . . . 8 setvar 𝑝
5	4	cv 1538	. . . . . . 7 class 𝑝
6		c2 12322	. . . . . . 7 class 2
7		cexp 14103	. . . . . . 7 class ↑
8	5, 6, 7	co 7432	. . . . . 6 class (𝑝↑2)
9	2	cv 1538	. . . . . 6 class 𝑥
10		cdvds 16291	. . . . . 6 class ∥
11	8, 9, 10	wbr 5142	. . . . 5 wff (𝑝↑2) ∥ 𝑥
12		cprime 16709	. . . . 5 class ℙ
13	11, 4, 12	wrex 3069	. . . 4 wff ∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥
14		cc0 11156	. . . 4 class 0
15		c1 11157	. . . . . 6 class 1
16	15	cneg 11494	. . . . 5 class -1
17	5, 9, 10	wbr 5142	. . . . . . 7 wff 𝑝 ∥ 𝑥
18	17, 4, 12	crab 3435	. . . . . 6 class {𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥}
19		chash 14370	. . . . . 6 class ♯
20	18, 19	cfv 6560	. . . . 5 class (♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥})
21	16, 20, 7	co 7432	. . . 4 class (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥}))
22	13, 14, 21	cif 4524	. . 3 class if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥})))
23	2, 3, 22	cmpt 5224	. 2 class (𝑥 ∈ ℕ ↦ if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥}))))
24	1, 23	wceq 1539	1 wff μ = (𝑥 ∈ ℕ ↦ if(∃𝑝 ∈ ℙ (𝑝↑2) ∥ 𝑥, 0, (-1↑(♯‘{𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥}))))

This definition is referenced by:  muval  27176  muf  27184