Theorem zncrng2

Description: Making a commutative ring as a quotient of ZZ and n ZZ . (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 )