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