Formalizing $na$ for $n\in\mathbb{Z}$ and $a\in R$ where $R$ is a ring. Let $R$ be a ring and let $n\in\mathbb{Z}$.
Given $a\in R$, I've seen $na$ defined as
$$
na:=\begin{cases}0&\text{if }n=0,\\\underbrace{a+a+\cdots+a}_{n\text{ times}}&\text{if }n>0,\\\underbrace{-a-a-\cdots-a}_{|n|\text{ times}}&\text{if }n<0.\end{cases}\tag{1}
$$
With this definition, I've even read that
$$
(m+n)a=ma+na\tag{2}
$$
and
$$
(mn)1=(m1)(n1)\tag{3}
$$
are obvious (and I do agree with this view).

Question:
(i) Isn't $(1)$ informal? If so, would $na$ be formally defined, for $n\geq0$, recursively via the equations
  \begin{align*}
0a&=0\tag{4}\\
(n+1)a&=na+a\tag{5}
\end{align*}
  and for $n<0$ by $na:=-(-n)a$ ?
(ii) Would formal proofs of $(2)$ and $(3)$ be as given below?
I'm asking since I've never seen this done...

Proof of $(2)$: For fixed $m$, proceed by induction on $n$ for $n\geq-m$. Then, for $n<-m$,
$$
(m+n)a=-(-m-n)a=-((-m)a+(-n)a)=-(-m)a-(-n)a=ma+na
$$
Proof of $(3)$: First show the result for $n\in\mathbb{Z}$ and $m\geq0$. To do so, prove by induction on $m$ for fixed $n$ that $(mn)1=m(n1)$ (making use of $(2)$) and then that this equals $(m1)(n1)$, by induction on $m$ again. Finally, for $m<0$,
$$
(mn)1=(-(-m)n)1=-((-m)n)1=-((-m)1)(n1)=(-(-m)1)(n1)=(m1)(n1)
$$
 A: $na$ is simply $a^n$ in the additive group of $R$, written additively of course.
In other words, since $\mathbb Z$ is a cyclic group generated by $1 \in \mathbb Z$, there is a unique homomorphism $\mu: \mathbb Z \to R^+$ of additive groups such that $\mu(1)=a$. Then $na$ is simply $\mu(n)$.
A: Your comment in the answer to @lhf is correct. This is formalized in set theory with the concept of recursive definition, in this case, the recursive definition of a homomorphism $f_a : \mathbb{Z} \to R$ with the property that $f_a(1)=a$. 
Informally it goes just like what you wrote: first define $f_a(1)$ which has already been done; then define $f_a(n)$ by a formula expressed in terms of the values of $f_a(1),…,f_a(n-1)$, in this case $f_a(n)=f_a(n-1)+a$. The principal of recursive definition then guarantees the existence of this function $f_a$ on the natural numbers, and then you extend to zero and negative numbers in the obvious way. 
This informal way of doing a recursive definition is almost universally acceptable, because a complete and formal recursive definition is often quite tedious and without much mathematical interest. There are definitely exceptions, though, where one really ought to write out the details of a recursive definition. 
Once you've proved the existence of $f_a$, you still want to prove that it is a homomorphism, and this will be a proof by induction.
And as long as we've gone this far, you may also wish to formally verify, using the axioms of set theory, that the formula $a \mapsto f_a$ defines a function from $R$ to the set of homomorphisms $\mathbb{Z} \to R$. This way one can completely formalize the definition of $n \cdot a$ to be $n \cdot a = f_a(n)$.
