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	Could not format assertion : No typesetting found for |- ( ( bRoU ` 3 ) ^ 2 ) e. ( Z[]l ` ( bRoU ` 3 ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqid	Could not format ( bRoU ` 3 ) = ( bRoU ` 3 ) : No typesetting found for |- ( bRoU ` 3 ) = ( bRoU ` 3 ) with typecode |-
2	1	bru3sqbru	Could not format ( ( bRoU ` 3 ) ^ 2 ) = ( -u 1 - ( bRoU ` 3 ) ) : No typesetting found for |- ( ( bRoU ` 3 ) ^ 2 ) = ( -u 1 - ( bRoU ` 3 ) ) with typecode |-
3		3nn	$$⊢3\in \mathbb{N}$$
4		brucn	Could not format ( 3 e. NN -> ( bRoU ` 3 ) e. CC ) : No typesetting found for |- ( 3 e. NN -> ( bRoU ` 3 ) e. CC ) with typecode |-
5	3 4	ax-mp	Could not format ( bRoU ` 3 ) e. CC : No typesetting found for |- ( bRoU ` 3 ) e. CC with typecode |-
6		neg1z	$$⊢-1\in \mathbb{Z}$$
7		zellaz	Could not format ( ( ( bRoU ` 3 ) e. CC /\ -u 1 e. ZZ ) -> -u 1 e. ( Z[]l ` ( bRoU ` 3 ) ) ) : No typesetting found for |- ( ( ( bRoU ` 3 ) e. CC /\ -u 1 e. ZZ ) -> -u 1 e. ( Z[]l ` ( bRoU ` 3 ) ) ) with typecode |-
8	5 6 7	mp2an	Could not format -u 1 e. ( Z[]l ` ( bRoU ` 3 ) ) : No typesetting found for |- -u 1 e. ( Z[]l ` ( bRoU ` 3 ) ) with typecode |-
9		adcnellaz	Could not format ( ( bRoU ` 3 ) e. CC -> ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) ) ) : No typesetting found for |- ( ( bRoU ` 3 ) e. CC -> ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) ) ) with typecode |-
10	5 9	ax-mp	Could not format ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) ) : No typesetting found for |- ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) ) with typecode |-
11	8 10	pm3.2i	Could not format ( -u 1 e. ( Z[]l ` ( bRoU ` 3 ) ) /\ ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) ) ) : No typesetting found for |- ( -u 1 e. ( Z[]l ` ( bRoU ` 3 ) ) /\ ( bRoU ` 3 ) e. ( Z[]l ` ( bRoU ` 3 ) ) ) with typecode |-
12		eqid	Could not format ( Z[]l ` ( bRoU ` 3 ) ) = ( Z[]l ` ( bRoU ` 3 ) ) : No typesetting found for |- ( Z[]l ` ( bRoU ` 3 ) ) = ( Z[]l ` ( bRoU ` 3 ) ) with typecode |-
13	12	lazsubcl	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
14	5 11 13	mp2	Could not format ( -u 1 - ( bRoU ` 3 ) ) e. ( Z[]l ` ( bRoU ` 3 ) ) : No typesetting found for |- ( -u 1 - ( bRoU ` 3 ) ) e. ( Z[]l ` ( bRoU ` 3 ) ) with typecode |-
15	2 14	eqeltri	Could not format ( ( bRoU ` 3 ) ^ 2 ) e. ( Z[]l ` ( bRoU ` 3 ) ) : No typesetting found for |- ( ( bRoU ` 3 ) ^ 2 ) e. ( Z[]l ` ( bRoU ` 3 ) ) with typecode |-