Theorem difrp

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

	Ref	Expression
Assertion	difrp	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) )

Proof

Step	Hyp	Ref	Expression
1		posdif	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B - A ) ) )
2		resubcl	|- ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
3	2	ancoms	|- ( ( A e. RR /\ B e. RR ) -> ( B - A ) e. RR )
4		elrp	|- ( ( B - A ) e. RR+ <-> ( ( B - A ) e. RR /\ 0 < ( B - A ) ) )
5	4	baib	|- ( ( B - A ) e. RR -> ( ( B - A ) e. RR+ <-> 0 < ( B - A ) ) )
6	3 5	syl	|- ( ( A e. RR /\ B e. RR ) -> ( ( B - A ) e. RR+ <-> 0 < ( B - A ) ) )
7	1 6	bitr4d	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) )