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

Result R4830 on D866: Standard real logarithm function

Change of base formula for logarithm function

Formulation 0

Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Let $b \in (0, \infty) \setminus \{ 1 \}$ be a D5407: Positive real number.

Then \begin{equation} \log_a x = \frac{\log_b x}{\log_b a} \end{equation}

Subresults

▶	R4829: Base inversion property of standard natural logarithm function

Proofs

Proof 0

Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Let $b \in (0, \infty) \setminus \{ 1 \}$ be a D5407: Positive real number.

Directly from the definitions, we have \begin{equation} \frac{\log_b x}{\log_b a} = \frac{\frac{\log_e x}{\log_e b}}{\frac{\log_e a}{\log_e b}} = \frac{\log_e x}{\log_e a} = \log_a x \end{equation} $\square$