Metamath Proof Explorer
Description: 'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 3-Aug-1999)
|
|
Ref |
Expression |
|
Hypotheses |
lt2.1 |
⊢ 𝐴 ∈ ℝ |
|
|
lt2.2 |
⊢ 𝐵 ∈ ℝ |
|
|
lt2.3 |
⊢ 𝐶 ∈ ℝ |
|
Assertion |
lesubadd2i |
⊢ ( ( 𝐴 − 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐵 + 𝐶 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
lt2.1 |
⊢ 𝐴 ∈ ℝ |
2 |
|
lt2.2 |
⊢ 𝐵 ∈ ℝ |
3 |
|
lt2.3 |
⊢ 𝐶 ∈ ℝ |
4 |
|
lesubadd2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 − 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐵 + 𝐶 ) ) ) |
5 |
1 2 3 4
|
mp3an |
⊢ ( ( 𝐴 − 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐵 + 𝐶 ) ) |