# Metamath Proof Explorer

## Theorem logleb

Description: Natural logarithm preserves <_ . (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion logleb ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\le {B}↔\mathrm{log}{A}\le \mathrm{log}{B}\right)$

### Proof

Step Hyp Ref Expression
1 logltb ${⊢}\left({B}\in {ℝ}^{+}\wedge {A}\in {ℝ}^{+}\right)\to \left({B}<{A}↔\mathrm{log}{B}<\mathrm{log}{A}\right)$
2 1 ancoms ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left({B}<{A}↔\mathrm{log}{B}<\mathrm{log}{A}\right)$
3 2 notbid ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left(¬{B}<{A}↔¬\mathrm{log}{B}<\mathrm{log}{A}\right)$
4 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
5 rpre ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℝ$
6 lenlt ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {B}↔¬{B}<{A}\right)$
7 4 5 6 syl2an ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\le {B}↔¬{B}<{A}\right)$
8 relogcl ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}{A}\in ℝ$
9 relogcl ${⊢}{B}\in {ℝ}^{+}\to \mathrm{log}{B}\in ℝ$
10 lenlt ${⊢}\left(\mathrm{log}{A}\in ℝ\wedge \mathrm{log}{B}\in ℝ\right)\to \left(\mathrm{log}{A}\le \mathrm{log}{B}↔¬\mathrm{log}{B}<\mathrm{log}{A}\right)$
11 8 9 10 syl2an ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left(\mathrm{log}{A}\le \mathrm{log}{B}↔¬\mathrm{log}{B}<\mathrm{log}{A}\right)$
12 3 7 11 3bitr4d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\le {B}↔\mathrm{log}{A}\le \mathrm{log}{B}\right)$