Theorem isnsqf

Description: Two ways to say that a number is not squarefree. (Contributed by Mario Carneiro, 3-Oct-2014)

	Ref	Expression
Assertion	isnsqf	$$⊢A\in \mathbb{N}\to \left(\mu \left(A\right)=0\leftrightarrow \exists p\in \mathbb{P}{p}^2\parallel A\right)$$

Proof

Step	Hyp	Ref	Expression
1		neg1cn	$$⊢-1\in ℂ$$
2		neg1ne0	$$⊢-1\ne 0$$
3		prmdvdsfi	$$⊢A\in \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{Fin}$$
4		hashcl	$$⊢\left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{Fin}\to \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|\in {\mathbb{N}}_0$$
5	3 4	syl	$$⊢A\in \mathbb{N}\to \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|\in {\mathbb{N}}_0$$
6	5	nn0zd	$$⊢A\in \mathbb{N}\to \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|\in \mathbb{Z}$$
7		expne0i	$$⊢\left(-1\in ℂ\wedge -1\ne 0\wedge \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|\in \mathbb{Z}\right)\to {\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\ne 0$$
8	1 2 6 7	mp3an12i	$$⊢A\in \mathbb{N}\to {\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\ne 0$$
9		iffalse	$$⊢\neg \exists p\in \mathbb{P}{p}^2\parallel A\to 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|}$$
10	9	neeq1d	$$⊢\neg \exists p\in \mathbb{P}{p}^2\parallel A\to \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)\ne 0\leftrightarrow {\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\ne 0\right)$$
11	8 10	syl5ibrcom	$$⊢A\in \mathbb{N}\to \left(\neg \exists p\in \mathbb{P}{p}^2\parallel A\to 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)\ne 0\right)$$
12		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)$$
13	12	neeq1d	$$⊢A\in \mathbb{N}\to \left(\mu \left(A\right)\ne 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)\ne 0\right)$$
14	11 13	sylibrd	$$⊢A\in \mathbb{N}\to \left(\neg \exists p\in \mathbb{P}{p}^2\parallel A\to \mu \left(A\right)\ne 0\right)$$
15	14	necon4bd	$$⊢A\in \mathbb{N}\to \left(\mu \left(A\right)=0\to \exists p\in \mathbb{P}{p}^2\parallel A\right)$$
16		iftrue	$$⊢\exists p\in \mathbb{P}{p}^2\parallel A\to 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$$
17	12	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)$$
18	16 17	syl5ibr	$$⊢A\in \mathbb{N}\to \left(\exists p\in \mathbb{P}{p}^2\parallel A\to \mu \left(A\right)=0\right)$$
19	15 18	impbid	$$⊢A\in \mathbb{N}\to \left(\mu \left(A\right)=0\leftrightarrow \exists p\in \mathbb{P}{p}^2\parallel A\right)$$