Theorem mule1

Description: The Möbius function takes on values in magnitude at most 1 . (Together with mucl , this implies that it takes a value in { -u 1 , 0 , 1 } for every positive integer.) (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	mule1	$$⊢A\in \mathbb{N}\to \left|\mu \left(A\right)\right|\le 1$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		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$$
3	1 2	sylan9eq	$$⊢\left(A\in \mathbb{N}\wedge \exists p\in \mathbb{P}{p}^2\parallel A\right)\to \mu \left(A\right)=0$$
4	3	fveq2d	$$⊢\left(A\in \mathbb{N}\wedge \exists p\in \mathbb{P}{p}^2\parallel A\right)\to \left|\mu \left(A\right)\right|=\left|0\right|$$
5		abs0	$$⊢\left|0\right|=0$$
6		0le1	$$⊢0\le 1$$
7	5 6	eqbrtri	$$⊢\left|0\right|\le 1$$
8	4 7	eqbrtrdi	$$⊢\left(A\in \mathbb{N}\wedge \exists p\in \mathbb{P}{p}^2\parallel A\right)\to \left|\mu \left(A\right)\right|\le 1$$
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	1 9	sylan9eq	$$⊢\left(A\in \mathbb{N}\wedge \neg \exists p\in \mathbb{P}{p}^2\parallel A\right)\to \mu \left(A\right)={\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}$$
11	10	fveq2d	$$⊢\left(A\in \mathbb{N}\wedge \neg \exists p\in \mathbb{P}{p}^2\parallel A\right)\to \left|\mu \left(A\right)\right|=\left|{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right|$$
12		neg1cn	$$⊢-1\in ℂ$$
13		prmdvdsfi	$$⊢A\in \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{Fin}$$
14		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$$
15	13 14	syl	$$⊢A\in \mathbb{N}\to \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|\in {\mathbb{N}}_0$$
16		absexp	$$⊢\left(-1\in ℂ\wedge \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|\in {\mathbb{N}}_0\right)\to \left|{\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|}$$
17	12 15 16	sylancr	$$⊢A\in \mathbb{N}\to \left|{\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|}$$
18		ax-1cn	$$⊢1\in ℂ$$
19	18	absnegi	$$⊢\left|-1\right|=\left|1\right|$$
20		abs1	$$⊢\left|1\right|=1$$
21	19 20	eqtri	$$⊢\left|-1\right|=1$$
22	21	oveq1i	$$⊢{\left|-1\right|}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}=1^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}$$
23	15	nn0zd	$$⊢A\in \mathbb{N}\to \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|\in \mathbb{Z}$$
24		1exp	$$⊢\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|\in \mathbb{Z}\to 1^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}=1$$
25	23 24	syl	$$⊢A\in \mathbb{N}\to 1^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}=1$$
26	22 25	eqtrid	$$⊢A\in \mathbb{N}\to {\left|-1\right|}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}=1$$
27	17 26	eqtrd	$$⊢A\in \mathbb{N}\to \left|{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right|=1$$
28	27	adantr	$$⊢\left(A\in \mathbb{N}\wedge \neg \exists p\in \mathbb{P}{p}^2\parallel A\right)\to \left|{\left(-1\right)}^{\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|}\right|=1$$
29	11 28	eqtrd	$$⊢\left(A\in \mathbb{N}\wedge \neg \exists p\in \mathbb{P}{p}^2\parallel A\right)\to \left|\mu \left(A\right)\right|=1$$
30		1le1	$$⊢1\le 1$$
31	29 30	eqbrtrdi	$$⊢\left(A\in \mathbb{N}\wedge \neg \exists p\in \mathbb{P}{p}^2\parallel A\right)\to \left|\mu \left(A\right)\right|\le 1$$
32	8 31	pm2.61dan	$$⊢A\in \mathbb{N}\to \left|\mu \left(A\right)\right|\le 1$$