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

Proof

Step Hyp Ref Expression
1 simpll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A ∈ ℝ
2 simprl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → C ∈ ℝ
3 simplr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B ∈ ℝ
4 leadd1 ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ B ∈ ℝ → A ≤ C ↔ A + B ≤ C + B
5 1 2 3 4 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A ≤ C ↔ A + B ≤ C + B
6 simprr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → D ∈ ℝ
7 leadd2 ⊢ B ∈ ℝ ∧ D ∈ ℝ ∧ C ∈ ℝ → B ≤ D ↔ C + B ≤ C + D
8 3 6 2 7 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → B ≤ D ↔ C + B ≤ C + D
9 5 8 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A ≤ C ∧ B ≤ D ↔ A + B ≤ C + B ∧ C + B ≤ C + D
10 1 3 readdcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A + B ∈ ℝ
11 2 3 readdcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → C + B ∈ ℝ
12 2 6 readdcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → C + D ∈ ℝ
13 letr ⊢ A + B ∈ ℝ ∧ C + B ∈ ℝ ∧ C + D ∈ ℝ → A + B ≤ C + B ∧ C + B ≤ C + D → A + B ≤ C + D
14 10 11 12 13 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A + B ≤ C + B ∧ C + B ≤ C + D → A + B ≤ C + D
15 9 14 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → A ≤ C ∧ B ≤ D → A + B ≤ C + D