Metamath Proof Explorer

Theorem fmtnoge3

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

Ref Expression
Assertion fmtnoge3 
|- ( N e. NN0 -> ( FermatNo ` N ) e. ( ZZ>= ` 3 ) )

Proof

Step Hyp Ref Expression
1 fmtno 
 |-  ( N e. NN0 -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
2 3z 
 |-  3 e. ZZ
3 2 a1i 
 |-  ( N e. NN0 -> 3 e. ZZ )
4 2nn0 
 |-  2 e. NN0
5 4 a1i 
 |-  ( N e. NN0 -> 2 e. NN0 )
6 id 
 |-  ( N e. NN0 -> N e. NN0 )
7 5 6 nn0expcld 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. NN0 )
8 5 7 nn0expcld 
 |-  ( N e. NN0 -> ( 2 ^ ( 2 ^ N ) ) e. NN0 )
9 peano2nn0 
 |-  ( ( 2 ^ ( 2 ^ N ) ) e. NN0 -> ( ( 2 ^ ( 2 ^ N ) ) + 1 ) e. NN0 )
10 8 9 syl 
 |-  ( N e. NN0 -> ( ( 2 ^ ( 2 ^ N ) ) + 1 ) e. NN0 )
11 10 nn0zd 
 |-  ( N e. NN0 -> ( ( 2 ^ ( 2 ^ N ) ) + 1 ) e. ZZ )
12 3m1e2 
 |-  ( 3 - 1 ) = 2
13 2cn 
 |-  2 e. CC
14 exp1 
 |-  ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
15 13 14 ax-mp 
 |-  ( 2 ^ 1 ) = 2
16 2re 
 |-  2 e. RR
17 16 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
18 1le2 
 |-  1 <_ 2
19 18 a1i 
 |-  ( N e. NN0 -> 1 <_ 2 )
20 17 6 19 expge1d 
 |-  ( N e. NN0 -> 1 <_ ( 2 ^ N ) )
21 1zzd 
 |-  ( N e. NN0 -> 1 e. ZZ )
22 7 nn0zd 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. ZZ )
23 1lt2 
 |-  1 < 2
24 23 a1i 
 |-  ( N e. NN0 -> 1 < 2 )
25 17 21 22 24 leexp2d 
 |-  ( N e. NN0 -> ( 1 <_ ( 2 ^ N ) <-> ( 2 ^ 1 ) <_ ( 2 ^ ( 2 ^ N ) ) ) )
26 20 25 mpbid 
 |-  ( N e. NN0 -> ( 2 ^ 1 ) <_ ( 2 ^ ( 2 ^ N ) ) )
27 15 26 eqbrtrrid 
 |-  ( N e. NN0 -> 2 <_ ( 2 ^ ( 2 ^ N ) ) )
28 12 27 eqbrtrid 
 |-  ( N e. NN0 -> ( 3 - 1 ) <_ ( 2 ^ ( 2 ^ N ) ) )
29 3re 
 |-  3 e. RR
30 29 a1i 
 |-  ( N e. NN0 -> 3 e. RR )
31 1red 
 |-  ( N e. NN0 -> 1 e. RR )
32 8 nn0red 
 |-  ( N e. NN0 -> ( 2 ^ ( 2 ^ N ) ) e. RR )
33 30 31 32 lesubaddd 
 |-  ( N e. NN0 -> ( ( 3 - 1 ) <_ ( 2 ^ ( 2 ^ N ) ) <-> 3 <_ ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) )
34 28 33 mpbid 
 |-  ( N e. NN0 -> 3 <_ ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
35 eluz2 
 |-  ( ( ( 2 ^ ( 2 ^ N ) ) + 1 ) e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ ( ( 2 ^ ( 2 ^ N ) ) + 1 ) e. ZZ /\ 3 <_ ( ( 2 ^ ( 2 ^ N ) ) + 1 ) ) )
36 3 11 34 35 syl3anbrc 
 |-  ( N e. NN0 -> ( ( 2 ^ ( 2 ^ N ) ) + 1 ) e. ( ZZ>= ` 3 ) )
37 1 36 eqeltrd 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. ( ZZ>= ` 3 ) )