Theorem rpltrp

Description: For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020)

	Ref	Expression
Assertion	rpltrp	$$⊢\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢y=\frac{x}{2}\to \left(y<x\leftrightarrow \frac{x}{2}<x\right)$$
2		rphalfcl	$$⊢x\in {ℝ}^{+}\to \frac{x}{2}\in {ℝ}^{+}$$
3		rphalflt	$$⊢x\in {ℝ}^{+}\to \frac{x}{2}<x$$
4	1 2 3	rspcedvdw	$$⊢x\in {ℝ}^{+}\to \exists y\in {ℝ}^{+}y<x$$
5	4	rgen	$$⊢\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x$$