Theorem difrp

Description: Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014)

	Ref	Expression
Assertion	difrp	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow B-A\in {ℝ}^{+}\right)$$

Proof

Step	Hyp	Ref	Expression
1		posdif	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow 0<B-A\right)$$
2		resubcl	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to B-A\in ℝ$$
3	2	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B-A\in ℝ$$
4		elrp	$$⊢B-A\in {ℝ}^{+}\leftrightarrow \left(B-A\in ℝ\wedge 0<B-A\right)$$
5	4	baib	$$⊢B-A\in ℝ\to \left(B-A\in {ℝ}^{+}\leftrightarrow 0<B-A\right)$$
6	3 5	syl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B-A\in {ℝ}^{+}\leftrightarrow 0<B-A\right)$$
7	1 6	bitr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow B-A\in {ℝ}^{+}\right)$$