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

Metamath Proof Explorer

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+ ) )