Metamath Proof Explorer

Theorem leltadd

Description: Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008)

Ref Expression
Assertion leltadd 
|- ( ( ( 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 ltleadd 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ ( D e. RR /\ C e. RR ) ) -> ( ( B < D /\ A <_ C ) -> ( B + A ) < ( D + C ) ) )
2 1 ancomsd 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ ( D e. RR /\ C e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( B + A ) < ( D + C ) ) )
3 2 ancom2s 
 |-  ( ( ( B e. RR /\ A e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( B + A ) < ( D + C ) ) )
4 3 ancom1s 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( B + A ) < ( D + C ) ) )
5 recn 
 |-  ( A e. RR -> A e. CC )
6 recn 
 |-  ( B e. RR -> B e. CC )
7 addcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
8 5 6 7 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) )
9 recn 
 |-  ( C e. RR -> C e. CC )
10 recn 
 |-  ( D e. RR -> D e. CC )
11 addcom 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C + D ) = ( D + C ) )
12 9 10 11 syl2an 
 |-  ( ( C e. RR /\ D e. RR ) -> ( C + D ) = ( D + C ) )
13 8 12 breqan12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A + B ) < ( C + D ) <-> ( B + A ) < ( D + C ) ) )
14 4 13 sylibrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( A + B ) < ( C + D ) ) )