Logarithms and their properties: ‘simple proofs’

I was thinking recently about the CHOOSE operator that Leslie Lamport describes in his book “Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers”. He uses it to describe things like division where a unique number is defined as something that satisfies a formula. For example, the division of a by b is defined as

    \[ a/b \triangleq CHOOSE ~ c \in \mathbb{R} : a = b \cdot c \]

where \mathbb{R} is the set of real number and \cdot indicates multiplication. The definition states the the division of a by b produces a unique number c that satisfies the formula a = b \cdot c. In effect this means division is the theorem

    \[a/b = c \Leftrightarrow a = b\cdot c \]

This came to mind when I was thinking of a way to express the definition of a logarithm from which I could derive its various properties. I wanted to do this derivation myself before searching for others online (after my search, it turns out people typically use a similar approach).The logarithm of a in base b, log_{b} (a), can therefore be defined as

    \[ log_{b} (a) \triangleq CHOOSE~ c \in \mathbb{R} : a = b^{c} \]

and in effect

(1)   \begin{equation*} log_{b} (a) = c \Leftrightarrow a = b^{c} \end{equation*}

From this we can derive the various properties of the logarithm and provide simple proofs.

Exponentiation

Below is a proof of log_{b} (a^{x}) = x\cdot log_{b} (a) using the definition above.

(2)   \begin{align*} log_{b} (a^{x}) = c &\Rightarrow a^{x} = b^{c}\\ &\Rightarrow a = (b)^{\frac{c}{x}}\\ &\Rightarrow log_{b} (a) = \frac{c}{x}\\ &\Rightarrow x\cdot log_{b} (a) = c = log_{b} (a^{x}) \end{align*}

Hence log_{b} (a^{x}) = x\cdot log_{b} (a)

Multiplication

Below is a proof of log_{b} (a_{1}\cdot a_{2}) =  log_{b} (a_{1}) + log_{b} (a_{2}) using the definition above.

(3)   \begin{equation*} log_{b} (a_{1}\cdot a_{2}) = c \Rightarrow a_{1}\cdot a_{2} = b^{c} \end{equation*}

Let a_{1} = b^{c_{1}} and a_{2} = b^{c_{2}}. Hence we have

(4)   \begin{equation*} a_{1} \cdot a_{2} = b^{c_{1}}\cdot b^{c_{2}} = b^{(c_{1} + c_{2})} \Rightarrow log_{b} (a_{1}\cdot a_{2}) = c_{1} + c_{2} \end{equation*}

From the logarithm definition (Equation 1) and the definition of a_{1} and a_{2} above, we have that log_{b} (a_{1}) = c_{1} and log_{b} (a_{2}) = c_{2}, and hence

(5)   \begin{equation*} log_{b} (a_{1}\cdot a_{2}) = c_{1} + c_{2} = log_{b} (a_{1}) + log_{b} (a_{2}) \end{equation*}

Division

The proof of log_{b} (\frac{a_{1}}{ a_{2}}) =  log_{b} (a_{1}) - log_{b} (a_{2}) is similar to the multiplication property.

(6)   \begin{equation*} log_{b} (\frac{a_{1}}{ a_{2}}) = c \Rightarrow \frac{a_{1}}{ a_{2}} = b^{c} \end{equation*}

Let a_{1} = b^{c_{1}} and a_{2} = b^{c_{2}}. Hence we have

(7)   \begin{equation*} \frac{a_{1}}{ a_{2}} = \frac{b^{c_{1}}}{b^{c_{2}}} = b^{(c_{1} - c_{2})} \Rightarrow log_{b} (a_{1}\cdot a_{2}) = c_{1} - c_{2} \end{equation*}

From the logarithm definition (Equation 1) and the definition of a_{1} and a_{2} above, we have that log_{b} (a_{1}) = c_{1} and log_{b} (a_{2}) = c_{2}, and hence

(8)   \begin{equation*} log_{b} (\frac{a_{1}}{ a_{2}}) = c_{1} - c_{2} = log_{b} (a_{1}) - log_{b} (a_{2}) \end{equation*}

Base Conversion

Below is a proof of the property log_{b}(x) = \frac{log_{a}(x)}{log_{a}(b)}.

(9)   \begin{equation*} log_{b}(x) &= c \Rightarrow x = b^c \Rightarrow log_{a}(x) = log_{a}(b^c) \end{equation*}

From the exponentiation property, we have that

(10)   \begin{equation*} log_{a}(x) = c\cdot log_{a}(b) \Rightarrow c = \frac{log_{a}(x)}{log_{a}(b)} \end{equation*}

But log_{b}(x) = c, and hence log_{b}(x) =  \frac{log_{a}(x)}{log_{a}(b)}