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	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\leftrightarrow \forall x\in {ℝ}^{+}A\le B+x\right)$$

Proof

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