Metamath Proof Explorer
Description: A number is less than or equal to itself plus a nonnegative number.
(Contributed by Mario Carneiro, 27May2016)


Ref 
Expression 

Hypotheses 
leidd.1 
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) 


ltnegd.2 
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) 

Assertion 
addge01d 
⊢ ( 𝜑 → ( 0 ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐴 + 𝐵 ) ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

leidd.1 
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) 
2 

ltnegd.2 
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) 
3 

addge01 
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐴 + 𝐵 ) ) ) 
4 
1 2 3

syl2anc 
⊢ ( 𝜑 → ( 0 ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐴 + 𝐵 ) ) ) 