Proof of Powers and Images of Natural Numbers in a Commutative Ring Lie in the Ring

Each result cited is universally quantified over the data in its own statement. No choice is used.

By Commutative Rings §ring, whose framing makes $R$ a set, and by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, in force by Commutative Rings, Fields and Ordered Fields: Standard Notation §base, both $R$ and $\mathbb{N}_{0}$ are sets. No map or class is formed from a formula in this proof: each map used is one whose existence a cited clause asserts.

Clause powers. Let $x\in R$ and $n\in\mathbb{N}_{0}$. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §ring-powers applied to $R$ and $x$, there is a map $p:\mathbb{N}_{0}\to R$ with $p(m)=x^{m}$ for every $m\in\mathbb{N}_{0}$. As $n\in\mathbb{N}_{0}$, Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph, applied with $A=\mathbb{N}_{0}$, $B=R$, $f=p$ and $a=n$, gives $p(n)\in R$. Hence $x^{n}=p(n)\in R$.

Clause images. Let $n\in\mathbb{N}_{0}$. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §images, applied to $R$, there is a map $\nu:\mathbb{N}_{0}\to R$ with $\nu(m)=m_{R}$ for every $m\in\mathbb{N}_{0}$. As $n\in\mathbb{N}_{0}$, Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §graph, applied with $A=\mathbb{N}_{0}$, $B=R$, $f=\nu$ and $a=n$, gives $\nu(n)\in R$. Hence $n_{R}=\nu(n)\in R$.