# 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}=⌊\frac{1}{{E}}⌋+1$
Assertion recnnltrp ${⊢}{E}\in {ℝ}^{+}\to \left({N}\in ℕ\wedge \frac{1}{{N}}<{E}\right)$

### Proof

Step Hyp Ref Expression
1 recnnltrp.1 ${⊢}{N}=⌊\frac{1}{{E}}⌋+1$
2 rpreccl ${⊢}{E}\in {ℝ}^{+}\to \frac{1}{{E}}\in {ℝ}^{+}$
3 2 rpred ${⊢}{E}\in {ℝ}^{+}\to \frac{1}{{E}}\in ℝ$
4 2 rpge0d ${⊢}{E}\in {ℝ}^{+}\to 0\le \frac{1}{{E}}$
5 flge0nn0 ${⊢}\left(\frac{1}{{E}}\in ℝ\wedge 0\le \frac{1}{{E}}\right)\to ⌊\frac{1}{{E}}⌋\in {ℕ}_{0}$
6 3 4 5 syl2anc ${⊢}{E}\in {ℝ}^{+}\to ⌊\frac{1}{{E}}⌋\in {ℕ}_{0}$
7 nn0p1nn ${⊢}⌊\frac{1}{{E}}⌋\in {ℕ}_{0}\to ⌊\frac{1}{{E}}⌋+1\in ℕ$
8 6 7 syl ${⊢}{E}\in {ℝ}^{+}\to ⌊\frac{1}{{E}}⌋+1\in ℕ$
9 1 8 eqeltrid ${⊢}{E}\in {ℝ}^{+}\to {N}\in ℕ$
10 flltp1 ${⊢}\frac{1}{{E}}\in ℝ\to \frac{1}{{E}}<⌊\frac{1}{{E}}⌋+1$
11 3 10 syl ${⊢}{E}\in {ℝ}^{+}\to \frac{1}{{E}}<⌊\frac{1}{{E}}⌋+1$
12 11 1 breqtrrdi ${⊢}{E}\in {ℝ}^{+}\to \frac{1}{{E}}<{N}$
13 9 nnrpd ${⊢}{E}\in {ℝ}^{+}\to {N}\in {ℝ}^{+}$
14 2 13 ltrecd ${⊢}{E}\in {ℝ}^{+}\to \left(\frac{1}{{E}}<{N}↔\frac{1}{{N}}<\frac{1}{\frac{1}{{E}}}\right)$
15 12 14 mpbid ${⊢}{E}\in {ℝ}^{+}\to \frac{1}{{N}}<\frac{1}{\frac{1}{{E}}}$
16 rpcn ${⊢}{E}\in {ℝ}^{+}\to {E}\in ℂ$
17 rpne0 ${⊢}{E}\in {ℝ}^{+}\to {E}\ne 0$
18 16 17 recrecd ${⊢}{E}\in {ℝ}^{+}\to \frac{1}{\frac{1}{{E}}}={E}$
19 15 18 breqtrd ${⊢}{E}\in {ℝ}^{+}\to \frac{1}{{N}}<{E}$
20 9 19 jca ${⊢}{E}\in {ℝ}^{+}\to \left({N}\in ℕ\wedge \frac{1}{{N}}<{E}\right)$