Theorem loge

Description: The natural logarithm of _e . One case of Property 1b of Cohen p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007)

	Ref	Expression
Assertion	loge	$$⊢\log \mathrm{e}=1$$

Proof

Step	Hyp	Ref	Expression
1		df-e	$$⊢\mathrm{e}={\mathrm{e}}^1$$
2	1	eqcomi	$$⊢{\mathrm{e}}^1=\mathrm{e}$$
3		epr	$$⊢\mathrm{e}\in {ℝ}^{+}$$
4		1re	$$⊢1\in ℝ$$
5		relogeftb	$$⊢\left(\mathrm{e}\in {ℝ}^{+}\wedge 1\in ℝ\right)\to \left(\log \mathrm{e}=1\leftrightarrow {\mathrm{e}}^1=\mathrm{e}\right)$$
6	3 4 5	mp2an	$$⊢\log \mathrm{e}=1\leftrightarrow {\mathrm{e}}^1=\mathrm{e}$$
7	2 6	mpbir	$$⊢\log \mathrm{e}=1$$