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

Metamath Proof Explorer

Theorem logle1b

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

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

Proof

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