Theorem edomediv

Description: Apply a Euclidean division in a Euclidean domain. (Contributed by Thierry Arnoux, 29-Oct-2026)

	Ref	Expression
Hypotheses	edomediv.b	$$⊢B={\mathrm{Base}}_D$$
	edomediv.z	$$⊢\underset{\dot{}}{0}=0_D$$
	edomediv.p	$$⊢\underset{\dot{}}{+}={+}_D$$
	edomediv.m	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	edomediv.e	$$⊢E=\mathrm{EuclF}\left(D\right)$$
	edomediv.d	$$⊢\phi \to D\in \mathrm{EDomn}$$
	edomediv.x	$$⊢\phi \to X\in B$$
	edomediv.y	$$⊢\phi \to Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	edomediv	$$⊢\phi \to \exists q\in B\exists r\in B\left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		edomediv.b	$$⊢B={\mathrm{Base}}_D$$
2		edomediv.z	$$⊢\underset{\dot{}}{0}=0_D$$
3		edomediv.p	$$⊢\underset{\dot{}}{+}={+}_D$$
4		edomediv.m	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
5		edomediv.e	$$⊢E=\mathrm{EuclF}\left(D\right)$$
6		edomediv.d	$$⊢\phi \to D\in \mathrm{EDomn}$$
7		edomediv.x	$$⊢\phi \to X\in B$$
8		edomediv.y	$$⊢\phi \to Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9		eqeq1	$$⊢x=X\to \left(x=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\leftrightarrow X=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\right)$$
10	9	anbi1d	$$⊢x=X\to \left(\left(x=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\leftrightarrow \left(X=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\right)$$
11	10	2rexbidv	$$⊢x=X\to \left(\exists q\in B\exists r\in B\left(x=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\leftrightarrow \exists q\in B\exists r\in B\left(X=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\right)$$
12		oveq1	$$⊢y=Y\to y\underset{\dot{}}{·}q=Y\underset{\dot{}}{·}q$$
13	12	oveq1d	$$⊢y=Y\to \left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r$$
14	13	eqeq2d	$$⊢y=Y\to \left(X=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\leftrightarrow X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\right)$$
15		fveq2	$$⊢y=Y\to \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)=\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)$$
16	15	breq2d	$$⊢y=Y\to \left(\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\leftrightarrow \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)$$
17	16	orbi2d	$$⊢y=Y\to \left(\left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\leftrightarrow \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\right)$$
18	14 17	anbi12d	$$⊢y=Y\to \left(\left(X=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\leftrightarrow \left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\right)\right)$$
19	18	2rexbidv	$$⊢y=Y\to \left(\exists q\in B\exists r\in B\left(X=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\leftrightarrow \exists q\in B\exists r\in B\left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\right)\right)$$
20	5	reseq1i	$$⊢{E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}={\mathrm{EuclF}\left(D\right)\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}$$
21	1 2 3 4 20	isedom	$$⊢D\in \mathrm{EDomn}\leftrightarrow \left(D\in \mathrm{IDomn}\wedge \left(\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right):B\setminus \left\{\underset{\dot{}}{0}\right\}⟶{\mathbb{N}}_0\wedge \forall x\in B\forall y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\exists q\in B\exists r\in B\left(x=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\right)\right)$$
22	6 21	sylib	$$⊢\phi \to \left(D\in \mathrm{IDomn}\wedge \left(\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right):B\setminus \left\{\underset{\dot{}}{0}\right\}⟶{\mathbb{N}}_0\wedge \forall x\in B\forall y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\exists q\in B\exists r\in B\left(x=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\right)\right)$$
23	22	simprrd	$$⊢\phi \to \forall x\in B\forall y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\exists q\in B\exists r\in B\left(x=\left(y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)$$
24	11 19 23 7 8	rspc2dv	$$⊢\phi \to \exists q\in B\exists r\in B\left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\right)$$
25		biort	$$⊢r=\underset{\dot{}}{0}\to \left(r=\underset{\dot{}}{0}\leftrightarrow \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\right)$$
26		biort	$$⊢r=\underset{\dot{}}{0}\to \left(r=\underset{\dot{}}{0}\leftrightarrow \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)$$
27	25 26	bitr3d	$$⊢r=\underset{\dot{}}{0}\to \left(\left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\leftrightarrow \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)$$
28	27	adantl	$$⊢\left(\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\wedge r=\underset{\dot{}}{0}\right)\to \left(\left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\leftrightarrow \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)$$
29		simplr	$$⊢\left(\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\wedge r\ne \underset{\dot{}}{0}\right)\to r\in B$$
30		simpr	$$⊢\left(\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\wedge r\ne \underset{\dot{}}{0}\right)\to r\ne \underset{\dot{}}{0}$$
31	29 30	eldifsnd	$$⊢\left(\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\wedge r\ne \underset{\dot{}}{0}\right)\to r\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
32	31	fvresd	$$⊢\left(\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\wedge r\ne \underset{\dot{}}{0}\right)\to \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)=E\left(r\right)$$
33	8	ad2antrr	$$⊢\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\to Y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
34	33	fvresd	$$⊢\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\to \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)=E\left(Y\right)$$
35	34	adantr	$$⊢\left(\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\wedge r\ne \underset{\dot{}}{0}\right)\to \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)=E\left(Y\right)$$
36	32 35	breq12d	$$⊢\left(\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\wedge r\ne \underset{\dot{}}{0}\right)\to \left(\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\leftrightarrow E\left(r\right)<E\left(Y\right)\right)$$
37	36	orbi2d	$$⊢\left(\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\wedge r\ne \underset{\dot{}}{0}\right)\to \left(\left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\leftrightarrow \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)$$
38	28 37	pm2.61dane	$$⊢\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\to \left(\left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\leftrightarrow \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)$$
39	38	anbi2d	$$⊢\left(\left(\phi \wedge q\in B\right)\wedge r\in B\right)\to \left(\left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\right)\leftrightarrow \left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)\right)$$
40	39	anasss	$$⊢\left(\phi \wedge \left(q\in B\wedge r\in B\right)\right)\to \left(\left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\right)\leftrightarrow \left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)\right)$$
41	40	2rexbidva	$$⊢\phi \to \left(\exists q\in B\exists r\in B\left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(Y\right)\right)\right)\leftrightarrow \exists q\in B\exists r\in B\left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)\right)$$
42	24 41	mpbid	$$⊢\phi \to \exists q\in B\exists r\in B\left(X=\left(Y\underset{\dot{}}{·}q\right)\underset{\dot{}}{+}r\wedge \left(r=\underset{\dot{}}{0}\vee E\left(r\right)<E\left(Y\right)\right)\right)$$