Theorem muval2

Description: The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014)

	Ref	Expression
Assertion	muval2	$$⊢\left(A\in \mathbb{N}\wedge \mu \left(A\right)\ne 0\right)\to \mu \left(A\right)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}$$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$$⊢\mu \left(A\right)\ne 0\leftrightarrow \neg \mu \left(A\right)=0$$
2		ifeqor	$$⊢\left(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)=0\vee 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)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)$$
3		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)$$
4	3	eqeq1d	$$⊢A\in \mathbb{N}\to \left(\mu \left(A\right)=0\leftrightarrow 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)=0\right)$$
5	3	eqeq1d	$$⊢A\in \mathbb{N}\to \left(\mu \left(A\right)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\leftrightarrow 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)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)$$
6	4 5	orbi12d	$$⊢A\in \mathbb{N}\to \left(\left(\mu \left(A\right)=0\vee \mu \left(A\right)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)\leftrightarrow \left(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)=0\vee 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)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)\right)$$
7	2 6	mpbiri	$$⊢A\in \mathbb{N}\to \left(\mu \left(A\right)=0\vee \mu \left(A\right)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)$$
8	7	ord	$$⊢A\in \mathbb{N}\to \left(\neg \mu \left(A\right)=0\to \mu \left(A\right)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)$$
9	1 8	syl5bi	$$⊢A\in \mathbb{N}\to \left(\mu \left(A\right)\ne 0\to \mu \left(A\right)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right)$$
10	9	imp	$$⊢\left(A\in \mathbb{N}\wedge \mu \left(A\right)\ne 0\right)\to \mu \left(A\right)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}$$