Metamath Proof Explorer


Theorem recnnltrp

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 N=1E+1
Assertion recnnltrp E+N1N<E

Proof

Step Hyp Ref Expression
1 recnnltrp.1 N=1E+1
2 rpreccl E+1E+
3 2 rpred E+1E
4 2 rpge0d E+01E
5 flge0nn0 1E01E1E0
6 3 4 5 syl2anc E+1E0
7 nn0p1nn 1E01E+1
8 6 7 syl E+1E+1
9 1 8 eqeltrid E+N
10 flltp1 1E1E<1E+1
11 3 10 syl E+1E<1E+1
12 11 1 breqtrrdi E+1E<N
13 9 nnrpd E+N+
14 2 13 ltrecd E+1E<N1N<11E
15 12 14 mpbid E+1N<11E
16 rpcn E+E
17 rpne0 E+E0
18 16 17 recrecd E+11E=E
19 15 18 breqtrd E+1N<E
20 9 19 jca E+N1N<E