Metamath Proof Explorer


Theorem suble

Description: Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005)

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

Proof

Step Hyp Ref Expression
1 lesubadd
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> A <_ ( C + B ) ) )
2 lesubadd2
 |-  ( ( A e. RR /\ C e. RR /\ B e. RR ) -> ( ( A - C ) <_ B <-> A <_ ( C + B ) ) )
3 2 3com23
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - C ) <_ B <-> A <_ ( C + B ) ) )
4 1 3 bitr4d
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> ( A - C ) <_ B ) )