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	⊢ FermatNo : ℕ0 –1-1→ ℕ

Proof

Step	Hyp	Ref	Expression
1		df-fmtno	⊢ FermatNo = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
2		2nn	⊢ 2 ∈ ℕ
3	2	a1i	⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ )
4		2nn0	⊢ 2 ∈ ℕ0
5	4	a1i	⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ0 )
6		id	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 )
7	5 6	nn0expcld	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ 𝑛 ) ∈ ℕ0 )
8	3 7	nnexpcld	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑛 ) ) ∈ ℕ )
9	8	peano2nnd	⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) ∈ ℕ )
10	1 9	fmpti	⊢ FermatNo : ℕ0 ⟶ ℕ
11		fmtno	⊢ ( 𝑛 ∈ ℕ0 → ( FermatNo ‘ 𝑛 ) = ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
12		fmtno	⊢ ( 𝑚 ∈ ℕ0 → ( FermatNo ‘ 𝑚 ) = ( ( 2 ↑ ( 2 ↑ 𝑚 ) ) + 1 ) )
13	11 12	eqeqan12d	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) ↔ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑚 ) ) + 1 ) ) )
14	5 7	nn0expcld	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑛 ) ) ∈ ℕ0 )
15	14	nn0cnd	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑛 ) ) ∈ ℂ )
16	15	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 2 ↑ ( 2 ↑ 𝑛 ) ) ∈ ℂ )
17	4	a1i	⊢ ( 𝑚 ∈ ℕ0 → 2 ∈ ℕ0 )
18		id	⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℕ0 )
19	17 18	nn0expcld	⊢ ( 𝑚 ∈ ℕ0 → ( 2 ↑ 𝑚 ) ∈ ℕ0 )
20	17 19	nn0expcld	⊢ ( 𝑚 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑚 ) ) ∈ ℕ0 )
21	20	nn0cnd	⊢ ( 𝑚 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑚 ) ) ∈ ℂ )
22	21	adantl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 2 ↑ ( 2 ↑ 𝑚 ) ) ∈ ℂ )
23		1cnd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → 1 ∈ ℂ )
24	16 22 23	addcan2d	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑚 ) ) + 1 ) ↔ ( 2 ↑ ( 2 ↑ 𝑛 ) ) = ( 2 ↑ ( 2 ↑ 𝑚 ) ) ) )
25		2re	⊢ 2 ∈ ℝ
26	25	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → 2 ∈ ℝ )
27	7	nn0zd	⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ 𝑛 ) ∈ ℤ )
28	27	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℤ )
29	19	nn0zd	⊢ ( 𝑚 ∈ ℕ0 → ( 2 ↑ 𝑚 ) ∈ ℤ )
30	29	adantl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 2 ↑ 𝑚 ) ∈ ℤ )
31		1lt2	⊢ 1 < 2
32	31	a1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → 1 < 2 )
33		expcan	⊢ ( ( ( 2 ∈ ℝ ∧ ( 2 ↑ 𝑛 ) ∈ ℤ ∧ ( 2 ↑ 𝑚 ) ∈ ℤ ) ∧ 1 < 2 ) → ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) = ( 2 ↑ ( 2 ↑ 𝑚 ) ) ↔ ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) ) )
34	26 28 30 32 33	syl31anc	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) = ( 2 ↑ ( 2 ↑ 𝑚 ) ) ↔ ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) ) )
35	24 34	bitrd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑚 ) ) + 1 ) ↔ ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) ) )
36		nn0z	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
37	36	adantr	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → 𝑛 ∈ ℤ )
38		nn0z	⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℤ )
39	38	adantl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℤ )
40		expcan	⊢ ( ( ( 2 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ) ∧ 1 < 2 ) → ( ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) ↔ 𝑛 = 𝑚 ) )
41	40	biimpd	⊢ ( ( ( 2 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ) ∧ 1 < 2 ) → ( ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) → 𝑛 = 𝑚 ) )
42	26 37 39 32 41	syl31anc	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) → 𝑛 = 𝑚 ) )
43	35 42	sylbid	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑚 ) ) + 1 ) → 𝑛 = 𝑚 ) )
44	13 43	sylbid	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) → 𝑛 = 𝑚 ) )
45	44	rgen2	⊢ ∀ 𝑛 ∈ ℕ0 ∀ 𝑚 ∈ ℕ0 ( ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) → 𝑛 = 𝑚 )
46		dff13	⊢ ( FermatNo : ℕ0 –1-1→ ℕ ↔ ( FermatNo : ℕ0 ⟶ ℕ ∧ ∀ 𝑛 ∈ ℕ0 ∀ 𝑚 ∈ ℕ0 ( ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 𝑚 ) → 𝑛 = 𝑚 ) ) )
47	10 45 46	mpbir2an	⊢ FermatNo : ℕ0 –1-1→ ℕ