@user170039 Not at all. I will admit I'm still glossing over a little. Specifically when I said that you can prove a unique $x>0$ exists that solves $x^n=a$ I'm implicitly assuming you already have some definition of $\mathbb{R}$. That's not particularly obvious and depending on how you're doing the whole thing might actually be a bit cyclical. Usually the way you get from $\mathbb{Q}$ to $\mathbb{R}$ is by using dedekind cuts or cauchy sequences. In that case you are golden.

But you could also first go to an algebraic closure of $\mathbb{Q}$ in which case what I claim you can prove is really just something you essentially define.