logleb

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

		Ref	Expression
	Assertion	logleb	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (A \leq B \leftrightarrow \log A \leq \log B)$

Step	Hyp	Ref	Expression
1		logltb	$⊢ (B \in ℝ^{+} \land A \in ℝ^{+}) \to (B < A \leftrightarrow \log B < \log A)$
2	1	ancoms	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (B < A \leftrightarrow \log B < \log A)$
3	2	notbid	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (\neg B < A \leftrightarrow \neg \log B < \log A)$
4		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
5		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
6		lenlt	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq B \leftrightarrow \neg B < A)$
7	4 5 6	syl2an	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (A \leq B \leftrightarrow \neg B < A)$
8		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
9		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
10		lenlt	$⊢ (\log A \in ℝ \land \log B \in ℝ) \to (\log A \leq \log B \leftrightarrow \neg \log B < \log A)$
11	8 9 10	syl2an	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (\log A \leq \log B \leftrightarrow \neg \log B < \log A)$
12	3 7 11	3bitr4d	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (A \leq B \leftrightarrow \log A \leq \log B)$

Metamath Proof Explorer