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	$⊢ FermatNo : ℕ_{0} \underset{1-1}{⟶} ℕ$

Proof

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

Metamath Proof Explorer

Theorem fmtnof1

Proof