Metamath Proof Explorer

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 ) ) e. ( SubRing ` CCfld )

Proof

Step Hyp Ref Expression
1 3nn 
 |-  3 e. NN
2 brucn 
 |-  ( 3 e. NN -> ( bRoU ` 3 ) e. CC )
3 1 2 ax-mp 
 |-  ( bRoU ` 3 ) e. CC
4 lazcn 
 |-  ( ( bRoU ` 3 ) e. CC -> ( a e. ( Z[]l ` ( bRoU ` 3 ) ) -> a e. CC ) )
5 3 4 ax-mp 
 |-  ( a e. ( Z[]l ` ( bRoU ` 3 ) ) -> a e. CC )
6 eqid 
 |-  ( Z[]l ` ( bRoU ` 3 ) ) = ( Z[]l ` ( bRoU ` 3 ) )
7 6 lazaddcl 
 |-  ( ( bRoU ` 3 ) e. CC -> ( ( a e. ( Z[]l ` ( bRoU ` 3 ) ) /\ b e. ( Z[]l ` ( bRoU ` 3 ) ) ) -> ( a + b ) e. ( Z[]l ` ( bRoU ` 3 ) ) ) )
8 3 7 ax-mp 
 |-  ( ( a e. ( Z[]l ` ( bRoU ` 3 ) ) /\ b e. ( Z[]l ` ( bRoU ` 3 ) ) ) -> ( a + b ) e. ( Z[]l ` ( bRoU ` 3 ) ) )
9 6 laznegcl 
 |-  ( ( bRoU ` 3 ) e. CC -> ( a e. ( Z[]l ` ( bRoU ` 3 ) ) -> -u a e. ( Z[]l ` ( bRoU ` 3 ) ) ) )
10 3 9 ax-mp 
 |-  ( a e. ( Z[]l ` ( bRoU ` 3 ) ) -> -u a e. ( Z[]l ` ( bRoU ` 3 ) ) )
11 1z 
 |-  1 e. ZZ
12 zellaz 
 |-  ( ( ( bRoU ` 3 ) e. CC /\ 1 e. ZZ ) -> 1 e. ( Z[]l ` ( bRoU ` 3 ) ) )
13 3 11 12 mp2an 
 |-  1 e. ( Z[]l ` ( bRoU ` 3 ) )
14 bru3sqez 
 |-  ( ( bRoU ` 3 ) ^ 2 ) e. ( Z[]l ` ( bRoU ` 3 ) )
15 6 lazmulcl 
 |-  ( ( ( bRoU ` 3 ) e. CC /\ ( ( bRoU ` 3 ) ^ 2 ) e. ( Z[]l ` ( bRoU ` 3 ) ) ) -> ( ( a e. ( Z[]l ` ( bRoU ` 3 ) ) /\ b e. ( Z[]l ` ( bRoU ` 3 ) ) ) -> ( a x. b ) e. ( Z[]l ` ( bRoU ` 3 ) ) ) )
16 3 14 15 mp2an 
 |-  ( ( a e. ( Z[]l ` ( bRoU ` 3 ) ) /\ b e. ( Z[]l ` ( bRoU ` 3 ) ) ) -> ( a x. b ) e. ( Z[]l ` ( bRoU ` 3 ) ) )
17 5 8 10 13 16 cnsubrglem 
 |-  ( Z[]l ` ( bRoU ` 3 ) ) e. ( SubRing ` CCfld )