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