Prove $(x+y) \text{ mod } n = ((x \text{ mod } n)+(y \text{ mod } n)) \text{ mod } n,\,$ and product analog 
For all $n \in \mathbb{N}$, $n > 1$ and $x,y \in \mathbb{Z}$ prove that
\begin{equation}
  (x+y) \text{ mod } n
  = ((x \text{ mod } n)+(y \text{ mod } n))\text{ mod } n.
\end{equation}

Would this be a proof if I say:
Let $x = x' \text{ mod } n$ and let $y=y' \text{ mod } n$. Then
\begin{equation}
  x+y = x'+y' \text{ mod } n.
\end{equation}
Now, if we look at the current thing we want prove, this will follow:
\begin{equation}
  x+y \text { mod } n = (x \text{ mod } n + y \text{ mod } n) \text{ mod } n.
\end{equation}

I'm not sure if this is allowed or will count as a "proof" at all. Maybe you can show me some other ways of doing this, more precise ones?
 A: Recall $\,\ a\equiv b\pmod {\!n}\!\color{#c00}\iff\! (\overbrace{a\ {\rm mod}\ n}^{\large a'}) = (\overbrace{b\ {\rm mod}\ n}^{\large b'}),\,$  so by Congruence Rules
$\qquad\qquad\ \begin{align} {\rm mod}\ n\!:\qquad x&\,\color{#c00}\equiv\,  x'\\
y&\,\color{#c00}\equiv\, y'\\  
\Rightarrow\qquad\qquad\ x+y&\, \equiv\,  x' + y'\ \  \ \ \text{by Congruence Sum Rule}\\[.2em]
\Rightarrow\, (x+y)\ {\rm mod}\ n\, &=\, (x' + y')\ {\rm mod}\ n\ \ \ \ {\rm by}\ (\color{#c00}{\Rightarrow})\rm \ above\end{align}$
The same proof works for products by changing $+$ to $*,\,$ using the Congruence Product Rule., so
$$\bbox[5px,border:1px solid #c00]{\begin{align} 
(x+y)\bmod n &\,=\, (x\bmod n  + y\bmod n)\bmod n\\[.2em]
(x\,*\,y)\bmod n &\,=\:\! (x\bmod n  \,*\, y\bmod n)\bmod n \end{align}}\qquad\qquad$$
Generally, as above, to prove an identity about mod as an operation it is usually easiest to first convert it into the more flexible congruence relation form, prove it using congruences, then convert back to operator form at the end (using the equivalence in the first line above).
See here for much further discussion of $\!\bmod\!$ as an operator vs. (congruence) relation.
See here for how to interpret the above as transporting the ring operations on cosets in the quotient ring $\,\Bbb Z/n\,$ to corresponding operations on their normal-form (remainder) reps in $\,\Bbb Z_n$.
A: I will assume that $x\pmod n$ stands for element of $\{0,1\ldots,n-1\}$ which I will denote with $x'$ such that $x = kn + x'$. But, it doesn't actually matter at all.
First, let me clarify definitions: $x\equiv x'\pmod n$ if and only if $n\mid x - x'$. Note that since we have Euclidean division (division with remainder) in $\Bbb Z$, for every $x\in\Bbb Z$, there is a unique number $x'\in\{0,\ldots,n-1\}$ such that $x = kn + x'$ for some $k\in\Bbb Z$ (which you denote by $x\pmod n$). But, $x-x' = kn$ which implies that $x\equiv x'\pmod n$. Conversely, if $x\equiv x'\pmod n$ and $x'\in\{0,1,\ldots,n-1\}$, then $x' = x\pmod n$. So, to prove your statement, I will use this more general notion of congruence.
I claim that whenever $x\equiv x'\pmod n$ and $y\equiv y'\pmod n$, then $x+y\equiv x' + y'\pmod n$ (i.e., addition is well defined in modular arithmetic). This will give your result as a special case.
So, $x-x' = kn$, $y - y' = ln$, with $k,l\in\Bbb Z$. Add this two to get $(x+y)-(x'+y') = (k+l)n$ which implies that $x + y\equiv x'+y'\pmod n$.
