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	⊢ 𝑆 = ( RSpan ‘ ℤring )
	znval.u	⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
Assertion	zncrng2	⊢ ( 𝑁 ∈ ℤ → 𝑈 ∈ CRing )

Proof

Step	Hyp	Ref	Expression
1		znval.s	⊢ 𝑆 = ( RSpan ‘ ℤring )
2		znval.u	⊢ 𝑈 = ( ℤring /s ( ℤring ~QG ( 𝑆 ‘ { 𝑁 } ) ) )
3		zringcrng	⊢ ℤring ∈ CRing
4	1	znlidl	⊢ ( 𝑁 ∈ ℤ → ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
5		eqid	⊢ ( LIdeal ‘ ℤring ) = ( LIdeal ‘ ℤring )
6	2 5	quscrng	⊢ ( ( ℤring ∈ CRing ∧ ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) ) → 𝑈 ∈ CRing )
7	3 4 6	sylancr	⊢ ( 𝑁 ∈ ℤ → 𝑈 ∈ CRing )