Theorem ezsubrg

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

	Ref	Expression
Assertion	ezsubrg	⊢ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∈ ( SubRing ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		3nn	⊢ 3 ∈ ℕ
2		brucn	⊢ ( 3 ∈ ℕ → ( bRoU ‘ 3 ) ∈ ℂ )
3	1 2	ax-mp	⊢ ( bRoU ‘ 3 ) ∈ ℂ
4		lazcn	⊢ ( ( bRoU ‘ 3 ) ∈ ℂ → ( 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) → 𝑎 ∈ ℂ ) )
5	3 4	ax-mp	⊢ ( 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) → 𝑎 ∈ ℂ )
6		eqid	⊢ ( Z[]l ‘ ( bRoU ‘ 3 ) ) = ( Z[]l ‘ ( bRoU ‘ 3 ) )
7	6	lazaddcl	⊢ ( ( bRoU ‘ 3 ) ∈ ℂ → ( ( 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∧ 𝑏 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) → ( 𝑎 + 𝑏 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) )
8	3 7	ax-mp	⊢ ( ( 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∧ 𝑏 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) → ( 𝑎 + 𝑏 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) )
9	6	laznegcl	⊢ ( ( bRoU ‘ 3 ) ∈ ℂ → ( 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) → - 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) )
10	3 9	ax-mp	⊢ ( 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) → - 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) )
11		1z	⊢ 1 ∈ ℤ
12		zellaz	⊢ ( ( ( bRoU ‘ 3 ) ∈ ℂ ∧ 1 ∈ ℤ ) → 1 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) )
13	3 11 12	mp2an	⊢ 1 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) )
14		bru3sqez	⊢ ( ( bRoU ‘ 3 ) ↑ 2 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) )
15	6	lazmulcl	⊢ ( ( ( bRoU ‘ 3 ) ∈ ℂ ∧ ( ( bRoU ‘ 3 ) ↑ 2 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) → ( ( 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∧ 𝑏 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) → ( 𝑎 · 𝑏 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) )
16	3 14 15	mp2an	⊢ ( ( 𝑎 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∧ 𝑏 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) → ( 𝑎 · 𝑏 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) )
17	5 8 10 13 16	cnsubrglem	⊢ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∈ ( SubRing ‘ ℂfld )