Theorem le2add

Description: Adding both sides of two 'less than or equal to' relations. (Contributed by NM, 17-Apr-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		simpll	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> A e. RR )
2		simprl	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> C e. RR )
3		simplr	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> B e. RR )
4		leadd1	|- ( ( A e. RR /\ C e. RR /\ B e. RR ) -> ( A <_ C <-> ( A + B ) <_ ( C + B ) ) )
5	1 2 3 4	syl3anc	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A <_ C <-> ( A + B ) <_ ( C + B ) ) )
6		simprr	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> D e. RR )
7		leadd2	|- ( ( B e. RR /\ D e. RR /\ C e. RR ) -> ( B <_ D <-> ( C + B ) <_ ( C + D ) ) )
8	3 6 2 7	syl3anc	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B <_ D <-> ( C + B ) <_ ( C + D ) ) )
9	5 8	anbi12d	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B <_ D ) <-> ( ( A + B ) <_ ( C + B ) /\ ( C + B ) <_ ( C + D ) ) ) )
10	1 3	readdcld	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A + B ) e. RR )
11	2 3	readdcld	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C + B ) e. RR )
12	2 6	readdcld	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( C + D ) e. RR )
13		letr	|- ( ( ( A + B ) e. RR /\ ( C + B ) e. RR /\ ( C + D ) e. RR ) -> ( ( ( A + B ) <_ ( C + B ) /\ ( C + B ) <_ ( C + D ) ) -> ( A + B ) <_ ( C + D ) ) )
14	10 11 12 13	syl3anc	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A + B ) <_ ( C + B ) /\ ( C + B ) <_ ( C + D ) ) -> ( A + B ) <_ ( C + D ) ) )
15	9 14	sylbid	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B <_ D ) -> ( A + B ) <_ ( C + D ) ) )