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\leftrightarrow \log A<\log B\right)$$

Proof

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