Definition df-edom

Description: Define Euclidean Domains. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Assertion	df-edom	Could not format assertion : No typesetting found for |- EDomn = { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cedom	Could not format EDomn : No typesetting found for class EDomn with typecode class
1		vd	$$setvard$$
2		cidom	$$class\mathrm{IDomn}$$
3		ceuf	Could not format EuclF : No typesetting found for class EuclF with typecode class
4	1	cv	$$setvard$$
5	4 3	cfv	Could not format ( EuclF ` d ) : No typesetting found for class ( EuclF ` d ) with typecode class
6		ve	$$setvare$$
7		cbs	$$class\mathrm{Base}$$
8	4 7	cfv	$$class{\mathrm{Base}}_d$$
9		vv	$$setvarv$$
10	6	cv	$$setvare$$
11	10	wfun	$$wff\mathrm{Fun}e$$
12	9	cv	$$setvarv$$
13		c0g	$$class{0}_{𝑔}$$
14	4 13	cfv	$$class{0}_d$$
15	14	csn	$$class\left\{0_d\right\}$$
16	12 15	cdif	$$class\left(v\setminus \left\{0_d\right\}\right)$$
17	10 16	cima	$$classe\left[v\setminus \left\{0_d\right\}\right]$$
18		cc0	$$class0$$
19		cico	$$class\left[.\right)$$
20		cpnf	$$class\mathrm{+\infty }$$
21	18 20 19	co	$$class\left[0,\mathrm{+\infty }\right)$$
22	17 21	wss	$$wffe\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)$$
23		va	$$setvara$$
24		vb	$$setvarb$$
25		vq	$$setvarq$$
26		vr	$$setvarr$$
27	23	cv	$$setvara$$
28	24	cv	$$setvarb$$
29		cmulr	$$class{\cdot }_{𝑟}$$
30	4 29	cfv	$$class{\cdot }_d$$
31	25	cv	$$setvarq$$
32	28 31 30	co	$$class\left(b{\cdot }_{d}q\right)$$
33		cplusg	$$class{+}_{𝑔}$$
34	4 33	cfv	$$class{+}_d$$
35	26	cv	$$setvarr$$
36	32 35 34	co	$$class\left(\left(b{\cdot }_{d}q\right){+}_{d}r\right)$$
37	27 36	wceq	$$wffa=\left(b{\cdot }_{d}q\right){+}_{d}r$$
38	35 14	wceq	$$wffr=0_d$$
39	35 10	cfv	$$classe\left(r\right)$$
40		clt	$$class<$$
41	28 10	cfv	$$classe\left(b\right)$$
42	39 41 40	wbr	$$wffe\left(r\right)<e\left(b\right)$$
43	38 42	wo	$$wff\left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)$$
44	37 43	wa	$$wff\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
45	44 26 12	wrex	$$wff\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
46	45 25 12	wrex	$$wff\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
47	46 24 16	wral	$$wff\forall b\in \left(v\setminus \left\{0_d\right\}\right)\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
48	47 23 12	wral	$$wff\forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)$$
49	11 22 48	w3a	$$wff\left(\mathrm{Fun}e\wedge e\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)\wedge \forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)\right)$$
50	49 9 8	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_d/v\underset{\dot{}}{]}\left(\mathrm{Fun}e\wedge e\left[v\setminus \left\{0_d\right\}\right]\subseteq \left[0,\mathrm{+\infty }\right)\wedge \forall a\in v\forall b\in \left(v\setminus \left\{0_d\right\}\right)\exists q\in v\exists r\in v\left(a=\left(b{\cdot }_{d}q\right){+}_{d}r\wedge \left(r=0_d\vee e\left(r\right)<e\left(b\right)\right)\right)\right)$$
51	50 6 5	wsbc	Could not format [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) : No typesetting found for wff [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) with typecode wff
52	51 1 2	crab	Could not format { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) } : No typesetting found for class { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) } with typecode class
53	0 52	wceq	Could not format EDomn = { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) } : No typesetting found for wff EDomn = { d e. IDomn | [. ( EuclF ` d ) / e ]. [. ( Base ` d ) / v ]. ( Fun e /\ ( e " ( v \ { ( 0g ` d ) } ) ) C_ ( 0 [,) +oo ) /\ A. a e. v A. b e. ( v \ { ( 0g ` d ) } ) E. q e. v E. r e. v ( a = ( ( b ( .r ` d ) q ) ( +g ` d ) r ) /\ ( r = ( 0g ` d ) \/ ( e ` r ) < ( e ` b ) ) ) ) } with typecode wff