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} \in EDomn$

Proof

Step	Hyp	Ref	Expression
1		zzedom.1	$⊢ abs = EuclF (ℤ_{ring})$
2		zringidom	$⊢ ℤ_{ring} \in IDomn$
3		absf	$⊢ abs : ℂ ⟶ ℝ$
4	3	a1i	$⊢ ⊤ \to abs : ℂ ⟶ ℝ$
5		zsscn	$⊢ ℤ \subseteq ℂ$
6		ssdifss	$⊢ ℤ \subseteq ℂ \to ℤ ∖ \{0\} \subseteq ℂ$
7	5 6	mp1i	$⊢ ⊤ \to ℤ ∖ \{0\} \subseteq ℂ$
8	4 7	feqresmpt	$⊢ ⊤ \to {abs ↾}_{(ℤ ∖ \{0\})} = (x \in (ℤ ∖ \{0\}) ⟼ \|x\|)$
9	8	mptru	$⊢ {abs ↾}_{(ℤ ∖ \{0\})} = (x \in (ℤ ∖ \{0\}) ⟼ \|x\|)$
10		eldifi	$⊢ x \in (ℤ ∖ \{0\}) \to x \in ℤ$
11		nn0abscl	$⊢ x \in ℤ \to \|x\| \in ℕ_{0}$
12	10 11	syl	$⊢ x \in (ℤ ∖ \{0\}) \to \|x\| \in ℕ_{0}$
13	9 12	fmpti	$⊢ ({abs ↾}_{(ℤ ∖ \{0\})}) : ℤ ∖ \{0\} ⟶ ℕ_{0}$
14		simpr	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to x = q y + r$
15		simp-5r	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to q \in ℤ$
16	15	zcnd	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to q \in ℂ$
17		difssd	$⊢ x \in ℤ \to ℤ ∖ \{0\} \subseteq ℤ$
18	17	sselda	$⊢ (x \in ℤ \land y \in (ℤ ∖ \{0\})) \to y \in ℤ$
19	18	ad5antr	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to y \in ℤ$
20	19	zcnd	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to y \in ℂ$
21	16 20	mulcomd	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to q y = y q$
22	21	oveq1d	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to q y + r = y q + r$
23	14 22	eqtrd	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to x = y q + r$
24		df-ne	$⊢ r \neq 0 \leftrightarrow \neg r = 0$
25		simpllr	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to r < \|y\|$
26		simp-4r	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to r \in ℤ$
27	26	adantr	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to r \in ℤ$
28		simpr	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to r \neq 0$
29	27 28	eldifsnd	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to r \in (ℤ ∖ \{0\})$
30	29	fvresd	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to ({abs ↾}_{(ℤ ∖ \{0\})}) (r) = \|r\|$
31	26	zred	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to r \in ℝ$
32		simpllr	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to 0 \leq r$
33	31 32	absidd	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to \|r\| = r$
34	33	adantr	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to \|r\| = r$
35	30 34	eqtrd	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to ({abs ↾}_{(ℤ ∖ \{0\})}) (r) = r$
36		simp-7r	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to y \in (ℤ ∖ \{0\})$
37	36	fvresd	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to ({abs ↾}_{(ℤ ∖ \{0\})}) (y) = \|y\|$
38	25 35 37	3brtr4d	$⊢ (((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \land r \neq 0) \to ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y)$
39	38	ex	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to (r \neq 0 \to ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y))$
40	24 39	biimtrrid	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to (\neg r = 0 \to ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y))$
41	40	orrd	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to (r = 0 \lor ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y))$
42	23 41	jca	$⊢ ((((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land 0 \leq r) \land r < \|y\|) \land x = q y + r) \to (x = y q + r \land (r = 0 \lor ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y)))$
43	42	3anasss	$⊢ ((((x \in ℤ \land y \in (ℤ ∖ \{0\})) \land q \in ℤ) \land r \in ℤ) \land (0 \leq r \land r < \|y\| \land x = q y + r)) \to (x = y q + r \land (r = 0 \lor ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y)))$
44		simpl	$⊢ (x \in ℤ \land y \in (ℤ ∖ \{0\})) \to x \in ℤ$
45		simpr	$⊢ (x \in ℤ \land y \in (ℤ ∖ \{0\})) \to y \in (ℤ ∖ \{0\})$
46	45	eldifsnbd	$⊢ (x \in ℤ \land y \in (ℤ ∖ \{0\})) \to y \neq 0$
47		divalg	$⊢ (x \in ℤ \land y \in ℤ \land y \neq 0) \to \exists! r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|y\| \land x = q y + r)$
48		reurex	$⊢ \exists! r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|y\| \land x = q y + r) \to \exists r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|y\| \land x = q y + r)$
49	47 48	syl	$⊢ (x \in ℤ \land y \in ℤ \land y \neq 0) \to \exists r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|y\| \land x = q y + r)$
50	44 18 46 49	syl3anc	$⊢ (x \in ℤ \land y \in (ℤ ∖ \{0\})) \to \exists r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|y\| \land x = q y + r)$
51		rexcom	$⊢ \exists r \in ℤ \exists q \in ℤ (0 \leq r \land r < \|y\| \land x = q y + r) \leftrightarrow \exists q \in ℤ \exists r \in ℤ (0 \leq r \land r < \|y\| \land x = q y + r)$
52	50 51	sylib	$⊢ (x \in ℤ \land y \in (ℤ ∖ \{0\})) \to \exists q \in ℤ \exists r \in ℤ (0 \leq r \land r < \|y\| \land x = q y + r)$
53	43 52	reximddv2	$⊢ (x \in ℤ \land y \in (ℤ ∖ \{0\})) \to \exists q \in ℤ \exists r \in ℤ (x = y q + r \land (r = 0 \lor ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y)))$
54	53	rgen2	$⊢ \forall x \in ℤ \forall y \in (ℤ ∖ \{0\}) \exists q \in ℤ \exists r \in ℤ (x = y q + r \land (r = 0 \lor ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y)))$
55	13 54	pm3.2i	$⊢ (({abs ↾}_{(ℤ ∖ \{0\})}) : ℤ ∖ \{0\} ⟶ ℕ_{0} \land \forall x \in ℤ \forall y \in (ℤ ∖ \{0\}) \exists q \in ℤ \exists r \in ℤ (x = y q + r \land (r = 0 \lor ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y))))$
56		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
57		zring0	$⊢ 0 = 0_{ℤ_{ring}}$
58		zringplusg	$⊢ + = +_{ℤ_{ring}}$
59		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
60	1	reseq1i	$⊢ {abs ↾}_{(ℤ ∖ \{0\})} = {EuclF (ℤ_{ring}) ↾}_{(ℤ ∖ \{0\})}$
61	56 57 58 59 60	isedom	$⊢ ℤ_{ring} \in EDomn \leftrightarrow (ℤ_{ring} \in IDomn \land (({abs ↾}_{(ℤ ∖ \{0\})}) : ℤ ∖ \{0\} ⟶ ℕ_{0} \land \forall x \in ℤ \forall y \in (ℤ ∖ \{0\}) \exists q \in ℤ \exists r \in ℤ (x = y q + r \land (r = 0 \lor ({abs ↾}_{(ℤ ∖ \{0\})}) (r) < ({abs ↾}_{(ℤ ∖ \{0\})}) (y)))))$
62	2 55 61	mpbir2an	$⊢ ℤ_{ring} \in EDomn$

Metamath Proof Explorer

Theorem zzedom

Proof