Description: Adding both sides of two 'less than' relations. Theorem I.25 of Apostol p. 20. (Contributed by NM, 15-Aug-1999) (Proof shortened by Mario Carneiro, 27-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | lt2add | |- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ B < D ) -> ( A + B ) < ( C + D ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltle | |- ( ( A e. RR /\ C e. RR ) -> ( A < C -> A <_ C ) ) |
|
| 2 | 1 | ad2ant2r | |- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A < C -> A <_ C ) ) |
| 3 | leltadd | |- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( A + B ) < ( C + D ) ) ) |
|
| 4 | 2 3 | syland | |- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ B < D ) -> ( A + B ) < ( C + D ) ) ) |