Theorem fmtnoge3

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

	Ref	Expression
Assertion	fmtnoge3	⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 3 ) )

Proof

Step	Hyp	Ref	Expression
1		fmtno	⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
2		3z	⊢ 3 ∈ ℤ
3	2	a1i	⊢ ( 𝑁 ∈ ℕ0 → 3 ∈ ℤ )
4		2nn0	⊢ 2 ∈ ℕ0
5	4	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℕ0 )
6		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
7	5 6	nn0expcld	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
8	5 7	nn0expcld	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℕ0 )
9		peano2nn0	⊢ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ℕ0 )
10	8 9	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ℕ0 )
11	10	nn0zd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ℤ )
12		3m1e2	⊢ ( 3 − 1 ) = 2
13		2cn	⊢ 2 ∈ ℂ
14		exp1	⊢ ( 2 ∈ ℂ → ( 2 ↑ 1 ) = 2 )
15	13 14	ax-mp	⊢ ( 2 ↑ 1 ) = 2
16		2re	⊢ 2 ∈ ℝ
17	16	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
18		1le2	⊢ 1 ≤ 2
19	18	a1i	⊢ ( 𝑁 ∈ ℕ0 → 1 ≤ 2 )
20	17 6 19	expge1d	⊢ ( 𝑁 ∈ ℕ0 → 1 ≤ ( 2 ↑ 𝑁 ) )
21		1zzd	⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℤ )
22	7	nn0zd	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℤ )
23		1lt2	⊢ 1 < 2
24	23	a1i	⊢ ( 𝑁 ∈ ℕ0 → 1 < 2 )
25	17 21 22 24	leexp2d	⊢ ( 𝑁 ∈ ℕ0 → ( 1 ≤ ( 2 ↑ 𝑁 ) ↔ ( 2 ↑ 1 ) ≤ ( 2 ↑ ( 2 ↑ 𝑁 ) ) ) )
26	20 25	mpbid	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 1 ) ≤ ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
27	15 26	eqbrtrrid	⊢ ( 𝑁 ∈ ℕ0 → 2 ≤ ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
28	12 27	eqbrtrid	⊢ ( 𝑁 ∈ ℕ0 → ( 3 − 1 ) ≤ ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
29		3re	⊢ 3 ∈ ℝ
30	29	a1i	⊢ ( 𝑁 ∈ ℕ0 → 3 ∈ ℝ )
31		1red	⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ )
32	8	nn0red	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℝ )
33	30 31 32	lesubaddd	⊢ ( 𝑁 ∈ ℕ0 → ( ( 3 − 1 ) ≤ ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↔ 3 ≤ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) )
34	28 33	mpbid	⊢ ( 𝑁 ∈ ℕ0 → 3 ≤ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
35		eluz2	⊢ ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ℤ ∧ 3 ≤ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) )
36	3 11 34 35	syl3anbrc	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ∈ ( ℤ≥ ‘ 3 ) )
37	1 36	eqeltrd	⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ( ℤ≥ ‘ 3 ) )