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 ) ) ⊆ ℂ

Proof

Step	Hyp	Ref	Expression
1		ezsubrg	⊢ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∈ ( SubRing ‘ ℂfld )
2		subrgccsscc	⊢ ( ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∈ ( SubRing ‘ ℂfld ) → ( Z[]l ‘ ( bRoU ‘ 3 ) ) ⊆ ℂ )
3	1 2	ax-mp	⊢ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ⊆ ℂ