Metamath Proof Explorer

Theorem tgoldbachgnn

Description: Lemma for tgoldbachgtd . (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Hypotheses tgoldbachgtda.o 
|- O = { z e. ZZ | -. 2 || z }
tgoldbachgtda.n 
|- ( ph -> N e. O )
tgoldbachgtda.0 
|- ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
Assertion tgoldbachgnn 
|- ( ph -> N e. NN )

Proof

Step Hyp Ref Expression
1 tgoldbachgtda.o 
 |-  O = { z e. ZZ | -. 2 || z }
2 tgoldbachgtda.n 
 |-  ( ph -> N e. O )
3 tgoldbachgtda.0 
 |-  ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
4 2 1 eleqtrdi 
 |-  ( ph -> N e. { z e. ZZ | -. 2 || z } )
5 elrabi 
 |-  ( N e. { z e. ZZ | -. 2 || z } -> N e. ZZ )
6 4 5 syl 
 |-  ( ph -> N e. ZZ )
7 1red 
 |-  ( ph -> 1 e. RR )
8 10nn0 
 |-  ; 1 0 e. NN0
9 8 nn0rei 
 |-  ; 1 0 e. RR
10 2nn0 
 |-  2 e. NN0
11 7nn0 
 |-  7 e. NN0
12 10 11 deccl 
 |-  ; 2 7 e. NN0
13 reexpcl 
 |-  ( ( ; 1 0 e. RR /\ ; 2 7 e. NN0 ) -> ( ; 1 0 ^ ; 2 7 ) e. RR )
14 9 12 13 mp2an 
 |-  ( ; 1 0 ^ ; 2 7 ) e. RR
15 14 a1i 
 |-  ( ph -> ( ; 1 0 ^ ; 2 7 ) e. RR )
16 6 zred 
 |-  ( ph -> N e. RR )
17 1re 
 |-  1 e. RR
18 1lt10 
 |-  1 < ; 1 0
19 17 9 18 ltleii 
 |-  1 <_ ; 1 0
20 expge1 
 |-  ( ( ; 1 0 e. RR /\ ; 2 7 e. NN0 /\ 1 <_ ; 1 0 ) -> 1 <_ ( ; 1 0 ^ ; 2 7 ) )
21 9 12 19 20 mp3an 
 |-  1 <_ ( ; 1 0 ^ ; 2 7 )
22 21 a1i 
 |-  ( ph -> 1 <_ ( ; 1 0 ^ ; 2 7 ) )
23 7 15 16 22 3 letrd 
 |-  ( ph -> 1 <_ N )
24 elnnz1 
 |-  ( N e. NN <-> ( N e. ZZ /\ 1 <_ N ) )
25 6 23 24 sylanbrc 
 |-  ( ph -> N e. NN )