Metamath Proof Explorer

Theorem zzedom

Description: The ring of integers is a Euclidean domain. Note that the hypothesis abs = ( EuclFZZring ) could be dropped if the definition of CCfld is adapted. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypothesis zzedom.1 
|- abs = ( EuclF ` ZZring )
Assertion zzedom 
|- ZZring e. EDomn

Proof

Step Hyp Ref Expression
1 zzedom.1 
 |-  abs = ( EuclF ` ZZring )
2 zringidom 
 |-  ZZring e. IDomn
3 absf 
 |-  abs : CC --> RR
4 3 a1i 
 |-  ( T. -> abs : CC --> RR )
5 zsscn 
 |-  ZZ C_ CC
6 ssdifss 
 |-  ( ZZ C_ CC -> ( ZZ \ { 0 } ) C_ CC )
7 5 6 mp1i 
 |-  ( T. -> ( ZZ \ { 0 } ) C_ CC )
8 4 7 feqresmpt 
 |-  ( T. -> ( abs |` ( ZZ \ { 0 } ) ) = ( x e. ( ZZ \ { 0 } ) |-> ( abs ` x ) ) )
9 8 mptru 
 |-  ( abs |` ( ZZ \ { 0 } ) ) = ( x e. ( ZZ \ { 0 } ) |-> ( abs ` x ) )
10 eldifi 
 |-  ( x e. ( ZZ \ { 0 } ) -> x e. ZZ )
11 nn0abscl 
 |-  ( x e. ZZ -> ( abs ` x ) e. NN0 )
12 10 11 syl 
 |-  ( x e. ( ZZ \ { 0 } ) -> ( abs ` x ) e. NN0 )
13 9 12 fmpti 
 |-  ( abs |` ( ZZ \ { 0 } ) ) : ( ZZ \ { 0 } ) --> NN0
14 simpr 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> x = ( ( q x. y ) + r ) )
15 simp-5r 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> q e. ZZ )
16 15 zcnd 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> q e. CC )
17 difssd 
 |-  ( x e. ZZ -> ( ZZ \ { 0 } ) C_ ZZ )
18 17 sselda 
 |-  ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) -> y e. ZZ )
19 18 ad5antr 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> y e. ZZ )
20 19 zcnd 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> y e. CC )
21 16 20 mulcomd 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> ( q x. y ) = ( y x. q ) )
22 21 oveq1d 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> ( ( q x. y ) + r ) = ( ( y x. q ) + r ) )
23 14 22 eqtrd 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> x = ( ( y x. q ) + r ) )
24 df-ne 
 |-  ( r =/= 0 <-> -. r = 0 )
25 simpllr 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> r < ( abs ` y ) )
26 simp-4r 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> r e. ZZ )
27 26 adantr 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> r e. ZZ )
28 simpr 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> r =/= 0 )
29 27 28 eldifsnd 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> r e. ( ZZ \ { 0 } ) )
30 29 fvresd 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) = ( abs ` r ) )
31 26 zred 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> r e. RR )
32 simpllr 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> 0 <_ r )
33 31 32 absidd 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> ( abs ` r ) = r )
34 33 adantr 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> ( abs ` r ) = r )
35 30 34 eqtrd 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) = r )
36 simp-7r 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> y e. ( ZZ \ { 0 } ) )
37 36 fvresd 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) = ( abs ` y ) )
38 25 35 37 3brtr4d 
 |-  ( ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) /\ r =/= 0 ) -> ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) )
39 38 ex 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> ( r =/= 0 -> ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) ) )
40 24 39 biimtrrid 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> ( -. r = 0 -> ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) ) )
41 40 orrd 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> ( r = 0 \/ ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) ) )
42 23 41 jca 
 |-  ( ( ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ 0 <_ r ) /\ r < ( abs ` y ) ) /\ x = ( ( q x. y ) + r ) ) -> ( x = ( ( y x. q ) + r ) /\ ( r = 0 \/ ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) ) ) )
43 42 3anasss 
 |-  ( ( ( ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) /\ q e. ZZ ) /\ r e. ZZ ) /\ ( 0 <_ r /\ r < ( abs ` y ) /\ x = ( ( q x. y ) + r ) ) ) -> ( x = ( ( y x. q ) + r ) /\ ( r = 0 \/ ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) ) ) )
44 simpl 
 |-  ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) -> x e. ZZ )
45 simpr 
 |-  ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) -> y e. ( ZZ \ { 0 } ) )
46 45 eldifsnbd 
 |-  ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) -> y =/= 0 )
47 divalg 
 |-  ( ( x e. ZZ /\ y e. ZZ /\ y =/= 0 ) -> E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` y ) /\ x = ( ( q x. y ) + r ) ) )
48 reurex 
 |-  ( E! r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` y ) /\ x = ( ( q x. y ) + r ) ) -> E. r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` y ) /\ x = ( ( q x. y ) + r ) ) )
49 47 48 syl 
 |-  ( ( x e. ZZ /\ y e. ZZ /\ y =/= 0 ) -> E. r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` y ) /\ x = ( ( q x. y ) + r ) ) )
50 44 18 46 49 syl3anc 
 |-  ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) -> E. r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` y ) /\ x = ( ( q x. y ) + r ) ) )
51 rexcom 
 |-  ( E. r e. ZZ E. q e. ZZ ( 0 <_ r /\ r < ( abs ` y ) /\ x = ( ( q x. y ) + r ) ) <-> E. q e. ZZ E. r e. ZZ ( 0 <_ r /\ r < ( abs ` y ) /\ x = ( ( q x. y ) + r ) ) )
52 50 51 sylib 
 |-  ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) -> E. q e. ZZ E. r e. ZZ ( 0 <_ r /\ r < ( abs ` y ) /\ x = ( ( q x. y ) + r ) ) )
53 43 52 reximddv2 
 |-  ( ( x e. ZZ /\ y e. ( ZZ \ { 0 } ) ) -> E. q e. ZZ E. r e. ZZ ( x = ( ( y x. q ) + r ) /\ ( r = 0 \/ ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) ) ) )
54 53 rgen2 
 |-  A. x e. ZZ A. y e. ( ZZ \ { 0 } ) E. q e. ZZ E. r e. ZZ ( x = ( ( y x. q ) + r ) /\ ( r = 0 \/ ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) ) )
55 13 54 pm3.2i 
 |-  ( ( abs |` ( ZZ \ { 0 } ) ) : ( ZZ \ { 0 } ) --> NN0 /\ A. x e. ZZ A. y e. ( ZZ \ { 0 } ) E. q e. ZZ E. r e. ZZ ( x = ( ( y x. q ) + r ) /\ ( r = 0 \/ ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) ) ) )
56 zringbas 
 |-  ZZ = ( Base ` ZZring )
57 zring0 
 |-  0 = ( 0g ` ZZring )
58 zringplusg 
 |-  + = ( +g ` ZZring )
59 zringmulr 
 |-  x. = ( .r ` ZZring )
60 1 reseq1i 
 |-  ( abs |` ( ZZ \ { 0 } ) ) = ( ( EuclF ` ZZring ) |` ( ZZ \ { 0 } ) )
61 56 57 58 59 60 isedom 
 |-  ( ZZring e. EDomn <-> ( ZZring e. IDomn /\ ( ( abs |` ( ZZ \ { 0 } ) ) : ( ZZ \ { 0 } ) --> NN0 /\ A. x e. ZZ A. y e. ( ZZ \ { 0 } ) E. q e. ZZ E. r e. ZZ ( x = ( ( y x. q ) + r ) /\ ( r = 0 \/ ( ( abs |` ( ZZ \ { 0 } ) ) ` r ) < ( ( abs |` ( ZZ \ { 0 } ) ) ` y ) ) ) ) ) )
62 2 55 61 mpbir2an 
 |-  ZZring e. EDomn