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		rphalfcl	$$⊢x\in {ℝ}^{+}\to \frac{x}{2}\in {ℝ}^{+}$$
2		breq1	$$⊢y=\frac{x}{2}\to \left(y<x\leftrightarrow \frac{x}{2}<x\right)$$
3	2	adantl	$$⊢\left(x\in {ℝ}^{+}\wedge y=\frac{x}{2}\right)\to \left(y<x\leftrightarrow \frac{x}{2}<x\right)$$
4		rphalflt	$$⊢x\in {ℝ}^{+}\to \frac{x}{2}<x$$
5	1 3 4	rspcedvd	$$⊢x\in {ℝ}^{+}\to \exists y\in {ℝ}^{+}y<x$$
6	5	rgen	$$⊢\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x$$