Theorem 1arith

Description: Fundamental theorem of arithmetic, where a prime factorization is represented as a sequence of prime exponents, for which only finitely many primes have nonzero exponent. The function M maps the set of positive integers one-to-one onto the set of prime factorizations R . (Contributed by Paul Chapman, 17-Nov-2012) (Proof shortened by Mario Carneiro, 30-May-2014)

	Ref	Expression
Hypotheses	1arith.1	$$⊢M=\left(n\in \mathbb{N}⟼\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\right)$$
	1arith.2	$$⊢R=\left\{e\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
Assertion	1arith	$$⊢M:\mathbb{N}\underset{1-1\; onto}{⟶}R$$

Proof

Step	Hyp	Ref	Expression
1		1arith.1	$$⊢M=\left(n\in \mathbb{N}⟼\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\right)$$
2		1arith.2	$$⊢R=\left\{e\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		prmex	$$⊢\mathbb{P}\in \mathrm{V}$$
4	3	mptex	$$⊢\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\in \mathrm{V}$$
5	4 1	fnmpti	$$⊢MFn\mathbb{N}$$
6	1	1arithlem3	$$⊢x\in \mathbb{N}\to M\left(x\right):\mathbb{P}⟶{\mathbb{N}}_0$$
7		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
8	7 3	elmap	$$⊢M\left(x\right)\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)\leftrightarrow M\left(x\right):\mathbb{P}⟶{\mathbb{N}}_0$$
9	6 8	sylibr	$$⊢x\in \mathbb{N}\to M\left(x\right)\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)$$
10		fzfi	$$⊢\left(1\dots x\right)\in \mathrm{Fin}$$
11		ffn	$$⊢M\left(x\right):\mathbb{P}⟶{\mathbb{N}}_0\to M\left(x\right)Fn\mathbb{P}$$
12		elpreima	$$⊢M\left(x\right)Fn\mathbb{P}\to \left(q\in {M\left(x\right)}^{-1}\left[\mathbb{N}\right]\leftrightarrow \left(q\in \mathbb{P}\wedge M\left(x\right)\left(q\right)\in \mathbb{N}\right)\right)$$
13	6 11 12	3syl	$$⊢x\in \mathbb{N}\to \left(q\in {M\left(x\right)}^{-1}\left[\mathbb{N}\right]\leftrightarrow \left(q\in \mathbb{P}\wedge M\left(x\right)\left(q\right)\in \mathbb{N}\right)\right)$$
14	1	1arithlem2	$$⊢\left(x\in \mathbb{N}\wedge q\in \mathbb{P}\right)\to M\left(x\right)\left(q\right)=q\mathrm{pCnt}x$$
15	14	eleq1d	$$⊢\left(x\in \mathbb{N}\wedge q\in \mathbb{P}\right)\to \left(M\left(x\right)\left(q\right)\in \mathbb{N}\leftrightarrow q\mathrm{pCnt}x\in \mathbb{N}\right)$$
16		prmz	$$⊢q\in \mathbb{P}\to q\in \mathbb{Z}$$
17		id	$$⊢x\in \mathbb{N}\to x\in \mathbb{N}$$
18		dvdsle	$$⊢\left(q\in \mathbb{Z}\wedge x\in \mathbb{N}\right)\to \left(q\parallel x\to q\le x\right)$$
19	16 17 18	syl2anr	$$⊢\left(x\in \mathbb{N}\wedge q\in \mathbb{P}\right)\to \left(q\parallel x\to q\le x\right)$$
20		pcelnn	$$⊢\left(q\in \mathbb{P}\wedge x\in \mathbb{N}\right)\to \left(q\mathrm{pCnt}x\in \mathbb{N}\leftrightarrow q\parallel x\right)$$
21	20	ancoms	$$⊢\left(x\in \mathbb{N}\wedge q\in \mathbb{P}\right)\to \left(q\mathrm{pCnt}x\in \mathbb{N}\leftrightarrow q\parallel x\right)$$
22		prmnn	$$⊢q\in \mathbb{P}\to q\in \mathbb{N}$$
23		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
24	22 23	eleqtrdi	$$⊢q\in \mathbb{P}\to q\in {\mathbb{Z}}_{\ge 1}$$
25		nnz	$$⊢x\in \mathbb{N}\to x\in \mathbb{Z}$$
26		elfz5	$$⊢\left(q\in {\mathbb{Z}}_{\ge 1}\wedge x\in \mathbb{Z}\right)\to \left(q\in \left(1\dots x\right)\leftrightarrow q\le x\right)$$
27	24 25 26	syl2anr	$$⊢\left(x\in \mathbb{N}\wedge q\in \mathbb{P}\right)\to \left(q\in \left(1\dots x\right)\leftrightarrow q\le x\right)$$
28	19 21 27	3imtr4d	$$⊢\left(x\in \mathbb{N}\wedge q\in \mathbb{P}\right)\to \left(q\mathrm{pCnt}x\in \mathbb{N}\to q\in \left(1\dots x\right)\right)$$
29	15 28	sylbid	$$⊢\left(x\in \mathbb{N}\wedge q\in \mathbb{P}\right)\to \left(M\left(x\right)\left(q\right)\in \mathbb{N}\to q\in \left(1\dots x\right)\right)$$
30	29	expimpd	$$⊢x\in \mathbb{N}\to \left(\left(q\in \mathbb{P}\wedge M\left(x\right)\left(q\right)\in \mathbb{N}\right)\to q\in \left(1\dots x\right)\right)$$
31	13 30	sylbid	$$⊢x\in \mathbb{N}\to \left(q\in {M\left(x\right)}^{-1}\left[\mathbb{N}\right]\to q\in \left(1\dots x\right)\right)$$
32	31	ssrdv	$$⊢x\in \mathbb{N}\to {M\left(x\right)}^{-1}\left[\mathbb{N}\right]\subseteq \left(1\dots x\right)$$
33		ssfi	$$⊢\left(\left(1\dots x\right)\in \mathrm{Fin}\wedge {M\left(x\right)}^{-1}\left[\mathbb{N}\right]\subseteq \left(1\dots x\right)\right)\to {M\left(x\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
34	10 32 33	sylancr	$$⊢x\in \mathbb{N}\to {M\left(x\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
35		cnveq	$$⊢e=M\left(x\right)\to e^{-1}={M\left(x\right)}^{-1}$$
36	35	imaeq1d	$$⊢e=M\left(x\right)\to e^{-1}\left[\mathbb{N}\right]={M\left(x\right)}^{-1}\left[\mathbb{N}\right]$$
37	36	eleq1d	$$⊢e=M\left(x\right)\to \left(e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow {M\left(x\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
38	37 2	elrab2	$$⊢M\left(x\right)\in R\leftrightarrow \left(M\left(x\right)\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)\wedge {M\left(x\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
39	9 34 38	sylanbrc	$$⊢x\in \mathbb{N}\to M\left(x\right)\in R$$
40	39	rgen	$$⊢\forall x\in \mathbb{N}M\left(x\right)\in R$$
41		ffnfv	$$⊢M:\mathbb{N}⟶R\leftrightarrow \left(MFn\mathbb{N}\wedge \forall x\in \mathbb{N}M\left(x\right)\in R\right)$$
42	5 40 41	mpbir2an	$$⊢M:\mathbb{N}⟶R$$
43	14	adantlr	$$⊢\left(\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\wedge q\in \mathbb{P}\right)\to M\left(x\right)\left(q\right)=q\mathrm{pCnt}x$$
44	1	1arithlem2	$$⊢\left(y\in \mathbb{N}\wedge q\in \mathbb{P}\right)\to M\left(y\right)\left(q\right)=q\mathrm{pCnt}y$$
45	44	adantll	$$⊢\left(\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\wedge q\in \mathbb{P}\right)\to M\left(y\right)\left(q\right)=q\mathrm{pCnt}y$$
46	43 45	eqeq12d	$$⊢\left(\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\wedge q\in \mathbb{P}\right)\to \left(M\left(x\right)\left(q\right)=M\left(y\right)\left(q\right)\leftrightarrow q\mathrm{pCnt}x=q\mathrm{pCnt}y\right)$$
47	46	ralbidva	$$⊢\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\to \left(\forall q\in \mathbb{P}M\left(x\right)\left(q\right)=M\left(y\right)\left(q\right)\leftrightarrow \forall q\in \mathbb{P}q\mathrm{pCnt}x=q\mathrm{pCnt}y\right)$$
48	1	1arithlem3	$$⊢y\in \mathbb{N}\to M\left(y\right):\mathbb{P}⟶{\mathbb{N}}_0$$
49		ffn	$$⊢M\left(y\right):\mathbb{P}⟶{\mathbb{N}}_0\to M\left(y\right)Fn\mathbb{P}$$
50		eqfnfv	$$⊢\left(M\left(x\right)Fn\mathbb{P}\wedge M\left(y\right)Fn\mathbb{P}\right)\to \left(M\left(x\right)=M\left(y\right)\leftrightarrow \forall q\in \mathbb{P}M\left(x\right)\left(q\right)=M\left(y\right)\left(q\right)\right)$$
51	11 49 50	syl2an	$$⊢\left(M\left(x\right):\mathbb{P}⟶{\mathbb{N}}_0\wedge M\left(y\right):\mathbb{P}⟶{\mathbb{N}}_0\right)\to \left(M\left(x\right)=M\left(y\right)\leftrightarrow \forall q\in \mathbb{P}M\left(x\right)\left(q\right)=M\left(y\right)\left(q\right)\right)$$
52	6 48 51	syl2an	$$⊢\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\to \left(M\left(x\right)=M\left(y\right)\leftrightarrow \forall q\in \mathbb{P}M\left(x\right)\left(q\right)=M\left(y\right)\left(q\right)\right)$$
53		nnnn0	$$⊢x\in \mathbb{N}\to x\in {\mathbb{N}}_0$$
54		nnnn0	$$⊢y\in \mathbb{N}\to y\in {\mathbb{N}}_0$$
55		pc11	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to \left(x=y\leftrightarrow \forall q\in \mathbb{P}q\mathrm{pCnt}x=q\mathrm{pCnt}y\right)$$
56	53 54 55	syl2an	$$⊢\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\to \left(x=y\leftrightarrow \forall q\in \mathbb{P}q\mathrm{pCnt}x=q\mathrm{pCnt}y\right)$$
57	47 52 56	3bitr4d	$$⊢\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\to \left(M\left(x\right)=M\left(y\right)\leftrightarrow x=y\right)$$
58	57	biimpd	$$⊢\left(x\in \mathbb{N}\wedge y\in \mathbb{N}\right)\to \left(M\left(x\right)=M\left(y\right)\to x=y\right)$$
59	58	rgen2	$$⊢\forall x\in \mathbb{N}\forall y\in \mathbb{N}\left(M\left(x\right)=M\left(y\right)\to x=y\right)$$
60		dff13	$$⊢M:\mathbb{N}\underset{1-1}{⟶}R\leftrightarrow \left(M:\mathbb{N}⟶R\wedge \forall x\in \mathbb{N}\forall y\in \mathbb{N}\left(M\left(x\right)=M\left(y\right)\to x=y\right)\right)$$
61	42 59 60	mpbir2an	$$⊢M:\mathbb{N}\underset{1-1}{⟶}R$$
62		eqid	$$⊢\left(g\in \mathbb{N}⟼if\left(g\in \mathbb{P},g^{f\left(g\right)},1\right)\right)=\left(g\in \mathbb{N}⟼if\left(g\in \mathbb{P},g^{f\left(g\right)},1\right)\right)$$
63		cnveq	$$⊢e=f\to e^{-1}=f^{-1}$$
64	63	imaeq1d	$$⊢e=f\to e^{-1}\left[\mathbb{N}\right]=f^{-1}\left[\mathbb{N}\right]$$
65	64	eleq1d	$$⊢e=f\to \left(e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\leftrightarrow f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
66	65 2	elrab2	$$⊢f\in R\leftrightarrow \left(f\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)\wedge f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
67	66	simplbi	$$⊢f\in R\to f\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)$$
68	7 3	elmap	$$⊢f\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)\leftrightarrow f:\mathbb{P}⟶{\mathbb{N}}_0$$
69	67 68	sylib	$$⊢f\in R\to f:\mathbb{P}⟶{\mathbb{N}}_0$$
70	69	ad2antrr	$$⊢\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\to f:\mathbb{P}⟶{\mathbb{N}}_0$$
71		simplr	$$⊢\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\to y\in ℝ$$
72		0re	$$⊢0\in ℝ$$
73		ifcl	$$⊢\left(y\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le y,y,0\right)\in ℝ$$
74	71 72 73	sylancl	$$⊢\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\to if\left(0\le y,y,0\right)\in ℝ$$
75		max1	$$⊢\left(0\in ℝ\wedge y\in ℝ\right)\to 0\le if\left(0\le y,y,0\right)$$
76	72 71 75	sylancr	$$⊢\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\to 0\le if\left(0\le y,y,0\right)$$
77		flge0nn0	$$⊢\left(if\left(0\le y,y,0\right)\in ℝ\wedge 0\le if\left(0\le y,y,0\right)\right)\to ⌊if\left(0\le y,y,0\right)⌋\in {\mathbb{N}}_0$$
78	74 76 77	syl2anc	$$⊢\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\to ⌊if\left(0\le y,y,0\right)⌋\in {\mathbb{N}}_0$$
79		nn0p1nn	$$⊢⌊if\left(0\le y,y,0\right)⌋\in {\mathbb{N}}_0\to ⌊if\left(0\le y,y,0\right)⌋+1\in \mathbb{N}$$
80	78 79	syl	$$⊢\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\to ⌊if\left(0\le y,y,0\right)⌋+1\in \mathbb{N}$$
81	71	adantr	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to y\in ℝ$$
82	80	adantr	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to ⌊if\left(0\le y,y,0\right)⌋+1\in \mathbb{N}$$
83	82	nnred	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to ⌊if\left(0\le y,y,0\right)⌋+1\in ℝ$$
84	16	ssriv	$$⊢\mathbb{P}\subseteq \mathbb{Z}$$
85		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
86	84 85	sstri	$$⊢\mathbb{P}\subseteq ℝ$$
87		simprl	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to q\in \mathbb{P}$$
88	86 87	sselid	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to q\in ℝ$$
89	74	adantr	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to if\left(0\le y,y,0\right)\in ℝ$$
90		max2	$$⊢\left(0\in ℝ\wedge y\in ℝ\right)\to y\le if\left(0\le y,y,0\right)$$
91	72 81 90	sylancr	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to y\le if\left(0\le y,y,0\right)$$
92		flltp1	$$⊢if\left(0\le y,y,0\right)\in ℝ\to if\left(0\le y,y,0\right)<⌊if\left(0\le y,y,0\right)⌋+1$$
93	89 92	syl	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to if\left(0\le y,y,0\right)<⌊if\left(0\le y,y,0\right)⌋+1$$
94	81 89 83 91 93	lelttrd	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to y<⌊if\left(0\le y,y,0\right)⌋+1$$
95		simprr	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to ⌊if\left(0\le y,y,0\right)⌋+1\le q$$
96	81 83 88 94 95	ltletrd	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to y<q$$
97	81 88	ltnled	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \left(y<q\leftrightarrow \neg q\le y\right)$$
98	96 97	mpbid	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \neg q\le y$$
99	87	biantrurd	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \left(f\left(q\right)\in \mathbb{N}\leftrightarrow \left(q\in \mathbb{P}\wedge f\left(q\right)\in \mathbb{N}\right)\right)$$
100	70	adantr	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to f:\mathbb{P}⟶{\mathbb{N}}_0$$
101		ffn	$$⊢f:\mathbb{P}⟶{\mathbb{N}}_0\to fFn\mathbb{P}$$
102		elpreima	$$⊢fFn\mathbb{P}\to \left(q\in f^{-1}\left[\mathbb{N}\right]\leftrightarrow \left(q\in \mathbb{P}\wedge f\left(q\right)\in \mathbb{N}\right)\right)$$
103	100 101 102	3syl	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \left(q\in f^{-1}\left[\mathbb{N}\right]\leftrightarrow \left(q\in \mathbb{P}\wedge f\left(q\right)\in \mathbb{N}\right)\right)$$
104	99 103	bitr4d	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \left(f\left(q\right)\in \mathbb{N}\leftrightarrow q\in f^{-1}\left[\mathbb{N}\right]\right)$$
105		simplr	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y$$
106		breq1	$$⊢k=q\to \left(k\le y\leftrightarrow q\le y\right)$$
107	106	rspccv	$$⊢\forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\to \left(q\in f^{-1}\left[\mathbb{N}\right]\to q\le y\right)$$
108	105 107	syl	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \left(q\in f^{-1}\left[\mathbb{N}\right]\to q\le y\right)$$
109	104 108	sylbid	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \left(f\left(q\right)\in \mathbb{N}\to q\le y\right)$$
110	98 109	mtod	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \neg f\left(q\right)\in \mathbb{N}$$
111	100 87	ffvelcdmd	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to f\left(q\right)\in {\mathbb{N}}_0$$
112		elnn0	$$⊢f\left(q\right)\in {\mathbb{N}}_0\leftrightarrow \left(f\left(q\right)\in \mathbb{N}\vee f\left(q\right)=0\right)$$
113	111 112	sylib	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \left(f\left(q\right)\in \mathbb{N}\vee f\left(q\right)=0\right)$$
114	113	ord	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to \left(\neg f\left(q\right)\in \mathbb{N}\to f\left(q\right)=0\right)$$
115	110 114	mpd	$$⊢\left(\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\wedge \left(q\in \mathbb{P}\wedge ⌊if\left(0\le y,y,0\right)⌋+1\le q\right)\right)\to f\left(q\right)=0$$
116	1 62 70 80 115	1arithlem4	$$⊢\left(\left(f\in R\wedge y\in ℝ\right)\wedge \forall k\in f^{-1}\left[\mathbb{N}\right]k\le y\right)\to \exists x\in \mathbb{N}f=M\left(x\right)$$
117		cnvimass	$$⊢f^{-1}\left[\mathbb{N}\right]\subseteq \mathrm{dom}f$$
118	69	fdmd	$$⊢f\in R\to \mathrm{dom}f=\mathbb{P}$$
119	118 86	eqsstrdi	$$⊢f\in R\to \mathrm{dom}f\subseteq ℝ$$
120	117 119	sstrid	$$⊢f\in R\to f^{-1}\left[\mathbb{N}\right]\subseteq ℝ$$
121	66	simprbi	$$⊢f\in R\to f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
122		fimaxre2	$$⊢\left(f^{-1}\left[\mathbb{N}\right]\subseteq ℝ\wedge f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)\to \exists y\in ℝ\forall k\in f^{-1}\left[\mathbb{N}\right]k\le y$$
123	120 121 122	syl2anc	$$⊢f\in R\to \exists y\in ℝ\forall k\in f^{-1}\left[\mathbb{N}\right]k\le y$$
124	116 123	r19.29a	$$⊢f\in R\to \exists x\in \mathbb{N}f=M\left(x\right)$$
125	124	rgen	$$⊢\forall f\in R\exists x\in \mathbb{N}f=M\left(x\right)$$
126		dffo3	$$⊢M:\mathbb{N}\underset{onto}{⟶}R\leftrightarrow \left(M:\mathbb{N}⟶R\wedge \forall f\in R\exists x\in \mathbb{N}f=M\left(x\right)\right)$$
127	42 125 126	mpbir2an	$$⊢M:\mathbb{N}\underset{onto}{⟶}R$$
128		df-f1o	$$⊢M:\mathbb{N}\underset{1-1\; onto}{⟶}R\leftrightarrow \left(M:\mathbb{N}\underset{1-1}{⟶}R\wedge M:\mathbb{N}\underset{onto}{⟶}R\right)$$
129	61 127 128	mpbir2an	$$⊢M:\mathbb{N}\underset{1-1\; onto}{⟶}R$$