Logarithms and their properties: ‘simple proofs’

I was thinking recently about the 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 by is defined as where is the set of real number and indicates multiplication. The definition states the the division of by produces a unique number that satisfies the formula . In effect this means division is the theorem 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 in base , , can therefore be defined as and in effect

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

Exponentiation

Below is a proof of  using the definition above.

Hence

Multiplication

Below is a proof of  using the definition above.

Let and . Hence we have

From the logarithm definition (Equation ??) and the definition of and above, we have that and , and hence

Division

The proof of  is similar to the multiplication property.

Let and . Hence we have

From the logarithm definition (Equation ??) and the definition of and above, we have that and , and hence

Base Conversion

Below is a proof of the property .

From the exponentiation property, we have that

But , and hence