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

Metamath Proof Explorer

Theorem lt2add

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 ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A < C ∧ B < D → A + B < C + D

Proof

Step Hyp Ref Expression
1 ltle ⊢ A ∈ ℝ ∧ C ∈ ℝ → A < C → A ≤ C
2 1 ad2ant2r ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A < C → A ≤ C
3 leltadd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A ≤ C ∧ B < D → A + B < C + D
4 2 3 syland ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A < C ∧ B < D → A + B < C + D