Metamath Proof Explorer


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