fmtnoge3

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

		Ref	Expression
	Assertion	fmtnoge3	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℤ_{\geq 3}$

Proof

Step	Hyp	Ref	Expression
1		fmtno	$⊢ N \in ℕ_{0} \to FermatNo (N) = 2^{2^{N}} + 1$
2		3z	$⊢ 3 \in ℤ$
3	2	a1i	$⊢ N \in ℕ_{0} \to 3 \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	5 7	nn0expcld	$⊢ N \in ℕ_{0} \to 2^{2^{N}} \in ℕ_{0}$
9		peano2nn0	$⊢ 2^{2^{N}} \in ℕ_{0} \to 2^{2^{N}} + 1 \in ℕ_{0}$
10	8 9	syl	$⊢ N \in ℕ_{0} \to 2^{2^{N}} + 1 \in ℕ_{0}$
11	10	nn0zd	$⊢ N \in ℕ_{0} \to 2^{2^{N}} + 1 \in ℤ$
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 ℕ_{0} \to 2 \in ℝ$
18		1le2	$⊢ 1 \leq 2$
19	18	a1i	$⊢ N \in ℕ_{0} \to 1 \leq 2$
20	17 6 19	expge1d	$⊢ N \in ℕ_{0} \to 1 \leq 2^{N}$
21		1zzd	$⊢ N \in ℕ_{0} \to 1 \in ℤ$
22	7	nn0zd	$⊢ N \in ℕ_{0} \to 2^{N} \in ℤ$
23		1lt2	$⊢ 1 < 2$
24	23	a1i	$⊢ N \in ℕ_{0} \to 1 < 2$
25	17 21 22 24	leexp2d	$⊢ N \in ℕ_{0} \to (1 \leq 2^{N} \leftrightarrow 2^{1} \leq 2^{2^{N}})$
26	20 25	mpbid	$⊢ N \in ℕ_{0} \to 2^{1} \leq 2^{2^{N}}$
27	15 26	eqbrtrrid	$⊢ N \in ℕ_{0} \to 2 \leq 2^{2^{N}}$
28	12 27	eqbrtrid	$⊢ N \in ℕ_{0} \to 3 - 1 \leq 2^{2^{N}}$
29		3re	$⊢ 3 \in ℝ$
30	29	a1i	$⊢ N \in ℕ_{0} \to 3 \in ℝ$
31		1red	$⊢ N \in ℕ_{0} \to 1 \in ℝ$
32	8	nn0red	$⊢ N \in ℕ_{0} \to 2^{2^{N}} \in ℝ$
33	30 31 32	lesubaddd	$⊢ N \in ℕ_{0} \to (3 - 1 \leq 2^{2^{N}} \leftrightarrow 3 \leq 2^{2^{N}} + 1)$
34	28 33	mpbid	$⊢ N \in ℕ_{0} \to 3 \leq 2^{2^{N}} + 1$
35		eluz2	$⊢ 2^{2^{N}} + 1 \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land 2^{2^{N}} + 1 \in ℤ \land 3 \leq 2^{2^{N}} + 1)$
36	3 11 34 35	syl3anbrc	$⊢ N \in ℕ_{0} \to 2^{2^{N}} + 1 \in ℤ_{\geq 3}$
37	1 36	eqeltrd	$⊢ N \in ℕ_{0} \to FermatNo (N) \in ℤ_{\geq 3}$

Metamath Proof Explorer

Theorem fmtnoge3

Proof