How do we formally define powers/exponentiation in the theory of the reals? Assume the  second-order theory of the real numbers (it has to be second-order for categoricity) and suppose that we've already gone through the trouble of proving the existence and uniqueness of the natural numbers. That is, we have proven $\vdash \exists!X\Phi_N$, where $\Phi_N$ is a sentence uniquely characterizing the natural numbers. For convenience sake, we will use the macro
$$\mathbf N(x):=\exists! X(X(x)\land\Phi_N)$$
Now we want to define the power function. Specifically, we want to show
$$\vdash\forall x\forall n((\mathbf N(n)\land(1\le n))\implies\exists!y\epsilon(x,n,y))$$
where $\epsilon(x,n,y)$ is a formula with the same intensional meaning as $x^n=y$ (we will concern ourselves only with positive integer powers.)
How do we formally define exponentiation? What is $\epsilon(x,n,y)$?
The arithmetical definitions I have seen rely on properties of the natural numbers (remainders, factorization, etc.) to work. While I imagine it's possible to extend some of this to the reals (chiefly through modular arithmetic) and define exponentiation that way, I don't want to spend weeks deconstructing the logic of real modular arithmetic just to find out that some long-dead mathematician found a shorter way to do this 100 years ago.

Note: the answer is not "work inside the model to avoid formalization." Working inside a model of the theory of the reals means building out the set of the theorems of ZFC that describe the model up to isomorphism. This, if anything, requires more formal work; we essentially need to create an encoded copy of the theory of the reals (without knowing what it is) inside of ZFC, then figure out how to decode it so that we can recover the theory and verify that our model really is a model.
 A: One solution is as follows:
$$\epsilon(n, x, y) :\equiv \forall Q (\forall z (Q(1, z, z)) \land \forall m, w, z (Q(m, w, z) \to Q(m + 1, w, wz)) \to Q(n, x, y))$$
This states that $\epsilon$ is the least predicate such that the identities $\forall x (\epsilon(1, x, x))$ and $\forall n, x, y (\epsilon(n, x, y) \to \epsilon(n + 1, x, xy))$ both hold. It should be straightforward to prove that for any $x, n$, the following are equivalent: (1) $\mathbf{N}(n)$, (2) $\exists y (\epsilon(n, x, y))$, and (3) $\exists! y (\epsilon(n, x, y))$.
Another solution which avoids additional use of second-order quantifiers (but of course requires $\mathbf{N}$ to be added as a symbol) is as follows:
First, note that we can define $n^m$ using first-order Peano arithmetic for $n, m \in \mathbb{N}$. So we can define exponentiation with natural number base and exponent using first-order logic and $\mathbf{N}$.
We can define $\mathbf{Q}(q) = \exists a, b (\mathbf{N}(a) \land \mathbf{N}(b) \land (q = 0 \lor bq = a \lor bq = -a))$. This is m first-order. It’s clear that using exponents with a natural number base, we can define exponents with a rational base in a first-order manner.
Finally, we can use the density of the rationals and the continuity of exponentiation to define real exponentiation. $x^n$ is the unique $y$ such that $\forall \epsilon > 0 \exists \delta > 0 \forall q (\mathbf{Q}(q) \land |q - x| < \delta \to |q^n - y| < \epsilon)$. Here, $q^n$ is defined with rational exponentiation as above.
