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 \mathbb{N}\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 {\mathbb{N}}_0$$
6	3 4 5	syl2anc	$$⊢E\in {ℝ}^{+}\to ⌊\frac{1}{E}⌋\in {\mathbb{N}}_0$$
7		nn0p1nn	$$⊢⌊\frac{1}{E}⌋\in {\mathbb{N}}_0\to ⌊\frac{1}{E}⌋+1\in \mathbb{N}$$
8	6 7	syl	$$⊢E\in {ℝ}^{+}\to ⌊\frac{1}{E}⌋+1\in \mathbb{N}$$
9	1 8	eqeltrid	$$⊢E\in {ℝ}^{+}\to N\in \mathbb{N}$$
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\leftrightarrow \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 \mathbb{N}\wedge \frac{1}{N}<E\right)$$