Theorem rpgtrecnn

Description: Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Assertion	rpgtrecnn	$$⊢A\in {ℝ}^{+}\to \exists n\in \mathbb{N}\frac{1}{n}<A$$

Proof

Step	Hyp	Ref	Expression
1		rpreccl	$$⊢A\in {ℝ}^{+}\to \frac{1}{A}\in {ℝ}^{+}$$
2	1	rpred	$$⊢A\in {ℝ}^{+}\to \frac{1}{A}\in ℝ$$
3	1	rpge0d	$$⊢A\in {ℝ}^{+}\to 0\le \frac{1}{A}$$
4		flge0nn0	$$⊢\left(\frac{1}{A}\in ℝ\wedge 0\le \frac{1}{A}\right)\to ⌊\frac{1}{A}⌋\in {\mathbb{N}}_0$$
5	2 3 4	syl2anc	$$⊢A\in {ℝ}^{+}\to ⌊\frac{1}{A}⌋\in {\mathbb{N}}_0$$
6		nn0p1nn	$$⊢⌊\frac{1}{A}⌋\in {\mathbb{N}}_0\to ⌊\frac{1}{A}⌋+1\in \mathbb{N}$$
7	5 6	syl	$$⊢A\in {ℝ}^{+}\to ⌊\frac{1}{A}⌋+1\in \mathbb{N}$$
8		flltp1	$$⊢\frac{1}{A}\in ℝ\to \frac{1}{A}<⌊\frac{1}{A}⌋+1$$
9	2 8	syl	$$⊢A\in {ℝ}^{+}\to \frac{1}{A}<⌊\frac{1}{A}⌋+1$$
10	7	nnrpd	$$⊢A\in {ℝ}^{+}\to ⌊\frac{1}{A}⌋+1\in {ℝ}^{+}$$
11	1 10	ltrecd	$$⊢A\in {ℝ}^{+}\to \left(\frac{1}{A}<⌊\frac{1}{A}⌋+1\leftrightarrow \frac{1}{⌊\frac{1}{A}⌋+1}<\frac{1}{\frac{1}{A}}\right)$$
12	9 11	mpbid	$$⊢A\in {ℝ}^{+}\to \frac{1}{⌊\frac{1}{A}⌋+1}<\frac{1}{\frac{1}{A}}$$
13		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
14		rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$
15	13 14	recrecd	$$⊢A\in {ℝ}^{+}\to \frac{1}{\frac{1}{A}}=A$$
16	12 15	breqtrd	$$⊢A\in {ℝ}^{+}\to \frac{1}{⌊\frac{1}{A}⌋+1}<A$$
17		oveq2	$$⊢n=⌊\frac{1}{A}⌋+1\to \frac{1}{n}=\frac{1}{⌊\frac{1}{A}⌋+1}$$
18	17	breq1d	$$⊢n=⌊\frac{1}{A}⌋+1\to \left(\frac{1}{n}<A\leftrightarrow \frac{1}{⌊\frac{1}{A}⌋+1}<A\right)$$
19	18	rspcev	$$⊢\left(⌊\frac{1}{A}⌋+1\in \mathbb{N}\wedge \frac{1}{⌊\frac{1}{A}⌋+1}<A\right)\to \exists n\in \mathbb{N}\frac{1}{n}<A$$
20	7 16 19	syl2anc	$$⊢A\in {ℝ}^{+}\to \exists n\in \mathbb{N}\frac{1}{n}<A$$