Metamath Proof Explorer
Description: Addition to both sides of 'less than or equal to'. (Contributed by Glauco Siliprandi, 5-Apr-2020)
|
|
Ref |
Expression |
|
Hypotheses |
leadd12dd.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
|
|
leadd12dd.b |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
|
|
leadd12dd.c |
⊢ ( 𝜑 → 𝐶 ∈ ℝ ) |
|
|
leadd12dd.d |
⊢ ( 𝜑 → 𝐷 ∈ ℝ ) |
|
|
leadd12dd.ac |
⊢ ( 𝜑 → 𝐴 ≤ 𝐶 ) |
|
|
leadd12dd.bd |
⊢ ( 𝜑 → 𝐵 ≤ 𝐷 ) |
|
Assertion |
leadd12dd |
⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
leadd12dd.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
2 |
|
leadd12dd.b |
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) |
3 |
|
leadd12dd.c |
⊢ ( 𝜑 → 𝐶 ∈ ℝ ) |
4 |
|
leadd12dd.d |
⊢ ( 𝜑 → 𝐷 ∈ ℝ ) |
5 |
|
leadd12dd.ac |
⊢ ( 𝜑 → 𝐴 ≤ 𝐶 ) |
6 |
|
leadd12dd.bd |
⊢ ( 𝜑 → 𝐵 ≤ 𝐷 ) |
7 |
1 2
|
readdcld |
⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ ) |
8 |
3 2
|
readdcld |
⊢ ( 𝜑 → ( 𝐶 + 𝐵 ) ∈ ℝ ) |
9 |
3 4
|
readdcld |
⊢ ( 𝜑 → ( 𝐶 + 𝐷 ) ∈ ℝ ) |
10 |
1 3 2 5
|
leadd1dd |
⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐵 ) ) |
11 |
2 4 3 6
|
leadd2dd |
⊢ ( 𝜑 → ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) |
12 |
7 8 9 10 11
|
letrd |
⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) |