ThmDex – An index of mathematical definitions, results, and conjectures.
Standard logarithm of a positive real number raised to an integer power
Formulation 0
Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Let $x \in (0, \infty)$ be a D5407: Positive real number.
Let $N \in \mathbb{Z}$ be a D995: Integer.
Then \begin{equation} \log_a x^N = N \log_a x \end{equation}
Proofs
Proof 0
Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Let $x \in (0, \infty)$ be a D5407: Positive real number.
Let $N \in \mathbb{Z}$ be a D995: Integer.
If $N = 0$, then $x^N = 1$ whence result R4828: Logarithm of one is zero shows that $\log_a x^N = 0 = 0 \cdot \log_a x$ so that the claim holds. Assume next that $N \geq 1$. Then, using result R4831: Homomorphism property of standard logarithm function, we have \begin{equation} \log_a x^N = \log_a \left( \prod_{n = 1}^N x \right) = \sum_{n = 1}^N \log_a x = N \log_a x \end{equation} Finally, if $N \leq -1$, then we may use the above argument with respect to the positive basic real number $1 / x$. The proof is therefore complete. $\square$