Associativity, commutativity and distributivity of modulo arithmetic

To prove (or "notice") that $\mathbb{Z}/13\mathbb{Z}$ is a (cyclic) group under addition you would need to know first of all that it is a group under addition; and in order to know that it is a group under addition, you would need to know that addition is associative, has an identity element, and has inverses; so you have to show it is associative. You cannot save yourself knowing/showing it is associative by first showing it's a group: showing/knowing associativity is a prerequisite of it being a group.

You don't have to prove it by "case analysis", but only through the basic properties of congruences. The key is really to show that addition and multiplication are well defined.

That is, we define addition and multiplication in $\mathbb{Z}/n\mathbb{Z}$ by "class representatives": if $[a]$ is the modular class of $a$, and $[b]$ is the modular class of $b$, we define $[a]+[b]$ as $[a+b]$ and $[a][b]$ as $[ab]$. So long as these operations are well-defined, the properties will be inherited from the properties of the usual addition and multiplication of integers (just like in any ring modulo an ideal).

To show it is well-defined, you need to show that if $[a]=[x]$ and $[b]=[y]$, then $[a+b]=[x+y]$ and $[ax]=[by]$. This is a direct consequence of the properties of congruences, namely that if $a\equiv x\pmod{n}$ and $b\equiv y\pmod{n}$, then $a+b\equiv x+y\pmod{n}$ and $ab\equiv xy\pmod{n}$. Verifying these through the definition of congruence is indeed trivial: If $a-x$ and $b-y$ are multiples of $n$, then so is $(a-x)+(b-y) = (a+b)-(x+y)$; and likewise, $(a-x)b + (b-y)x = ab - xy$ is also a multiple of $n$, being a sum of multiples of $n$.

The properties of the addition and multiplication of congruence classes now follows from the same properties for integers.

Added. It's important to note that it is not merely the fact that we are dealing with equivalence classes that makes this work. The key is really that the operations on equivalence classes defined via representatives are well defined. We have a set $S$ on which we already have a (binary) operation $*$, and an equivalence relation $\sim$ on $S$. If we want to define an operation on the congruence classes $S/\sim$ by using $*$, then the natural definition is to try $[a]*[b]=[a*b]$. That is: the "product" of the classes is the class of the "product". However, this does not always work correctly: it will depend on the operation and how $\sim$ relates to the operation. In the case of groups, for example, the only equivalence relations for which this definition works are the equivalence relations induced by normal subgroups (see my answer to this previous question for an ample discussion of trying to define an operation on equivalence classes in a group).

So it is not the fact that we have an equivalence relation/partition, but really how the partition behaves relative to the operation.

What we have is the following general result from Universal Algebra:

Theorem. Let $S$ be a set, and let $*$ be an $n$-ary operation on $S$. If $\sim$ is an equivalence relation on $S$, then the operation on $S/\sim$ defined by $$*([s_1],\ldots,[s_n]) = [*(s_1,\ldots,s_n)]$$ is well-defined if and only if $\sim$ is closed under $*\times*$ as a subset of $S\times S$, where $$*\times*\Bigl((a_1,b_1),\ldots,(a_n,b_n)\Bigr) = \Bigl(*(a_1,\ldots,a_n),*(b_1,\ldots,b_n)\Bigr).$$

Proof. Suppose $*$ is well defined. If $(a_1,b_1),\ldots,(a_n,b_n)\in \sim$, then $[a_i]=[b_i]$, so by assumption we have that $$[*(a_1,\ldots,a_n)] = *([a_1],\ldots,[a_n]) = *([b_1],\ldots,[b_n])=[*(b_1,\ldots,b_n)].$$ Therefore, $$*\times *\Bigl( (a_1,b_1),\ldots,(a_n,b_n)\Bigr) = \bigl( *(a_1,\ldots,a_n),*(b_1,\ldots,b_n)\bigr)\in \sim,$$ so $\sim$ is closed under $*\times *$.

Conversely, suppose that $\sim$ is closed under $*\times *$, and that $[a_1]=[b_1],\ldots,[a_n]=[b_n]$. We need to show that $*([a_1],\ldots,[a_n]) = *([b_1],\ldots,[b_n])$. Since $(a_1,b_1),\ldots,(a_n,b_n)\in \sim$, then $$*\times *\Bigl( (a_1,b_1),\ldots,(a_n,b_n)\Bigr) = \Bigl(*(a_1,\ldots,a_n),*(b_1,\ldots,b_n)\Bigr)\in \sim,$$ hence $[*(a_1,\ldots,a_n)] = [*(b_1,\ldots,b_n)]$. But this is exactly what we need to show $*$ is well defined on $S/\sim$. QED

So if the equivalence relation is a substructure of $S\times S$, then we can define the induced operation on $S/\sim$ via representatives, and this operation on $S/\sim$ will inherit the properties of the operation from $S$.

Thus, to show that sums and products of congruence classes modulo $m$ in the integers inherit the properties of the sum and product of integers is equivalent to showing that the equivalence relation "congruent modulo $m$", $\equiv_m$, interpreted as a subset of $\mathbb{Z}\times\mathbb{Z}$, is a subring of $\mathbb{Z}\times\mathbb{Z}$ (the latter with coordinate-wise operations). This is precisely showing that if $a\equiv x\pmod{m}$ (i.e., $(a,x)\in\equiv_m$) and $b\equiv y\pmod{m}$ (i.e., $(b,y)\in\equiv_m$) , then $a+b\equiv x+y\pmod{m}$ (i.e., $(a,x)+(b,y)=(a+b,x+y)\in\equiv_m$) and $ab\equiv xy\pmod{m}$ (i.e., $(a,x)(b,y) = (ab,xy)\in\equiv_m$). So it still comes down to the specific properties of the equivalence relation, and not merely to the fact that it is an equivalence relation.

That ring axioms are preserved in congruence rings is simply a derived consequence of the fact that the map to the congruence class $\rm\ n\to [n]\ $ is a homomorphism, i.e. it preserves all the fundamental operations of the structure. Thus it necessarily preserves expressions composed of these operations, and hence it preserves all identities (laws) expressed in terms of these operations. For example, let's explicitly derive the preservation of the distributive law in a congruence ring:

$\rm\quad\quad\quad\quad [a(b+c)]\ =\ [a][b+c]\ =\ [a]([b]+[c])$

$\rm\quad\quad\quad\quad [ab+ac]\ =\ [ab]+[ac]\ =\ [a][b]+ [a][c]$

Hence $\rm\ [a]([b]+[c])\ =\ [a][b]+[a][c]\ $ i.e. the distributive law holds too in the congruence ring. Precisely the same proof works also for all the other ring laws, e.g. associative, commutative, etc. One is simply lifting a preservation property from the generating operations to expressions composed of those fundamental generating operations.