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 | ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐷 ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltle | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐶 → 𝐴 ≤ 𝐶 ) ) | |
| 2 | 1 | ad2ant2r | ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 < 𝐶 → 𝐴 ≤ 𝐶 ) ) |
| 3 | leltadd | ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐵 < 𝐷 ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) ) | |
| 4 | 2 3 | syland | ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐷 ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) ) |