ThmDex – An index of mathematical definitions, results, and conjectures.
Logarithm of a ratio
Formulation 0
Let $\log_a$ be the D866: Standard real logarithm function in base $a \in (0, \infty) \setminus \{ 1 \}$.
Let $x, y \in (0, \infty)$ each be a D5407: Positive real number.
Then \begin{equation} \log_a \frac{x}{y} = \log_a x - \log_a y \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, y \in (0, \infty)$ each be a D5407: Positive real number.
Applying results
(i) R4832: Homomorphism property of standard logarithm function in the binary case
(ii) R4857: Standard logarithm of a positive real number raised to an integer power

to the positive basic real numbers $x$ and $1 / y$, we have \begin{equation} \log_a \frac{x}{y} = \log_a x + \log_a y^{-1} = \log_a x - \log_a y \end{equation} $\square$