# Metamath Proof Explorer

## Theorem zncrng

Description: Z/nZ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis zncrng.y ${⊢}{Y}=ℤ/{N}ℤ$
Assertion zncrng ${⊢}{N}\in {ℕ}_{0}\to {Y}\in \mathrm{CRing}$

### Proof

Step Hyp Ref Expression
1 zncrng.y ${⊢}{Y}=ℤ/{N}ℤ$
2 nn0z ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℤ$
3 eqid ${⊢}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)=\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)$
4 eqid ${⊢}{ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)={ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)$
5 3 4 zncrng2 ${⊢}{N}\in ℤ\to {ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\in \mathrm{CRing}$
6 2 5 syl ${⊢}{N}\in {ℕ}_{0}\to {ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\in \mathrm{CRing}$
7 eqidd ${⊢}{N}\in {ℕ}_{0}\to {\mathrm{Base}}_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}={\mathrm{Base}}_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}$
8 3 4 1 znbas2 ${⊢}{N}\in {ℕ}_{0}\to {\mathrm{Base}}_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}={\mathrm{Base}}_{{Y}}$
9 3 4 1 znadd ${⊢}{N}\in {ℕ}_{0}\to {+}_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}={+}_{{Y}}$
10 9 oveqdr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({x}\in {\mathrm{Base}}_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}\wedge {y}\in {\mathrm{Base}}_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}\right)\right)\to {x}{+}_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}{y}={x}{+}_{{Y}}{y}$
11 3 4 1 znmul ${⊢}{N}\in {ℕ}_{0}\to {\cdot }_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}={\cdot }_{{Y}}$
12 11 oveqdr ${⊢}\left({N}\in {ℕ}_{0}\wedge \left({x}\in {\mathrm{Base}}_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}\wedge {y}\in {\mathrm{Base}}_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}\right)\right)\to {x}{\cdot }_{\left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\right)}{y}={x}{\cdot }_{{Y}}{y}$
13 7 8 10 12 crngpropd ${⊢}{N}\in {ℕ}_{0}\to \left({ℤ}_{\mathrm{ring}}{/}_{𝑠}\left({ℤ}_{\mathrm{ring}}{~}_{\mathit{QG}}\mathrm{RSpan}\left({ℤ}_{\mathrm{ring}}\right)\left(\left\{{N}\right\}\right)\right)\in \mathrm{CRing}↔{Y}\in \mathrm{CRing}\right)$
14 6 13 mpbid ${⊢}{N}\in {ℕ}_{0}\to {Y}\in \mathrm{CRing}$