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 \left(\log A\le 1\leftrightarrow A\le \mathrm{e}\right)$$

Proof

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