Theorem ezsscn

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

	Ref	Expression
Assertion	ezsscn	Could not format assertion : No typesetting found for |- ( Z[]l ` ( bRoU ` 3 ) ) C_ CC with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ezsubrg	Could not format ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld ) : No typesetting found for |- ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld ) with typecode |-
2		subrgccsscc	Could not format ( ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld ) -> ( Z[]l ` ( bRoU ` 3 ) ) C_ CC ) : No typesetting found for |- ( ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld ) -> ( Z[]l ` ( bRoU ` 3 ) ) C_ CC ) with typecode |-
3	1 2	ax-mp	Could not format ( Z[]l ` ( bRoU ` 3 ) ) C_ CC : No typesetting found for |- ( Z[]l ` ( bRoU ` 3 ) ) C_ CC with typecode |-