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

Proof

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