This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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$

Step	Hyp	Ref	Expression
1		breq1	$⊢ y = \frac{x}{2} \to (y < x \leftrightarrow \frac{x}{2} < x)$
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$