This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )