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

Proof

Step	Hyp	Ref	Expression
1		logltb	$$⊢\left(B\in {ℝ}^{+}\wedge A\in {ℝ}^{+}\right)\to \left(B<A\leftrightarrow \log B<\log A\right)$$
2	1	ancoms	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(B<A\leftrightarrow \log B<\log A\right)$$
3	2	notbid	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(\neg B<A\leftrightarrow \neg \log B<\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\leftrightarrow \neg B<A\right)$$
7	4 5 6	syl2an	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(A\le B\leftrightarrow \neg B<A\right)$$
8		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
9		relogcl	$$⊢B\in {ℝ}^{+}\to \log B\in ℝ$$
10		lenlt	$$⊢\left(\log A\in ℝ\wedge \log B\in ℝ\right)\to \left(\log A\le \log B\leftrightarrow \neg \log B<\log A\right)$$
11	8 9 10	syl2an	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(\log A\le \log B\leftrightarrow \neg \log B<\log A\right)$$
12	3 7 11	3bitr4d	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(A\le B\leftrightarrow \log A\le \log B\right)$$