# 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

(1)

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.

(2)

Hence

### Multiplication

Below is a proof of using the definition above.

(3)

Let and . Hence we have

(4)

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

(5)

### Division

The proof of is similar to the multiplication property.

(6)

Let and . Hence we have

(7)

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

(8)

### Base Conversion

Below is a proof of the property .

(9)

From the exponentiation property, we have that

(10)

But , and hence