Theorem edomidom

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

	Ref	Expression
Hypothesis	edomidom.1	|- ( ph -> D e. EDomn )
Assertion	edomidom	|- ( ph -> D e. IDomn )

Proof

Step	Hyp	Ref	Expression
1		edomidom.1	|- ( ph -> D e. EDomn )
2		eqid	|- ( Base ` D ) = ( Base ` D )
3		eqid	|- ( 0g ` D ) = ( 0g ` D )
4		eqid	|- ( +g ` D ) = ( +g ` D )
5		eqid	|- ( .r ` D ) = ( .r ` D )
6		eqid	|- ( ( EuclF ` D ) |` ( ( Base ` D ) \ { ( 0g ` D ) } ) ) = ( ( EuclF ` D ) |` ( ( Base ` D ) \ { ( 0g ` D ) } ) )
7	2 3 4 5 6	isedom	|- ( D e. EDomn <-> ( D e. IDomn /\ ( ( ( EuclF ` D ) |` ( ( Base ` D ) \ { ( 0g ` D ) } ) ) : ( ( Base ` D ) \ { ( 0g ` D ) } ) --> NN0 /\ A. x e. ( Base ` D ) A. y e. ( ( Base ` D ) \ { ( 0g ` D ) } ) E. q e. ( Base ` D ) E. r e. ( Base ` D ) ( x = ( ( y ( .r ` D ) q ) ( +g ` D ) r ) /\ ( r = ( 0g ` D ) \/ ( ( ( EuclF ` D ) |` ( ( Base ` D ) \ { ( 0g ` D ) } ) ) ` r ) < ( ( ( EuclF ` D ) |` ( ( Base ` D ) \ { ( 0g ` D ) } ) ) ` y ) ) ) ) ) )
8	7	simplbi	|- ( D e. EDomn -> D e. IDomn )
9	1 8	syl	|- ( ph -> D e. IDomn )