Extension of Tarski's result on the decidability of reals
I doubt there's a proof you can cite, since the result is obvious. The "features" you're adding are first-order definable, and first-order logic is closed under substitution.