Metamath Proof Explorer
Description: Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28May2016)


Ref 
Expression 

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


divgt0d.2 
⊢ ( 𝜑 → 𝐵 ∈ ℝ ) 


lemulge11d.3 
⊢ ( 𝜑 → 0 ≤ 𝐴 ) 


lemulge11d.4 
⊢ ( 𝜑 → 1 ≤ 𝐵 ) 

Assertion 
lemulge12d 
⊢ ( 𝜑 → 𝐴 ≤ ( 𝐵 · 𝐴 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

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

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

lemulge11d.4 
⊢ ( 𝜑 → 1 ≤ 𝐵 ) 
5 

lemulge12 
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 1 ≤ 𝐵 ) ) → 𝐴 ≤ ( 𝐵 · 𝐴 ) ) 
6 
1 2 3 4 5

syl22anc 
⊢ ( 𝜑 → 𝐴 ≤ ( 𝐵 · 𝐴 ) ) 