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

Metamath Proof Explorer

Theorem alrple

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014)

		Ref	Expression
	Assertion	alrple	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + x)$

Proof

Step	Hyp	Ref	Expression
1		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
2		xralrple	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + x)$
3	1 2	sylan	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + x)$