Theorem zncrng2

Description: The value of the Z/nZ structure. It is defined as the quotient ring ZZ / n ZZ , with an "artificial" ordering added to make it a Toset . (In other words, Z/nZ is aring with anorder , but it is not anordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 12-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znval.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	znval.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
Assertion	zncrng2	$$⊢N\in \mathbb{Z}\to U\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		znval.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		znval.u	$$⊢U={\mathbb{Z}}_{\mathrm{ring}}{/}_{𝑠}\left({\mathbb{Z}}_{\mathrm{ring}}{~}_{\mathit{QG}}S\left(\left\{N\right\}\right)\right)$$
3		zringcrng	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}$$
4	1	znlidl	$$⊢N\in \mathbb{Z}\to S\left(\left\{N\right\}\right)\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
5		eqid	$$⊢\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
6	2 5	quscrng	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{CRing}\wedge S\left(\left\{N\right\}\right)\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\right)\to U\in \mathrm{CRing}$$
7	3 4 6	sylancr	$$⊢N\in \mathbb{Z}\to U\in \mathrm{CRing}$$