Theorem fmtnoge3

Description: Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021)

	Ref	Expression
Assertion	fmtnoge3	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)\in {\mathbb{Z}}_{\ge 3}$$

Proof

Step	Hyp	Ref	Expression
1		fmtno	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)=2^{2^N}+1$$
2		3z	$$⊢3\in \mathbb{Z}$$
3	2	a1i	$$⊢N\in {\mathbb{N}}_0\to 3\in \mathbb{Z}$$
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	5 7	nn0expcld	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}\in {\mathbb{N}}_0$$
9		peano2nn0	$$⊢2^{2^N}\in {\mathbb{N}}_0\to 2^{2^N}+1\in {\mathbb{N}}_0$$
10	8 9	syl	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}+1\in {\mathbb{N}}_0$$
11	10	nn0zd	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}+1\in \mathbb{Z}$$
12		3m1e2	$$⊢3-1=2$$
13		2cn	$$⊢2\in ℂ$$
14		exp1	$$⊢2\in ℂ\to 2^1=2$$
15	13 14	ax-mp	$$⊢2^1=2$$
16		2re	$$⊢2\in ℝ$$
17	16	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in ℝ$$
18		1le2	$$⊢1\le 2$$
19	18	a1i	$$⊢N\in {\mathbb{N}}_0\to 1\le 2$$
20	17 6 19	expge1d	$$⊢N\in {\mathbb{N}}_0\to 1\le 2^N$$
21		1zzd	$$⊢N\in {\mathbb{N}}_0\to 1\in \mathbb{Z}$$
22	7	nn0zd	$$⊢N\in {\mathbb{N}}_0\to 2^N\in \mathbb{Z}$$
23		1lt2	$$⊢1<2$$
24	23	a1i	$$⊢N\in {\mathbb{N}}_0\to 1<2$$
25	17 21 22 24	leexp2d	$$⊢N\in {\mathbb{N}}_0\to \left(1\le 2^N\leftrightarrow 2^1\le 2^{2^N}\right)$$
26	20 25	mpbid	$$⊢N\in {\mathbb{N}}_0\to 2^1\le 2^{2^N}$$
27	15 26	eqbrtrrid	$$⊢N\in {\mathbb{N}}_0\to 2\le 2^{2^N}$$
28	12 27	eqbrtrid	$$⊢N\in {\mathbb{N}}_0\to 3-1\le 2^{2^N}$$
29		3re	$$⊢3\in ℝ$$
30	29	a1i	$$⊢N\in {\mathbb{N}}_0\to 3\in ℝ$$
31		1red	$$⊢N\in {\mathbb{N}}_0\to 1\in ℝ$$
32	8	nn0red	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}\in ℝ$$
33	30 31 32	lesubaddd	$$⊢N\in {\mathbb{N}}_0\to \left(3-1\le 2^{2^N}\leftrightarrow 3\le 2^{2^N}+1\right)$$
34	28 33	mpbid	$$⊢N\in {\mathbb{N}}_0\to 3\le 2^{2^N}+1$$
35		eluz2	$$⊢2^{2^N}+1\in {\mathbb{Z}}_{\ge 3}\leftrightarrow \left(3\in \mathbb{Z}\wedge 2^{2^N}+1\in \mathbb{Z}\wedge 3\le 2^{2^N}+1\right)$$
36	3 11 34 35	syl3anbrc	$$⊢N\in {\mathbb{N}}_0\to 2^{2^N}+1\in {\mathbb{Z}}_{\ge 3}$$
37	1 36	eqeltrd	$$⊢N\in {\mathbb{N}}_0\to \mathrm{FermatNo}\left(N\right)\in {\mathbb{Z}}_{\ge 3}$$