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	$$⊢\mu =\left(x\in \mathbb{N}⟼if\left(\exists p\in \mathbb{P}{p}^2\parallel x,0,{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel x\right\}\right|}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmu	$$class\mu$$
1		vx	$$setvarx$$
2		cn	$$class\mathbb{N}$$
3		vp	$$setvarp$$
4		cprime	$$class\mathbb{P}$$
5	3	cv	$$setvarp$$
6		cexp	$$class^$$
7		c2	$$class2$$
8	5 7 6	co	$$class{p}^2$$
9		cdvds	$$class\parallel$$
10	1	cv	$$setvarx$$
11	8 10 9	wbr	$$wff{p}^2\parallel x$$
12	11 3 4	wrex	$$wff\exists p\in \mathbb{P}{p}^2\parallel x$$
13		cc0	$$class0$$
14		c1	$$class1$$
15	14	cneg	$$class-1$$
16		chash	$$class\left|.\right|$$
17	5 10 9	wbr	$$wffp\parallel x$$
18	17 3 4	crab	$$class\left\{p\in \mathbb{P}|p\parallel x\right\}$$
19	18 16	cfv	$$class\left|\left\{p\in \mathbb{P}|p\parallel x\right\}\right|$$
20	15 19 6	co	$$class{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel x\right\}\right|}$$
21	12 13 20	cif	$$classif\left(\exists p\in \mathbb{P}{p}^2\parallel x,0,{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel x\right\}\right|}\right)$$
22	1 2 21	cmpt	$$class\left(x\in \mathbb{N}⟼if\left(\exists p\in \mathbb{P}{p}^2\parallel x,0,{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel x\right\}\right|}\right)\right)$$
23	0 22	wceq	$$wff\mu =\left(x\in \mathbb{N}⟼if\left(\exists p\in \mathbb{P}{p}^2\parallel x,0,{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel x\right\}\right|}\right)\right)$$