Theorem muval

Description: The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	muval	$$⊢A\in \mathbb{N}\to \mu \left(A\right)=if\left(\exists p\in \mathbb{P}{p}^2\parallel A,0,{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢x=A\to \left(p^2\parallel x\leftrightarrow p^2\parallel A\right)$$
2	1	rexbidv	$$⊢x=A\to \left(\exists p\in \mathbb{P}{p}^2\parallel x\leftrightarrow \exists p\in \mathbb{P}{p}^2\parallel A\right)$$
3		breq2	$$⊢x=A\to \left(p\parallel x\leftrightarrow p\parallel A\right)$$
4	3	rabbidv	$$⊢x=A\to \left\{p\in \mathbb{P}|p\parallel x\right\}=\left\{p\in \mathbb{P}|p\parallel A\right\}$$
5	4	fveq2d	$$⊢x=A\to \left|\left\{p\in \mathbb{P}|p\parallel x\right\}\right|=\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|$$
6	5	oveq2d	$$⊢x=A\to {\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel x\right\}\right|}={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}$$
7	2 6	ifbieq2d	$$⊢x=A\to 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)=if\left(\exists p\in \mathbb{P}{p}^2\parallel A,0,{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)$$
8		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)$$
9		c0ex	$$⊢0\in \mathrm{V}$$
10		ovex	$$⊢{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\in \mathrm{V}$$
11	9 10	ifex	$$⊢if\left(\exists p\in \mathbb{P}{p}^2\parallel A,0,{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)\in \mathrm{V}$$
12	7 8 11	fvmpt	$$⊢A\in \mathbb{N}\to \mu \left(A\right)=if\left(\exists p\in \mathbb{P}{p}^2\parallel A,0,{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)$$