Description: N is a natural number large enough that its reciprocal is smaller than the given positive E . (Contributed by Glauco Siliprandi, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | recnnltrp.1 | |
|
Assertion | recnnltrp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recnnltrp.1 | |
|
2 | rpreccl | |
|
3 | 2 | rpred | |
4 | 2 | rpge0d | |
5 | flge0nn0 | |
|
6 | 3 4 5 | syl2anc | |
7 | nn0p1nn | |
|
8 | 6 7 | syl | |
9 | 1 8 | eqeltrid | |
10 | flltp1 | |
|
11 | 3 10 | syl | |
12 | 11 1 | breqtrrdi | |
13 | 9 | nnrpd | |
14 | 2 13 | ltrecd | |
15 | 12 14 | mpbid | |
16 | rpcn | |
|
17 | rpne0 | |
|
18 | 16 17 | recrecd | |
19 | 15 18 | breqtrd | |
20 | 9 19 | jca | |