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

Metamath Proof Explorer

Theorem ltsub2

Description: Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 lesub2 
 |-  ( ( B e. RR /\ A e. RR /\ C e. RR ) -> ( B <_ A <-> ( C - A ) <_ ( C - B ) ) )
2 1 3com12 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B <_ A <-> ( C - A ) <_ ( C - B ) ) )
3 2 notbid 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. B <_ A <-> -. ( C - A ) <_ ( C - B ) ) )
4 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
5 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
6 4 5 ltnled 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> -. B <_ A ) )
7 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
8 7 5 resubcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C - B ) e. RR )
9 7 4 resubcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C - A ) e. RR )
10 8 9 ltnled 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C - B ) < ( C - A ) <-> -. ( C - A ) <_ ( C - B ) ) )
11 3 6 10 3bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( C - B ) < ( C - A ) ) )