Metamath Proof Explorer
Description: Addition of nonnegative and positive numbers is positive.
(Contributed by Mario Carneiro, 27May2016)


Ref 
Expression 

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


ltnegd.2 
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) 


addgegt0d.3 
⊢ ( 𝜑 → 0 ≤ 𝐴 ) 


addgegt0d.4 
⊢ ( 𝜑 → 0 < 𝐵 ) 

Assertion 
addgegt0d 
⊢ ( 𝜑 → 0 < ( 𝐴 + 𝐵 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

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

addgegt0d.3 
⊢ ( 𝜑 → 0 ≤ 𝐴 ) 
4 

addgegt0d.4 
⊢ ( 𝜑 → 0 < 𝐵 ) 
5 

addgegt0 
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 + 𝐵 ) ) 
6 
1 2 3 4 5

syl22anc 
⊢ ( 𝜑 → 0 < ( 𝐴 + 𝐵 ) ) 