Metamath Proof Explorer

Theorem bru3sqez

Description: The square of the basic 3rd root of unity is an Eisenstein integer. (Contributed by AV, 26-Oct-2026)

Ref Expression
Assertion bru3sqez 
|- ( ( bRoU ` 3 ) ^ 2 ) e. ( Z[]l ` ( bRoU ` 3 ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( bRoU ` 3 ) = ( bRoU ` 3 )
2 1 bru3sqbru 
 |-  ( ( bRoU ` 3 ) ^ 2 ) = ( -u 1 - ( bRoU ` 3 ) )
3 3nn 
 |-  3 e. NN
4 brucn 
 |-  ( 3 e. NN -> ( bRoU ` 3 ) e. CC )
5 3 4 ax-mp 
 |-  ( bRoU ` 3 ) e. CC
6 neg1z 
 |-  -u 1 e. ZZ
7 zellaz 
 |-  ( ( ( bRoU ` 3 ) e. CC /\ -u 1 e. ZZ ) -> -u 1 e. ( Z[]l ` ( bRoU ` 3 ) ) )
8 5 6 7 mp2an 
 |-  -u 1 e. ( Z[]l ` ( bRoU ` 3 ) )
9 adcnellaz 
 |-  ( ( bRoU ` 3 ) e. CC -> ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) ) )
10 5 9 ax-mp 
 |-  ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) )
11 8 10 pm3.2i 
 |-  ( -u 1 e. ( Z[]l ` ( bRoU ` 3 ) ) /\ ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) ) )
12 eqid 
 |-  ( Z[]l ` ( bRoU ` 3 ) ) = ( Z[]l ` ( bRoU ` 3 ) )
13 12 lazsubcl 
 |-  ( ( bRoU ` 3 ) e. CC -> ( ( -u 1 e. ( Z[]l ` ( bRoU ` 3 ) ) /\ ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) ) ) -> ( -u 1 - ( bRoU ` 3 ) ) e. ( Z[]l ` ( bRoU ` 3 ) ) ) )
14 5 11 13 mp2 
 |-  ( -u 1 - ( bRoU ` 3 ) ) e. ( Z[]l ` ( bRoU ` 3 ) )
15 2 14 eqeltri 
 |-  ( ( bRoU ` 3 ) ^ 2 ) e. ( Z[]l ` ( bRoU ` 3 ) )