Theorem fmtnof1

Description: The enumeration of the Fermat numbers is a one-one function into the positive integers. (Contributed by AV, 3-Aug-2021)

	Ref	Expression
Assertion	fmtnof1	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		df-fmtno	$$⊢\mathrm{FermatNo}=\left(n\in {\mathbb{N}}_0⟼2^{2^n}+1\right)$$
2		2nn	$$⊢2\in \mathbb{N}$$
3	2	a1i	$$⊢n\in {\mathbb{N}}_0\to 2\in \mathbb{N}$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5	4	a1i	$$⊢n\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
6		id	$$⊢n\in {\mathbb{N}}_0\to n\in {\mathbb{N}}_0$$
7	5 6	nn0expcld	$$⊢n\in {\mathbb{N}}_0\to 2^n\in {\mathbb{N}}_0$$
8	3 7	nnexpcld	$$⊢n\in {\mathbb{N}}_0\to 2^{2^n}\in \mathbb{N}$$
9	8	peano2nnd	$$⊢n\in {\mathbb{N}}_0\to 2^{2^n}+1\in \mathbb{N}$$
10	1 9	fmpti	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0⟶\mathbb{N}$$
11		fmtno	$$⊢n\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(n\right)=2^{2^n}+1$$
12		fmtno	$$⊢m\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(m\right)=2^{2^m}+1$$
13	11 12	eqeqan12d	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(\mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(m\right)\leftrightarrow 2^{2^n}+1=2^{2^m}+1\right)$$
14	5 7	nn0expcld	$$⊢n\in {\mathbb{N}}_0\to 2^{2^n}\in {\mathbb{N}}_0$$
15	14	nn0cnd	$$⊢n\in {\mathbb{N}}_0\to 2^{2^n}\in ℂ$$
16	15	adantr	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to 2^{2^n}\in ℂ$$
17	4	a1i	$$⊢m\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
18		id	$$⊢m\in {\mathbb{N}}_0\to m\in {\mathbb{N}}_0$$
19	17 18	nn0expcld	$$⊢m\in {\mathbb{N}}_0\to 2^m\in {\mathbb{N}}_0$$
20	17 19	nn0expcld	$$⊢m\in {\mathbb{N}}_0\to 2^{2^m}\in {\mathbb{N}}_0$$
21	20	nn0cnd	$$⊢m\in {\mathbb{N}}_0\to 2^{2^m}\in ℂ$$
22	21	adantl	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to 2^{2^m}\in ℂ$$
23		1cnd	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to 1\in ℂ$$
24	16 22 23	addcan2d	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(2^{2^n}+1=2^{2^m}+1\leftrightarrow 2^{2^n}=2^{2^m}\right)$$
25		2re	$$⊢2\in ℝ$$
26	25	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to 2\in ℝ$$
27	7	nn0zd	$$⊢n\in {\mathbb{N}}_0\to 2^n\in \mathbb{Z}$$
28	27	adantr	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to 2^n\in \mathbb{Z}$$
29	19	nn0zd	$$⊢m\in {\mathbb{N}}_0\to 2^m\in \mathbb{Z}$$
30	29	adantl	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to 2^m\in \mathbb{Z}$$
31		1lt2	$$⊢1<2$$
32	31	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to 1<2$$
33		expcan	$$⊢\left(\left(2\in ℝ\wedge 2^n\in \mathbb{Z}\wedge 2^m\in \mathbb{Z}\right)\wedge 1<2\right)\to \left(2^{2^n}=2^{2^m}\leftrightarrow 2^n=2^m\right)$$
34	26 28 30 32 33	syl31anc	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(2^{2^n}=2^{2^m}\leftrightarrow 2^n=2^m\right)$$
35	24 34	bitrd	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(2^{2^n}+1=2^{2^m}+1\leftrightarrow 2^n=2^m\right)$$
36		nn0z	$$⊢n\in {\mathbb{N}}_0\to n\in \mathbb{Z}$$
37	36	adantr	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to n\in \mathbb{Z}$$
38		nn0z	$$⊢m\in {\mathbb{N}}_0\to m\in \mathbb{Z}$$
39	38	adantl	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to m\in \mathbb{Z}$$
40		expcan	$$⊢\left(\left(2\in ℝ\wedge n\in \mathbb{Z}\wedge m\in \mathbb{Z}\right)\wedge 1<2\right)\to \left(2^n=2^m\leftrightarrow n=m\right)$$
41	40	biimpd	$$⊢\left(\left(2\in ℝ\wedge n\in \mathbb{Z}\wedge m\in \mathbb{Z}\right)\wedge 1<2\right)\to \left(2^n=2^m\to n=m\right)$$
42	26 37 39 32 41	syl31anc	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(2^n=2^m\to n=m\right)$$
43	35 42	sylbid	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(2^{2^n}+1=2^{2^m}+1\to n=m\right)$$
44	13 43	sylbid	$$⊢\left(n\in {\mathbb{N}}_0\wedge m\in {\mathbb{N}}_0\right)\to \left(\mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(m\right)\to n=m\right)$$
45	44	rgen2	$$⊢\forall n\in {\mathbb{N}}_0\forall m\in {\mathbb{N}}_0\left(\mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(m\right)\to n=m\right)$$
46		dff13	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathbb{N}\leftrightarrow \left(\mathrm{FermatNo}:{\mathbb{N}}_0⟶\mathbb{N}\wedge \forall n\in {\mathbb{N}}_0\forall m\in {\mathbb{N}}_0\left(\mathrm{FermatNo}\left(n\right)=\mathrm{FermatNo}\left(m\right)\to n=m\right)\right)$$
47	10 45 46	mpbir2an	$$⊢\mathrm{FermatNo}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathbb{N}$$