This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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