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) $$