Theorem edomidom

Description: Every Euclidean domain is an integral domain. (Contributed by Thierry Arnoux, 29-Oct-2026)

	Ref	Expression
Hypothesis	edomidom.1	$$⊢\phi \to D\in \mathrm{EDomn}$$
Assertion	edomidom	$$⊢\phi \to D\in \mathrm{IDomn}$$

Proof

Step	Hyp	Ref	Expression
1		edomidom.1	$$⊢\phi \to D\in \mathrm{EDomn}$$
2		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
3		eqid	$$⊢0_D=0_D$$
4		eqid	$$⊢{+}_D={+}_D$$
5		eqid	$$⊢{\cdot }_D={\cdot }_D$$
6		eqid	$$⊢{\mathrm{EuclF}\left(D\right)\upharpoonright }_{\left({\mathrm{Base}}_D\setminus \left\{0_D\right\}\right)}={\mathrm{EuclF}\left(D\right)\upharpoonright }_{\left({\mathrm{Base}}_D\setminus \left\{0_D\right\}\right)}$$
7	2 3 4 5 6	isedom	$$⊢D\in \mathrm{EDomn}\leftrightarrow \left(D\in \mathrm{IDomn}\wedge \left(\left({\mathrm{EuclF}\left(D\right)\upharpoonright }_{\left({\mathrm{Base}}_D\setminus \left\{0_D\right\}\right)}\right):{\mathrm{Base}}_D\setminus \left\{0_D\right\}⟶{\mathbb{N}}_0\wedge \forall x\in {\mathrm{Base}}_D\forall y\in \left({\mathrm{Base}}_D\setminus \left\{0_D\right\}\right)\exists q\in {\mathrm{Base}}_D\exists r\in {\mathrm{Base}}_D\left(x=\left(y{\cdot }_{D}q\right){+}_{D}r\wedge \left(r=0_D\vee \left({\mathrm{EuclF}\left(D\right)\upharpoonright }_{\left({\mathrm{Base}}_D\setminus \left\{0_D\right\}\right)}\right)\left(r\right)<\left({\mathrm{EuclF}\left(D\right)\upharpoonright }_{\left({\mathrm{Base}}_D\setminus \left\{0_D\right\}\right)}\right)\left(y\right)\right)\right)\right)\right)$$
8	7	simplbi	$$⊢D\in \mathrm{EDomn}\to D\in \mathrm{IDomn}$$
9	1 8	syl	$$⊢\phi \to D\in \mathrm{IDomn}$$