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 = ( RSpan ` ZZring )
	znval.u	|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
Assertion	zncrng2	|- ( N e. ZZ -> U e. CRing )

Proof

Step	Hyp	Ref	Expression
1		znval.s	|- S = ( RSpan ` ZZring )
2		znval.u	|- U = ( ZZring /s ( ZZring ~QG ( S ` { N } ) ) )
3		zringcrng	|- ZZring e. CRing
4	1	znlidl	|- ( N e. ZZ -> ( S ` { N } ) e. ( LIdeal ` ZZring ) )
5		eqid	|- ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
6	2 5	quscrng	|- ( ( ZZring e. CRing /\ ( S ` { N } ) e. ( LIdeal ` ZZring ) ) -> U e. CRing )
7	3 4 6	sylancr	|- ( N e. ZZ -> U e. CRing )