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

Metamath Proof Explorer

Theorem posdif

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

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

Proof

Step Hyp Ref Expression
1 resubcl 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
2 1 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B - A ) e. RR )
3 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
4 ltaddpos 
 |-  ( ( ( B - A ) e. RR /\ A e. RR ) -> ( 0 < ( B - A ) <-> A < ( A + ( B - A ) ) ) )
5 2 3 4 syl2anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( B - A ) <-> A < ( A + ( B - A ) ) ) )
6 recn 
 |-  ( A e. RR -> A e. CC )
7 recn 
 |-  ( B e. RR -> B e. CC )
8 pncan3 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + ( B - A ) ) = B )
9 6 7 8 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + ( B - A ) ) = B )
10 9 breq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < ( A + ( B - A ) ) <-> A < B ) )
11 5 10 bitr2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B - A ) ) )