Theorem sqff1o

Description: There is a bijection from the squarefree divisors of a number N to the powerset of the prime divisors of N . Among other things, this implies that a number has 2 ^ k squarefree divisors where k is the number of prime divisors, and a squarefree number has 2 ^ k divisors (because all divisors of a squarefree number are squarefree). The inverse function to F takes the product of all the primes in some subset of prime divisors of N . (Contributed by Mario Carneiro, 1-Jul-2015)

	Ref	Expression
Hypotheses	sqff1o.1	$$⊢S=\left\{x\in \mathbb{N}|\left(\mu \left(x\right)\ne 0\wedge x\parallel N\right)\right\}$$
	sqff1o.2	$$⊢F=\left(n\in S⟼\left\{p\in \mathbb{P}|p\parallel n\right\}\right)$$
	sqff1o.3	$$⊢G=\left(n\in \mathbb{N}⟼\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\right)$$
Assertion	sqff1o	$$⊢N\in \mathbb{N}\to F:S\underset{1-1\; onto}{⟶}𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}$$

Proof

Step	Hyp	Ref	Expression
1		sqff1o.1	$$⊢S=\left\{x\in \mathbb{N}|\left(\mu \left(x\right)\ne 0\wedge x\parallel N\right)\right\}$$
2		sqff1o.2	$$⊢F=\left(n\in S⟼\left\{p\in \mathbb{P}|p\parallel n\right\}\right)$$
3		sqff1o.3	$$⊢G=\left(n\in \mathbb{N}⟼\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\right)$$
4		fveq2	$$⊢x=n\to \mu \left(x\right)=\mu \left(n\right)$$
5	4	neeq1d	$$⊢x=n\to \left(\mu \left(x\right)\ne 0\leftrightarrow \mu \left(n\right)\ne 0\right)$$
6		breq1	$$⊢x=n\to \left(x\parallel N\leftrightarrow n\parallel N\right)$$
7	5 6	anbi12d	$$⊢x=n\to \left(\left(\mu \left(x\right)\ne 0\wedge x\parallel N\right)\leftrightarrow \left(\mu \left(n\right)\ne 0\wedge n\parallel N\right)\right)$$
8	7 1	elrab2	$$⊢n\in S\leftrightarrow \left(n\in \mathbb{N}\wedge \left(\mu \left(n\right)\ne 0\wedge n\parallel N\right)\right)$$
9	8	simprbi	$$⊢n\in S\to \left(\mu \left(n\right)\ne 0\wedge n\parallel N\right)$$
10	9	simprd	$$⊢n\in S\to n\parallel N$$
11	10	ad2antlr	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to n\parallel N$$
12		prmz	$$⊢p\in \mathbb{P}\to p\in \mathbb{Z}$$
13	12	adantl	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to p\in \mathbb{Z}$$
14		simplr	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to n\in S$$
15	14 8	sylib	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(n\in \mathbb{N}\wedge \left(\mu \left(n\right)\ne 0\wedge n\parallel N\right)\right)$$
16	15	simpld	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to n\in \mathbb{N}$$
17	16	nnzd	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to n\in \mathbb{Z}$$
18		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
19	18	ad2antrr	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to N\in \mathbb{Z}$$
20		dvdstr	$$⊢\left(p\in \mathbb{Z}\wedge n\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(\left(p\parallel n\wedge n\parallel N\right)\to p\parallel N\right)$$
21	13 17 19 20	syl3anc	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(\left(p\parallel n\wedge n\parallel N\right)\to p\parallel N\right)$$
22	11 21	mpan2d	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(p\parallel n\to p\parallel N\right)$$
23	22	ss2rabdv	$$⊢\left(N\in \mathbb{N}\wedge n\in S\right)\to \left\{p\in \mathbb{P}|p\parallel n\right\}\subseteq \left\{p\in \mathbb{P}|p\parallel N\right\}$$
24		prmex	$$⊢\mathbb{P}\in \mathrm{V}$$
25	24	rabex	$$⊢\left\{p\in \mathbb{P}|p\parallel n\right\}\in \mathrm{V}$$
26	25	elpw	$$⊢\left\{p\in \mathbb{P}|p\parallel n\right\}\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\leftrightarrow \left\{p\in \mathbb{P}|p\parallel n\right\}\subseteq \left\{p\in \mathbb{P}|p\parallel N\right\}$$
27	23 26	sylibr	$$⊢\left(N\in \mathbb{N}\wedge n\in S\right)\to \left\{p\in \mathbb{P}|p\parallel n\right\}\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}$$
28		cnveq	$$⊢y=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\to y^{-1}={\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}$$
29	28	imaeq1d	$$⊢y=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\to y^{-1}\left[\mathbb{N}\right]={\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]$$
30	29	eleq1d	$$⊢y=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\to \left(y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow {\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
31		1nn0	$$⊢1\in {\mathbb{N}}_0$$
32		0nn0	$$⊢0\in {\mathbb{N}}_0$$
33	31 32	ifcli	$$⊢if\left(k\in z,1,0\right)\in {\mathbb{N}}_0$$
34	33	rgenw	$$⊢\forall k\in \mathbb{P}if\left(k\in z,1,0\right)\in {\mathbb{N}}_0$$
35		eqid	$$⊢\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)$$
36	35	fmpt	$$⊢\forall k\in \mathbb{P}if\left(k\in z,1,0\right)\in {\mathbb{N}}_0\leftrightarrow \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right):\mathbb{P}⟶{\mathbb{N}}_0$$
37	34 36	mpbi	$$⊢\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right):\mathbb{P}⟶{\mathbb{N}}_0$$
38	37	a1i	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right):\mathbb{P}⟶{\mathbb{N}}_0$$
39		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
40	39 24	elmap	$$⊢\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)\leftrightarrow \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right):\mathbb{P}⟶{\mathbb{N}}_0$$
41	38 40	sylibr	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)$$
42		fzfi	$$⊢\left(1\dots N\right)\in \mathrm{Fin}$$
43		ffn	$$⊢\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right):\mathbb{P}⟶{\mathbb{N}}_0\to \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)Fn\mathbb{P}$$
44		elpreima	$$⊢\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)Fn\mathbb{P}\to \left(x\in {\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\leftrightarrow \left(x\in \mathbb{P}\wedge \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\left(x\right)\in \mathbb{N}\right)\right)$$
45	37 43 44	mp2b	$$⊢x\in {\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\leftrightarrow \left(x\in \mathbb{P}\wedge \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\left(x\right)\in \mathbb{N}\right)$$
46		elequ1	$$⊢k=x\to \left(k\in z\leftrightarrow x\in z\right)$$
47	46	ifbid	$$⊢k=x\to if\left(k\in z,1,0\right)=if\left(x\in z,1,0\right)$$
48	31 32	ifcli	$$⊢if\left(x\in z,1,0\right)\in {\mathbb{N}}_0$$
49	48	elexi	$$⊢if\left(x\in z,1,0\right)\in \mathrm{V}$$
50	47 35 49	fvmpt	$$⊢x\in \mathbb{P}\to \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\left(x\right)=if\left(x\in z,1,0\right)$$
51	50	eleq1d	$$⊢x\in \mathbb{P}\to \left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\left(x\right)\in \mathbb{N}\leftrightarrow if\left(x\in z,1,0\right)\in \mathbb{N}\right)$$
52	51	biimpa	$$⊢\left(x\in \mathbb{P}\wedge \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\left(x\right)\in \mathbb{N}\right)\to if\left(x\in z,1,0\right)\in \mathbb{N}$$
53	45 52	sylbi	$$⊢x\in {\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\to if\left(x\in z,1,0\right)\in \mathbb{N}$$
54		0nnn	$$⊢\neg 0\in \mathbb{N}$$
55		iffalse	$$⊢\neg x\in z\to if\left(x\in z,1,0\right)=0$$
56	55	eleq1d	$$⊢\neg x\in z\to \left(if\left(x\in z,1,0\right)\in \mathbb{N}\leftrightarrow 0\in \mathbb{N}\right)$$
57	54 56	mtbiri	$$⊢\neg x\in z\to \neg if\left(x\in z,1,0\right)\in \mathbb{N}$$
58	57	con4i	$$⊢if\left(x\in z,1,0\right)\in \mathbb{N}\to x\in z$$
59	53 58	syl	$$⊢x\in {\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\to x\in z$$
60	59	ssriv	$$⊢{\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\subseteq z$$
61		elpwi	$$⊢z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\to z\subseteq \left\{p\in \mathbb{P}|p\parallel N\right\}$$
62	61	adantl	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to z\subseteq \left\{p\in \mathbb{P}|p\parallel N\right\}$$
63		prmssnn	$$⊢\mathbb{P}\subseteq \mathbb{N}$$
64		rabss2	$$⊢\mathbb{P}\subseteq \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel N\right\}\subseteq \left\{p\in \mathbb{N}|p\parallel N\right\}$$
65	63 64	ax-mp	$$⊢\left\{p\in \mathbb{P}|p\parallel N\right\}\subseteq \left\{p\in \mathbb{N}|p\parallel N\right\}$$
66		dvdsssfz1	$$⊢N\in \mathbb{N}\to \left\{p\in \mathbb{N}|p\parallel N\right\}\subseteq \left(1\dots N\right)$$
67	66	adantr	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left\{p\in \mathbb{N}|p\parallel N\right\}\subseteq \left(1\dots N\right)$$
68	65 67	sstrid	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left\{p\in \mathbb{P}|p\parallel N\right\}\subseteq \left(1\dots N\right)$$
69	62 68	sstrd	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to z\subseteq \left(1\dots N\right)$$
70	60 69	sstrid	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to {\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\subseteq \left(1\dots N\right)$$
71		ssfi	$$⊢\left(\left(1\dots N\right)\in \mathrm{Fin}\wedge {\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\subseteq \left(1\dots N\right)\right)\to {\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
72	42 70 71	sylancr	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to {\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
73	30 41 72	elrabd	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\in \left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
74		eqid	$$⊢\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
75	3 74	1arith	$$⊢G:\mathbb{N}\underset{1-1\; onto}{⟶}\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
76		f1ocnv	$$⊢G:\mathbb{N}\underset{1-1\; onto}{⟶}\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to G^{-1}:\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\underset{1-1\; onto}{⟶}\mathbb{N}$$
77		f1of	$$⊢G^{-1}:\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\underset{1-1\; onto}{⟶}\mathbb{N}\to G^{-1}:\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶\mathbb{N}$$
78	75 76 77	mp2b	$$⊢G^{-1}:\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶\mathbb{N}$$
79	78	ffvelcdmi	$$⊢\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\in \left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in \mathbb{N}$$
80	73 79	syl	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in \mathbb{N}$$
81		f1ocnvfv2	$$⊢\left(G:\mathbb{N}\underset{1-1\; onto}{⟶}\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\in \left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to G\left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)$$
82	75 73 81	sylancr	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to G\left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)$$
83	3	1arithlem1	$$⊢G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in \mathbb{N}\to G\left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)$$
84	80 83	syl	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to G\left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)$$
85	82 84	eqtr3d	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)$$
86	85	fveq1d	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\left(q\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\left(q\right)$$
87		elequ1	$$⊢k=q\to \left(k\in z\leftrightarrow q\in z\right)$$
88	87	ifbid	$$⊢k=q\to if\left(k\in z,1,0\right)=if\left(q\in z,1,0\right)$$
89	31 32	ifcli	$$⊢if\left(q\in z,1,0\right)\in {\mathbb{N}}_0$$
90	89	elexi	$$⊢if\left(q\in z,1,0\right)\in \mathrm{V}$$
91	88 35 90	fvmpt	$$⊢q\in \mathbb{P}\to \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\left(q\right)=if\left(q\in z,1,0\right)$$
92	86 91	sylan9req	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to \left(p\in \mathbb{P}⟼p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\left(q\right)=if\left(q\in z,1,0\right)$$
93		oveq1	$$⊢p=q\to p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)=q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)$$
94		eqid	$$⊢\left(p\in \mathbb{P}⟼p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)$$
95		ovex	$$⊢q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in \mathrm{V}$$
96	93 94 95	fvmpt	$$⊢q\in \mathbb{P}\to \left(p\in \mathbb{P}⟼p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\left(q\right)=q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)$$
97	96	adantl	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to \left(p\in \mathbb{P}⟼p\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\left(q\right)=q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)$$
98	92 97	eqtr3d	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to if\left(q\in z,1,0\right)=q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)$$
99		breq1	$$⊢1=if\left(q\in z,1,0\right)\to \left(1\le 1\leftrightarrow if\left(q\in z,1,0\right)\le 1\right)$$
100		breq1	$$⊢0=if\left(q\in z,1,0\right)\to \left(0\le 1\leftrightarrow if\left(q\in z,1,0\right)\le 1\right)$$
101		1le1	$$⊢1\le 1$$
102		0le1	$$⊢0\le 1$$
103	99 100 101 102	keephyp	$$⊢if\left(q\in z,1,0\right)\le 1$$
104	98 103	eqbrtrrdi	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\le 1$$
105	104	ralrimiva	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \forall q\in \mathbb{P}q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\le 1$$
106		issqf	$$⊢G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in \mathbb{N}\to \left(\mu \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\ne 0\leftrightarrow \forall q\in \mathbb{P}q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\le 1\right)$$
107	80 106	syl	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left(\mu \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\ne 0\leftrightarrow \forall q\in \mathbb{P}q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\le 1\right)$$
108	105 107	mpbird	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \mu \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\ne 0$$
109		iftrue	$$⊢q\in z\to if\left(q\in z,1,0\right)=1$$
110	109	adantl	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to if\left(q\in z,1,0\right)=1$$
111	62	sselda	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to q\in \left\{p\in \mathbb{P}|p\parallel N\right\}$$
112		breq1	$$⊢p=q\to \left(p\parallel N\leftrightarrow q\parallel N\right)$$
113	112	elrab	$$⊢q\in \left\{p\in \mathbb{P}|p\parallel N\right\}\leftrightarrow \left(q\in \mathbb{P}\wedge q\parallel N\right)$$
114	111 113	sylib	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to \left(q\in \mathbb{P}\wedge q\parallel N\right)$$
115	114	simprd	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to q\parallel N$$
116	114	simpld	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to q\in \mathbb{P}$$
117		simpll	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to N\in \mathbb{N}$$
118		pcelnn	$$⊢\left(q\in \mathbb{P}\wedge N\in \mathbb{N}\right)\to \left(q\mathrm{pCnt}N\in \mathbb{N}\leftrightarrow q\parallel N\right)$$
119	116 117 118	syl2anc	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to \left(q\mathrm{pCnt}N\in \mathbb{N}\leftrightarrow q\parallel N\right)$$
120	115 119	mpbird	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to q\mathrm{pCnt}N\in \mathbb{N}$$
121	120	nnge1d	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to 1\le q\mathrm{pCnt}N$$
122	110 121	eqbrtrd	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in z\right)\to if\left(q\in z,1,0\right)\le q\mathrm{pCnt}N$$
123	122	ex	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left(q\in z\to if\left(q\in z,1,0\right)\le q\mathrm{pCnt}N\right)$$
124	123	adantr	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to \left(q\in z\to if\left(q\in z,1,0\right)\le q\mathrm{pCnt}N\right)$$
125		simpr	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to q\in \mathbb{P}$$
126	18	ad2antrr	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to N\in \mathbb{Z}$$
127		pcge0	$$⊢\left(q\in \mathbb{P}\wedge N\in \mathbb{Z}\right)\to 0\le q\mathrm{pCnt}N$$
128	125 126 127	syl2anc	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to 0\le q\mathrm{pCnt}N$$
129		iffalse	$$⊢\neg q\in z\to if\left(q\in z,1,0\right)=0$$
130	129	breq1d	$$⊢\neg q\in z\to \left(if\left(q\in z,1,0\right)\le q\mathrm{pCnt}N\leftrightarrow 0\le q\mathrm{pCnt}N\right)$$
131	128 130	syl5ibrcom	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to \left(\neg q\in z\to if\left(q\in z,1,0\right)\le q\mathrm{pCnt}N\right)$$
132	124 131	pm2.61d	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to if\left(q\in z,1,0\right)\le q\mathrm{pCnt}N$$
133	98 132	eqbrtrrd	$$⊢\left(\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\wedge q\in \mathbb{P}\right)\to q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\le q\mathrm{pCnt}N$$
134	133	ralrimiva	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \forall q\in \mathbb{P}q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\le q\mathrm{pCnt}N$$
135	80	nnzd	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in \mathbb{Z}$$
136	18	adantr	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to N\in \mathbb{Z}$$
137		pc2dvds	$$⊢\left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\parallel N\leftrightarrow \forall q\in \mathbb{P}q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\le q\mathrm{pCnt}N\right)$$
138	135 136 137	syl2anc	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\parallel N\leftrightarrow \forall q\in \mathbb{P}q\mathrm{pCnt}{G}^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\le q\mathrm{pCnt}N\right)$$
139	134 138	mpbird	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\parallel N$$
140	108 139	jca	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to \left(\mu \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\ne 0\wedge G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\parallel N\right)$$
141		fveq2	$$⊢x=G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\to \mu \left(x\right)=\mu \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)$$
142	141	neeq1d	$$⊢x=G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\to \left(\mu \left(x\right)\ne 0\leftrightarrow \mu \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\ne 0\right)$$
143		breq1	$$⊢x=G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\to \left(x\parallel N\leftrightarrow G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\parallel N\right)$$
144	142 143	anbi12d	$$⊢x=G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\to \left(\left(\mu \left(x\right)\ne 0\wedge x\parallel N\right)\leftrightarrow \left(\mu \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\ne 0\wedge G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\parallel N\right)\right)$$
145	144 1	elrab2	$$⊢G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in S\leftrightarrow \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in \mathbb{N}\wedge \left(\mu \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)\ne 0\wedge G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\parallel N\right)\right)$$
146	80 140 145	sylanbrc	$$⊢\left(N\in \mathbb{N}\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\to G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\in S$$
147		eqcom	$$⊢n=G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\leftrightarrow G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)=n$$
148	8	simplbi	$$⊢n\in S\to n\in \mathbb{N}$$
149	148	ad2antrl	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to n\in \mathbb{N}$$
150	24	mptex	$$⊢\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\in \mathrm{V}$$
151	3	fvmpt2	$$⊢\left(n\in \mathbb{N}\wedge \left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\in \mathrm{V}\right)\to G\left(n\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)$$
152	149 150 151	sylancl	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to G\left(n\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)$$
153	152	eqeq1d	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(G\left(n\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\leftrightarrow \left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)$$
154	75	a1i	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to G:\mathbb{N}\underset{1-1\; onto}{⟶}\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
155	73	adantrl	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\in \left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
156		f1ocnvfvb	$$⊢\left(G:\mathbb{N}\underset{1-1\; onto}{⟶}\left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge n\in \mathbb{N}\wedge \left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\in \left\{y\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(G\left(n\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\leftrightarrow G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)=n\right)$$
157	154 149 155 156	syl3anc	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(G\left(n\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\leftrightarrow G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)=n\right)$$
158	24	a1i	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \mathbb{P}\in \mathrm{V}$$
159		0cnd	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to 0\in ℂ$$
160		1cnd	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to 1\in ℂ$$
161		0ne1	$$⊢0\ne 1$$
162	161	a1i	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to 0\ne 1$$
163	158 159 160 162	pw2f1olem	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(\left(z\in 𝒫\mathbb{P}\wedge \left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\leftrightarrow \left(\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\in \left({\left\{0,1\right\}}^{\mathbb{P}}\right)\wedge z={\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)}^{-1}\left[\left\{1\right\}\right]\right)\right)$$
164		ssrab2	$$⊢\left\{p\in \mathbb{P}|p\parallel N\right\}\subseteq \mathbb{P}$$
165	164	sspwi	$$⊢𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\subseteq 𝒫\mathbb{P}$$
166		simprr	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}$$
167	165 166	sselid	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to z\in 𝒫\mathbb{P}$$
168	167	biantrurd	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\leftrightarrow \left(z\in 𝒫\mathbb{P}\wedge \left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\right)$$
169		id	$$⊢p\in \mathbb{P}\to p\in \mathbb{P}$$
170	148	adantl	$$⊢\left(N\in \mathbb{N}\wedge n\in S\right)\to n\in \mathbb{N}$$
171		pccl	$$⊢\left(p\in \mathbb{P}\wedge n\in \mathbb{N}\right)\to p\mathrm{pCnt}n\in {\mathbb{N}}_0$$
172	169 170 171	syl2anr	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to p\mathrm{pCnt}n\in {\mathbb{N}}_0$$
173		elnn0	$$⊢p\mathrm{pCnt}n\in {\mathbb{N}}_0\leftrightarrow \left(p\mathrm{pCnt}n\in \mathbb{N}\vee p\mathrm{pCnt}n=0\right)$$
174	172 173	sylib	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(p\mathrm{pCnt}n\in \mathbb{N}\vee p\mathrm{pCnt}n=0\right)$$
175	174	orcomd	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(p\mathrm{pCnt}n=0\vee p\mathrm{pCnt}n\in \mathbb{N}\right)$$
176	9	simpld	$$⊢n\in S\to \mu \left(n\right)\ne 0$$
177	176	adantl	$$⊢\left(N\in \mathbb{N}\wedge n\in S\right)\to \mu \left(n\right)\ne 0$$
178		issqf	$$⊢n\in \mathbb{N}\to \left(\mu \left(n\right)\ne 0\leftrightarrow \forall p\in \mathbb{P}p\mathrm{pCnt}n\le 1\right)$$
179	170 178	syl	$$⊢\left(N\in \mathbb{N}\wedge n\in S\right)\to \left(\mu \left(n\right)\ne 0\leftrightarrow \forall p\in \mathbb{P}p\mathrm{pCnt}n\le 1\right)$$
180	177 179	mpbid	$$⊢\left(N\in \mathbb{N}\wedge n\in S\right)\to \forall p\in \mathbb{P}p\mathrm{pCnt}n\le 1$$
181	180	r19.21bi	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to p\mathrm{pCnt}n\le 1$$
182		nnle1eq1	$$⊢p\mathrm{pCnt}n\in \mathbb{N}\to \left(p\mathrm{pCnt}n\le 1\leftrightarrow p\mathrm{pCnt}n=1\right)$$
183	181 182	syl5ibcom	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(p\mathrm{pCnt}n\in \mathbb{N}\to p\mathrm{pCnt}n=1\right)$$
184	183	orim2d	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(\left(p\mathrm{pCnt}n=0\vee p\mathrm{pCnt}n\in \mathbb{N}\right)\to \left(p\mathrm{pCnt}n=0\vee p\mathrm{pCnt}n=1\right)\right)$$
185	175 184	mpd	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(p\mathrm{pCnt}n=0\vee p\mathrm{pCnt}n=1\right)$$
186		ovex	$$⊢p\mathrm{pCnt}n\in \mathrm{V}$$
187	186	elpr	$$⊢p\mathrm{pCnt}n\in \left\{0,1\right\}\leftrightarrow \left(p\mathrm{pCnt}n=0\vee p\mathrm{pCnt}n=1\right)$$
188	185 187	sylibr	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to p\mathrm{pCnt}n\in \left\{0,1\right\}$$
189	188	fmpttd	$$⊢\left(N\in \mathbb{N}\wedge n\in S\right)\to \left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right):\mathbb{P}⟶\left\{0,1\right\}$$
190	189	adantrr	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right):\mathbb{P}⟶\left\{0,1\right\}$$
191		prex	$$⊢\left\{0,1\right\}\in \mathrm{V}$$
192	191 24	elmap	$$⊢\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\in \left({\left\{0,1\right\}}^{\mathbb{P}}\right)\leftrightarrow \left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right):\mathbb{P}⟶\left\{0,1\right\}$$
193	190 192	sylibr	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\in \left({\left\{0,1\right\}}^{\mathbb{P}}\right)$$
194	193	biantrurd	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(z={\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)}^{-1}\left[\left\{1\right\}\right]\leftrightarrow \left(\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\in \left({\left\{0,1\right\}}^{\mathbb{P}}\right)\wedge z={\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)}^{-1}\left[\left\{1\right\}\right]\right)\right)$$
195	163 168 194	3bitr4d	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\leftrightarrow z={\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)}^{-1}\left[\left\{1\right\}\right]\right)$$
196		eqid	$$⊢\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)$$
197	196	mptiniseg	$$⊢1\in {\mathbb{N}}_0\to {\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)}^{-1}\left[\left\{1\right\}\right]=\left\{p\in \mathbb{P}|p\mathrm{pCnt}n=1\right\}$$
198	31 197	ax-mp	$$⊢{\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)}^{-1}\left[\left\{1\right\}\right]=\left\{p\in \mathbb{P}|p\mathrm{pCnt}n=1\right\}$$
199		id	$$⊢p\mathrm{pCnt}n=1\to p\mathrm{pCnt}n=1$$
200		1nn	$$⊢1\in \mathbb{N}$$
201	199 200	eqeltrdi	$$⊢p\mathrm{pCnt}n=1\to p\mathrm{pCnt}n\in \mathbb{N}$$
202	201 183	impbid2	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(p\mathrm{pCnt}n=1\leftrightarrow p\mathrm{pCnt}n\in \mathbb{N}\right)$$
203		simpr	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to p\in \mathbb{P}$$
204		pcelnn	$$⊢\left(p\in \mathbb{P}\wedge n\in \mathbb{N}\right)\to \left(p\mathrm{pCnt}n\in \mathbb{N}\leftrightarrow p\parallel n\right)$$
205	203 16 204	syl2anc	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(p\mathrm{pCnt}n\in \mathbb{N}\leftrightarrow p\parallel n\right)$$
206	202 205	bitrd	$$⊢\left(\left(N\in \mathbb{N}\wedge n\in S\right)\wedge p\in \mathbb{P}\right)\to \left(p\mathrm{pCnt}n=1\leftrightarrow p\parallel n\right)$$
207	206	rabbidva	$$⊢\left(N\in \mathbb{N}\wedge n\in S\right)\to \left\{p\in \mathbb{P}|p\mathrm{pCnt}n=1\right\}=\left\{p\in \mathbb{P}|p\parallel n\right\}$$
208	207	adantrr	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left\{p\in \mathbb{P}|p\mathrm{pCnt}n=1\right\}=\left\{p\in \mathbb{P}|p\parallel n\right\}$$
209	198 208	eqtrid	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to {\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)}^{-1}\left[\left\{1\right\}\right]=\left\{p\in \mathbb{P}|p\parallel n\right\}$$
210	209	eqeq2d	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(z={\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)}^{-1}\left[\left\{1\right\}\right]\leftrightarrow z=\left\{p\in \mathbb{P}|p\parallel n\right\}\right)$$
211	195 210	bitrd	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)=\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\leftrightarrow z=\left\{p\in \mathbb{P}|p\parallel n\right\}\right)$$
212	153 157 211	3bitr3d	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)=n\leftrightarrow z=\left\{p\in \mathbb{P}|p\parallel n\right\}\right)$$
213	147 212	bitrid	$$⊢\left(N\in \mathbb{N}\wedge \left(n\in S\wedge z\in 𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}\right)\right)\to \left(n=G^{-1}\left(\left(k\in \mathbb{P}⟼if\left(k\in z,1,0\right)\right)\right)\leftrightarrow z=\left\{p\in \mathbb{P}|p\parallel n\right\}\right)$$
214	2 27 146 213	f1o2d	$$⊢N\in \mathbb{N}\to F:S\underset{1-1\; onto}{⟶}𝒫\left\{p\in \mathbb{P}|p\parallel N\right\}$$