Metamath Proof Explorer
Description: Adding both side of two inequalities. (Contributed by NM, 16-Sep-1999)
|
|
Ref |
Expression |
|
Hypotheses |
lt2.1 |
⊢ 𝐴 ∈ ℝ |
|
|
lt2.2 |
⊢ 𝐵 ∈ ℝ |
|
|
lt2.3 |
⊢ 𝐶 ∈ ℝ |
|
|
lt.4 |
⊢ 𝐷 ∈ ℝ |
|
Assertion |
le2addi |
⊢ ( ( 𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷 ) → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
lt2.1 |
⊢ 𝐴 ∈ ℝ |
2 |
|
lt2.2 |
⊢ 𝐵 ∈ ℝ |
3 |
|
lt2.3 |
⊢ 𝐶 ∈ ℝ |
4 |
|
lt.4 |
⊢ 𝐷 ∈ ℝ |
5 |
|
le2add |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷 ) → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) ) |
6 |
1 2 3 4 5
|
mp4an |
⊢ ( ( 𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷 ) → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) |