Theorem ltaddsub2

Description: 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004)

	Ref	Expression
Assertion	ltaddsub2	|- ( ( 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		ltaddsub	|- ( ( 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 ) ) )