I find it interesting that any automorphism of the semigroup $(\mathbb R^{\gt0},+)$ is continuous.
This is also true if we assume the Axiom of Choice; c.f. Automorphisms on (R,+) and the Axiom of Choice. The simple argument is that any morphism on $(\mathbb R^{\gt0},+)$ must preserve the order, and if you can show that it must be surjective, then it has no gaps and must be continuous; see this.
Has this found any use in the exposition of mathematical theories?
Also interested in any answer that shows two ways of proving something, one proof long and laborious, and the second argument, using this fact, considerably shorter, albeit more abstract.
The very best answers would be those that employ the theory of magnitudes.
For this exposition we are launching off the theory of magnitudes platform and are assuming that we know nothing about $(\mathbb R^{\gt0},1,+)$ except that it satisfies $\text{P-0}$ thru $\text{P-5}$ and the theorem found here.
In this study of foundational logic, we've made a beeline drive to the automorphism group of $(\mathbb R^{\gt0},+)$ and assume we only have the following three theoretical concepts under our belts:
$\quad (\mathbb N,(+,0),(1,*)) = \{0,1,2,\dots,n,\dots\}$
Note that we've only named the first $3$ numbers. We haven't 'discovered' Euclidean division or have a way of representing integers with a selected base.
-The integers,
$\quad (\mathbb Z,(+,0),(1,*)) =\{\dots,-n,\dots-2,-1,0,1,2,\dots,n,\dots\}$
-The theory of finite sets
We know that $(\mathbb N^{\gt 0},+)$ can be regarded as morphically contained in $(\mathbb R^{\gt0},+)$, but we've applied a 'forgetful functor' to the real numbers, and from here we can't even talk about the the rational numbers - there is no multiplication!.
Let us analyze the dilation automorphism, morphism $1 \mapsto 2$ on $(\mathbb R^{\gt0},+)$. We represent it with a name, $\mu_2$. It is easy to show that
$\tag 1 \sum_{k \in F} \mu_2^{k} \text{ with } F \text{ a finite subset of } \mathbb Z$
is an automorphism.
Of course when we apply it to the number $1$, numbers in $(\mathbb R^{\gt0},+)$ 'light up' (they get defined).
$\tag 2 \sum_{k \in F} \mu_2^{k} (1) = \sum_{k \in F} 2^{k}$
Let $\mathcal F (\mathbb Z)$ be the set of all finite subsets of $\mathbb Z$.
The following can be proven from this rudimentary logic platform:
Theorem 1: The mapping $F \mapsto \sum_{k \in F} \mu_2^{k}$ is an injection into the automorphism group.
The automorphisms are determined by where they send $1$, so we can also state
Theorem 2: If $\sum_{k \in F} 2^{k} = \sum_{k \in G} 2^{k}$ then the two finite sets $F$ and $G$ are identical.
So we can represent many numbers in $(\mathbb R^{\gt0},+)$. With a little effort we can show that $\sum_{k \in F} 2^{k}$ can only represent a positive integer when $F$ contains no negative integers.
The integer $1$ get represented since it corresponds to the identify automorphism applied to $1$, $\mu_2^{0}(1)$.
Assume $n$ can be represented. Using the identity
$\tag 3 2^k + 2^k = 2^{k+1}$
together with algebraic logic, we know that $n + 1$ is also represented.
Theorem 3: Every positive integer has a unique representation
$\tag 4 \sum_{k \in F} 2^{k}$
where $F$ has no negative integers.
So, without the notion of multiplication we have a representation theorem for integers.