Theorem ezidom

Description: The Eisenstein integers form an integral domain. (Contributed by AV, 26-Oct-2026)

	Ref	Expression
Assertion	ezidom	Could not format assertion : No typesetting found for |- ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) e. IDomn with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	Could not format ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) = ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) : No typesetting found for |- ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) = ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) with typecode |-
2		ezsubrg	Could not format ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld ) : No typesetting found for |- ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld ) with typecode |-
3	1 2	subrgccidom	Could not format ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) e. IDomn : No typesetting found for |- ( CCfld |`s ( Z[]l ` ( bRoU ` 3 ) ) ) e. IDomn with typecode |-