Theorem elogb

Description: The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using _e as the base in logb is the same as log . Definition in Cohen4 p. 352. (Contributed by David A. Wheeler, 17-Oct-2017) (Revised by David A. Wheeler and AV, 16-Jun-2020)

	Ref	Expression
Assertion	elogb	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to {\log }_{\mathrm{e}}A=\log A$$

Proof

Step	Hyp	Ref	Expression
1		ere	$$⊢\mathrm{e}\in ℝ$$
2	1	recni	$$⊢\mathrm{e}\in ℂ$$
3		ene0	$$⊢\mathrm{e}\ne 0$$
4		ene1	$$⊢\mathrm{e}\ne 1$$
5		eldifpr	$$⊢\mathrm{e}\in \left(ℂ\setminus \left\{0,1\right\}\right)\leftrightarrow \left(\mathrm{e}\in ℂ\wedge \mathrm{e}\ne 0\wedge \mathrm{e}\ne 1\right)$$
6	2 3 4 5	mpbir3an	$$⊢\mathrm{e}\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
7		logbval	$$⊢\left(\mathrm{e}\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge A\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to {\log }_{\mathrm{e}}A=\frac{\log A}{\log \mathrm{e}}$$
8	6 7	mpan	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to {\log }_{\mathrm{e}}A=\frac{\log A}{\log \mathrm{e}}$$
9		loge	$$⊢\log \mathrm{e}=1$$
10	9	oveq2i	$$⊢\frac{\log A}{\log \mathrm{e}}=\frac{\log A}{1}$$
11		eldifsn	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(A\in ℂ\wedge A\ne 0\right)$$
12		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
13	11 12	sylbi	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to \log A\in ℂ$$
14	13	div1d	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to \frac{\log A}{1}=\log A$$
15	10 14	eqtrid	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to \frac{\log A}{\log \mathrm{e}}=\log A$$
16	8 15	eqtrd	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to {\log }_{\mathrm{e}}A=\log A$$