| 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 ) |