Theorem ezidom

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

	Ref	Expression
Assertion	ezidom	⊢ ( ℂfld ↾s ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) ∈ IDomn

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ℂfld ↾s ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) = ( ℂfld ↾s ( Z[]l ‘ ( bRoU ‘ 3 ) ) )
2		ezsubrg	⊢ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∈ ( SubRing ‘ ℂfld )
3	1 2	subrgccidom	⊢ ( ℂfld ↾s ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) ∈ IDomn