Theorem ezsscn

Description: The Eisenstein integers are a subset of the complex numbers. (Contributed by AV, 26-Oct-2026)

	Ref	Expression
Assertion	ezsscn	|- ( Z[]l ` ( bRoU ` 3 ) ) C_ CC

Proof

Step	Hyp	Ref	Expression
1		ezsubrg	|- ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld )
2		subrgccsscc	|- ( ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld ) -> ( Z[]l ` ( bRoU ` 3 ) ) C_ CC )
3	1 2	ax-mp	|- ( Z[]l ` ( bRoU ` 3 ) ) C_ CC