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 ‘ ℤring )
Assertion zzedom ℤring ∈ EDomn

Proof

Step Hyp Ref Expression
1 zzedom.1 ⊢ abs = ( EuclF ‘ ℤring )
2 zringidom ⊢ ℤring ∈ IDomn
3 absf ⊢ abs : ℂ ⟶ ℝ
4 3 a1i ⊢ ( ⊤ → abs : ℂ ⟶ ℝ )
5 zsscn ⊢ ℤ ⊆ ℂ
6 ssdifss ⊢ ( ℤ ⊆ ℂ → ( ℤ ∖ { 0 } ) ⊆ ℂ )
7 5 6 mp1i ⊢ ( ⊤ → ( ℤ ∖ { 0 } ) ⊆ ℂ )
8 4 7 feqresmpt ⊢ ( ⊤ → ( abs ↾ ( ℤ ∖ { 0 } ) ) = ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ↦ ( abs ‘ 𝑥 ) ) )
9 8 mptru ⊢ ( abs ↾ ( ℤ ∖ { 0 } ) ) = ( 𝑥 ∈ ( ℤ ∖ { 0 } ) ↦ ( abs ‘ 𝑥 ) )
10 eldifi ⊢ ( 𝑥 ∈ ( ℤ ∖ { 0 } ) → 𝑥 ∈ ℤ )
11 nn0abscl ⊢ ( 𝑥 ∈ ℤ → ( abs ‘ 𝑥 ) ∈ ℕ0 )
12 10 11 syl ⊢ ( 𝑥 ∈ ( ℤ ∖ { 0 } ) → ( abs ‘ 𝑥 ) ∈ ℕ0 )
13 9 12 fmpti ⊢ ( abs ↾ ( ℤ ∖ { 0 } ) ) : ( ℤ ∖ { 0 } ) ⟶ ℕ0
14 simpr ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) )
15 simp-5r ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → 𝑞 ∈ ℤ )
16 15 zcnd ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → 𝑞 ∈ ℂ )
17 difssd ⊢ ( 𝑥 ∈ ℤ → ( ℤ ∖ { 0 } ) ⊆ ℤ )
18 17 sselda ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) → 𝑦 ∈ ℤ )
19 18 ad5antr ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → 𝑦 ∈ ℤ )
20 19 zcnd ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → 𝑦 ∈ ℂ )
21 16 20 mulcomd ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → ( 𝑞 · 𝑦 ) = ( 𝑦 · 𝑞 ) )
22 21 oveq1d ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → ( ( 𝑞 · 𝑦 ) + 𝑟 ) = ( ( 𝑦 · 𝑞 ) + 𝑟 ) )
23 14 22 eqtrd ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) )
24 df-ne ⊢ ( 𝑟 ≠ 0 ↔ ¬ 𝑟 = 0 )
25 simpllr ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 < ( abs ‘ 𝑦 ) )
26 simp-4r ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → 𝑟 ∈ ℤ )
27 26 adantr ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ ℤ )
28 simpr ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 ≠ 0 )
29 27 28 eldifsnd ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ ( ℤ ∖ { 0 } ) )
30 29 fvresd ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) = ( abs ‘ 𝑟 ) )
31 26 zred ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → 𝑟 ∈ ℝ )
32 simpllr ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → 0 ≤ 𝑟 )
33 31 32 absidd ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → ( abs ‘ 𝑟 ) = 𝑟 )
34 33 adantr ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( abs ‘ 𝑟 ) = 𝑟 )
35 30 34 eqtrd ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) = 𝑟 )
36 simp-7r ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → 𝑦 ∈ ( ℤ ∖ { 0 } ) )
37 36 fvresd ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) = ( abs ‘ 𝑦 ) )
38 25 35 37 3brtr4d ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ∧ 𝑟 ≠ 0 ) → ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) )
39 38 ex ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → ( 𝑟 ≠ 0 → ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) ) )
40 24 39 biimtrrid ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → ( ¬ 𝑟 = 0 → ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) ) )
41 40 orrd ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → ( 𝑟 = 0 ∨ ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) ) )
42 23 41 jca ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ 0 ≤ 𝑟 ) ∧ 𝑟 < ( abs ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
43 42 3anasss ⊢ ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) ∧ 𝑞 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) ∧ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝑦 ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ) → ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
44 simpl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) → 𝑥 ∈ ℤ )
45 simpr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) → 𝑦 ∈ ( ℤ ∖ { 0 } ) )
46 45 eldifsnbd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) → 𝑦 ≠ 0 )
47 divalg ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) → ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝑦 ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) )
48 reurex ⊢ ( ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝑦 ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) → ∃ 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝑦 ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) )
49 47 48 syl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) → ∃ 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝑦 ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) )
50 44 18 46 49 syl3anc ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) → ∃ 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝑦 ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) )
51 rexcom ⊢ ( ∃ 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝑦 ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) ↔ ∃ 𝑞 ∈ ℤ ∃ 𝑟 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝑦 ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) )
52 50 51 sylib ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) → ∃ 𝑞 ∈ ℤ ∃ 𝑟 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝑦 ) ∧ 𝑥 = ( ( 𝑞 · 𝑦 ) + 𝑟 ) ) )
53 43 52 reximddv2 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( ℤ ∖ { 0 } ) ) → ∃ 𝑞 ∈ ℤ ∃ 𝑟 ∈ ℤ ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
54 53 rgen2 ⊢ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ( ℤ ∖ { 0 } ) ∃ 𝑞 ∈ ℤ ∃ 𝑟 ∈ ℤ ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) ) )
55 13 54 pm3.2i ⊢ ( ( abs ↾ ( ℤ ∖ { 0 } ) ) : ( ℤ ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ( ℤ ∖ { 0 } ) ∃ 𝑞 ∈ ℤ ∃ 𝑟 ∈ ℤ ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
56 zringbas ⊢ ℤ = ( Base ‘ ℤring )
57 zring0 ⊢ 0 = ( 0g ‘ ℤring )
58 zringplusg ⊢ + = ( +g ‘ ℤring )
59 zringmulr ⊢ · = ( .r ‘ ℤring )
60 1 reseq1i ⊢ ( abs ↾ ( ℤ ∖ { 0 } ) ) = ( ( EuclF ‘ ℤring ) ↾ ( ℤ ∖ { 0 } ) )
61 56 57 58 59 60 isedom ⊢ ( ℤring ∈ EDomn ↔ ( ℤring ∈ IDomn ∧ ( ( abs ↾ ( ℤ ∖ { 0 } ) ) : ( ℤ ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ( ℤ ∖ { 0 } ) ∃ 𝑞 ∈ ℤ ∃ 𝑟 ∈ ℤ ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( abs ↾ ( ℤ ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) ) )
62 2 55 61 mpbir2an ⊢ ℤring ∈ EDomn