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

Metamath Proof Explorer

Theorem reltre

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

		Ref	Expression
	Assertion	reltre	$⊢ \forall x \in ℝ \exists y \in ℝ y < x$

Step	Hyp	Ref	Expression
1		breq1	$⊢ y = x - 1 \to (y < x \leftrightarrow x - 1 < x)$
2		peano2rem	$⊢ x \in ℝ \to x - 1 \in ℝ$
3		ltm1	$⊢ x \in ℝ \to x - 1 < 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$