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