This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem loglt1b

Description: The logarithm of a number is less than 1 iff the number is less than Euler's constant. (Contributed by AV, 30-May-2020)

		Ref	Expression
	Assertion	loglt1b	$⊢ A \in ℝ^{+} \to (\log A < 1 \leftrightarrow A < e)$

Step	Hyp	Ref	Expression
1		epr	$⊢ e \in ℝ^{+}$
2		logltb	$⊢ (A \in ℝ^{+} \land e \in ℝ^{+}) \to (A < e \leftrightarrow \log A < \log e)$
3	1 2	mpan2	$⊢ A \in ℝ^{+} \to (A < e \leftrightarrow \log A < \log e)$
4		loge	$⊢ \log e = 1$
5	4	a1i	$⊢ A \in ℝ^{+} \to \log e = 1$
6	5	breq2d	$⊢ A \in ℝ^{+} \to (\log A < \log e \leftrightarrow \log A < 1)$
7	3 6	bitr2d	$⊢ A \in ℝ^{+} \to (\log A < 1 \leftrightarrow A < e)$