Metamath Proof Explorer
Description: Natural logarithm preserves <_ . (Contributed by Mario Carneiro, 29May2016)


Ref 
Expression 

Hypotheses 
relogcld.1 
⊢ ( 𝜑 → 𝐴 ∈ ℝ^{+} ) 


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

Assertion 
logled 
⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

relogcld.1 
⊢ ( 𝜑 → 𝐴 ∈ ℝ^{+} ) 
2 

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

logleb 
⊢ ( ( 𝐴 ∈ ℝ^{+} ∧ 𝐵 ∈ ℝ^{+} ) → ( 𝐴 ≤ 𝐵 ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ) ) 
4 
1 2 3

syl2anc 
⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ) ) 