Theorem posdif

Description: Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004)

	Ref	Expression
Assertion	posdif	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow 0<B-A\right)$$

Proof

Step	Hyp	Ref	Expression
1		resubcl	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to B-A\in ℝ$$
2	1	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B-A\in ℝ$$
3		simpl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\in ℝ$$
4		ltaddpos	$$⊢\left(B-A\in ℝ\wedge A\in ℝ\right)\to \left(0<B-A\leftrightarrow A<A+B-A\right)$$
5	2 3 4	syl2anc	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0<B-A\leftrightarrow A<A+B-A\right)$$
6		recn	$$⊢A\in ℝ\to A\in ℂ$$
7		recn	$$⊢B\in ℝ\to B\in ℂ$$
8		pncan3	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B-A=B$$
9	6 7 8	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+B-A=B$$
10	9	breq2d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<A+B-A\leftrightarrow A<B\right)$$
11	5 10	bitr2d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow 0<B-A\right)$$