Integer Powers in a Group

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(G,\cdot)$ be a group with identity $e$, unique by Uniqueness of the Identity Element and of Inverses in a Group (i), let $g\in G$, and let $n$ be an integer.

(i) Integer powers. If $n\ge0$, then $n$ is an element of $\mathbb{N}_{0}$ under The Integers and the Rational Numbers, with the Natural Numbers and the Integers Identified with Subsets of the Rationals (vii), and the $n$-th power $g^{n}$ of $g$ is that of Powers with Exponents in the Natural Numbers with Zero (i) and Powers with Exponents in the Natural Numbers with Zero (ii); in particular $g^{0}=e$. If $n<0$, then $-n$ is a natural number by The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements (vii), and the $n$-th power of $g$ is

$$g^{n}=(g^{-1})^{-n},$$

the $(-n)$-th power, as in Powers with Exponents in the Natural Numbers with Zero (i), of the inverse $g^{-1}$ of $g$, which is unique by Uniqueness of the Identity Element and of Inverses in a Group (ii).