Theorem dvdsrzring

Description: Ring divisibility in the ring of integers corresponds to ordinary divisibility in ZZ . (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by AV, 9-Jun-2019)

	Ref	Expression
Assertion	dvdsrzring	|- || = ( ||r ` ZZring )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( x e. ZZ /\ y e. ZZ ) -> x e. ZZ )
2	1	anim1i	|- ( ( ( x e. ZZ /\ y e. ZZ ) /\ E. z e. ZZ ( z x. x ) = y ) -> ( x e. ZZ /\ E. z e. ZZ ( z x. x ) = y ) )
3		simpl	|- ( ( x e. ZZ /\ E. z e. ZZ ( z x. x ) = y ) -> x e. ZZ )
4		zmulcl	|- ( ( z e. ZZ /\ x e. ZZ ) -> ( z x. x ) e. ZZ )
5	4	ancoms	|- ( ( x e. ZZ /\ z e. ZZ ) -> ( z x. x ) e. ZZ )
6		eleq1	|- ( ( z x. x ) = y -> ( ( z x. x ) e. ZZ <-> y e. ZZ ) )
7	5 6	syl5ibcom	|- ( ( x e. ZZ /\ z e. ZZ ) -> ( ( z x. x ) = y -> y e. ZZ ) )
8	7	rexlimdva	|- ( x e. ZZ -> ( E. z e. ZZ ( z x. x ) = y -> y e. ZZ ) )
9	8	imp	|- ( ( x e. ZZ /\ E. z e. ZZ ( z x. x ) = y ) -> y e. ZZ )
10		simpr	|- ( ( x e. ZZ /\ E. z e. ZZ ( z x. x ) = y ) -> E. z e. ZZ ( z x. x ) = y )
11	3 9 10	jca31	|- ( ( x e. ZZ /\ E. z e. ZZ ( z x. x ) = y ) -> ( ( x e. ZZ /\ y e. ZZ ) /\ E. z e. ZZ ( z x. x ) = y ) )
12	2 11	impbii	|- ( ( ( x e. ZZ /\ y e. ZZ ) /\ E. z e. ZZ ( z x. x ) = y ) <-> ( x e. ZZ /\ E. z e. ZZ ( z x. x ) = y ) )
13	12	opabbii	|- { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. z e. ZZ ( z x. x ) = y ) } = { <. x , y >. | ( x e. ZZ /\ E. z e. ZZ ( z x. x ) = y ) }
14		df-dvds	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. z e. ZZ ( z x. x ) = y ) }
15		zringbas	|- ZZ = ( Base ` ZZring )
16		eqid	|- ( ||r ` ZZring ) = ( ||r ` ZZring )
17		zringmulr	|- x. = ( .r ` ZZring )
18	15 16 17	dvdsrval	|- ( ||r ` ZZring ) = { <. x , y >. | ( x e. ZZ /\ E. z e. ZZ ( z x. x ) = y ) }
19	13 14 18	3eqtr4i	|- || = ( ||r ` ZZring )