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


Ref 
Expression 

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


rpgecld.2 
⊢ ( 𝜑 → 𝐵 ∈ ℝ^{+} ) 


divge0d.3 
⊢ ( 𝜑 → 0 ≤ 𝐴 ) 

Assertion 
divge0d 
⊢ ( 𝜑 → 0 ≤ ( 𝐴 / 𝐵 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

rpgecld.2 
⊢ ( 𝜑 → 𝐵 ∈ ℝ^{+} ) 
3 

divge0d.3 
⊢ ( 𝜑 → 0 ≤ 𝐴 ) 
4 
2

rpregt0d 
⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) 
5 

divge0 
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 ≤ ( 𝐴 / 𝐵 ) ) 
6 
1 3 4 5

syl21anc 
⊢ ( 𝜑 → 0 ≤ ( 𝐴 / 𝐵 ) ) 