Uniqueness of the logarithm function

Question

In my Analysis class, we started to prove a theorem that said:

Let a > 1. So there is a unique increasing function $f:(0,\infty)\to\mathbb{R}$ so that:

1. $f(a) = 1$
2. $f(xy) = f(x) + f(y)\quad\forall x, y > 0$

First we supposed its existence. Then through 2 it follows that f is a group homomorphism between the multiplicative group $(0,\infty)$ and the additive group $\mathbb{R}$.

$f(x) = f(x\cdot1) = f(x)+f(1)$, so $f(1)=0=f(x\cdot x^{-1})=f(x)+f(x^{-1})$

Then $f(x^{-1}) = -f(x)$.

We affirm that $f(x^n) = n f(x)\quad\forall x>0, n \in \mathbb{N}$ (and then we proved by induction).

Let x > 0 and $n\in \mathbb{N}^*$. So exists $m \in \mathbb{Z}$ so that $a^m \le x^n \le a^{m+1}$

So $f(a^m) \le f(x^n) \le f(a^{m+1})$, i.e. $m\le nf(x) \le m+1$

And finally $m/n \le f(x) \le (m+1)/n$

Let $A_x = \{ \frac{m}{n} : m \in \mathbb{Z},\: n \in \mathbb{N},\: a^m \le x^n\}$

So $f(x) = \sup A_x$

He said that this means f is unique, but I can see no reason why. I've omitted some lemmas and parts of the proof, but kept all the results. It's quite clear f is $log_ax$, but why it is unique?

Edit: I can't get LaTeX to work. It all seems fine while editing, but wrong in the question page.

Answer 1

Suppose that at some point $x$ the function $f(x)$ assumes a different value $f(x)\ne\sup A_x$.

If $f(x)>\sup A_x$, take a rational number $m/n$ in the interval $(\sup A_x,f(x))$. It does not belong to $A_x$ (otherwise it's at most $\sup A_x$), so $a^m>x^n$ implying $m>nf(x)$, hence $f(x)$ is less than $m/n$, a contradiction.

If $f(x)<\sup A_x$, then take any $m/n\in A_x$ which is greater than $f(x)$ (if all such $m/n\in A_x$ are less or equal than $f(x)$, then $\sup A_x$ is less or equal than $f(x)$ as well by the definition of the supremum). In this case $m/n\in A_x$ implies $a^m\le x^n$, so that $m\le nf(x)$ or $f(x)\ge m/n$, again a contradiction.

Therefore, the only choice for the function $f(x)$ to satisfy (1), (2) and the increasing property is to assume the value $\sup A_x$ at the point $x$.