Theorem leaddsub2

Description: 'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005)

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

Proof

Step	Hyp	Ref	Expression
1		recn	|- ( A e. RR -> A e. CC )
2		recn	|- ( B e. RR -> B e. CC )
3		addcom	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
4	1 2 3	syl2an	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) )
5	4	3adant3	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + B ) = ( B + A ) )
6	5	breq1d	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) <_ C <-> ( B + A ) <_ C ) )
7		leaddsub	|- ( ( B e. RR /\ A e. RR /\ C e. RR ) -> ( ( B + A ) <_ C <-> B <_ ( C - A ) ) )
8	7	3com12	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + A ) <_ C <-> B <_ ( C - A ) ) )
9	6 8	bitrd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) <_ C <-> B <_ ( C - A ) ) )