# Metamath Proof Explorer

## Theorem logltb

Description: The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007)

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

### Proof

Step Hyp Ref Expression
1 relogiso ${⊢}\left({log↾}_{{ℝ}^{+}}\right){Isom}_{<,<}\left({ℝ}^{+},ℝ\right)$
2 df-isom ${⊢}\left({log↾}_{{ℝ}^{+}}\right){Isom}_{<,<}\left({ℝ}^{+},ℝ\right)↔\left(\left({log↾}_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1 onto}{⟶}ℝ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({x}<{y}↔\left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)\right)\right)$
3 1 2 mpbi ${⊢}\left(\left({log↾}_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1 onto}{⟶}ℝ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({x}<{y}↔\left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)\right)\right)$
4 3 simpri ${⊢}\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({x}<{y}↔\left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)\right)$
5 breq1 ${⊢}{x}={A}\to \left({x}<{y}↔{A}<{y}\right)$
6 fveq2 ${⊢}{x}={A}\to \left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)=\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)$
7 6 breq1d ${⊢}{x}={A}\to \left(\left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)↔\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)\right)$
8 5 7 bibi12d ${⊢}{x}={A}\to \left(\left({x}<{y}↔\left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)\right)↔\left({A}<{y}↔\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)\right)\right)$
9 breq2 ${⊢}{y}={B}\to \left({A}<{y}↔{A}<{B}\right)$
10 fveq2 ${⊢}{y}={B}\to \left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)=\left({log↾}_{{ℝ}^{+}}\right)\left({B}\right)$
11 10 breq2d ${⊢}{y}={B}\to \left(\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)↔\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({B}\right)\right)$
12 9 11 bibi12d ${⊢}{y}={B}\to \left(\left({A}<{y}↔\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)\right)↔\left({A}<{B}↔\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({B}\right)\right)\right)$
13 8 12 rspc2v ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({x}<{y}↔\left({log↾}_{{ℝ}^{+}}\right)\left({x}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({y}\right)\right)\to \left({A}<{B}↔\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({B}\right)\right)\right)$
14 4 13 mpi ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left({A}<{B}↔\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({B}\right)\right)$
15 fvres ${⊢}{A}\in {ℝ}^{+}\to \left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)=\mathrm{log}{A}$
16 fvres ${⊢}{B}\in {ℝ}^{+}\to \left({log↾}_{{ℝ}^{+}}\right)\left({B}\right)=\mathrm{log}{B}$
17 15 16 breqan12d ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left(\left({log↾}_{{ℝ}^{+}}\right)\left({A}\right)<\left({log↾}_{{ℝ}^{+}}\right)\left({B}\right)↔\mathrm{log}{A}<\mathrm{log}{B}\right)$
18 14 17 bitrd ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left({A}<{B}↔\mathrm{log}{A}<\mathrm{log}{B}\right)$