ThmDex – An index of mathematical definitions, results, and conjectures.

Result R4829 on D865: Standard natural real logarithm function
Subresult of R4830: Change of base formula for logarithm function

Base inversion property of standard natural logarithm function

Formulation 0

Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Let $e$ be the D169: Napier's constant.

Then \begin{equation} \log_a e = \frac{1}{\log_e a} \end{equation}

Proofs

Proof 0

Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Let $e$ be the D169: Napier's constant.

Since $\log_e e = 1$, this result is a special case of R4830: Change of base formula for logarithm function. $\square$