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 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( bRoU ‘ 3 ) = ( bRoU ‘ 3 )
2	1	bru3sqbru	⊢ ( ( bRoU ‘ 3 ) ↑ 2 ) = ( - 1 − ( bRoU ‘ 3 ) )
3		3nn	⊢ 3 ∈ ℕ
4		brucn	⊢ ( 3 ∈ ℕ → ( bRoU ‘ 3 ) ∈ ℂ )
5	3 4	ax-mp	⊢ ( bRoU ‘ 3 ) ∈ ℂ
6		neg1z	⊢ - 1 ∈ ℤ
7		zellaz	⊢ ( ( ( bRoU ‘ 3 ) ∈ ℂ ∧ - 1 ∈ ℤ ) → - 1 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) )
8	5 6 7	mp2an	⊢ - 1 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) )
9		adcnellaz	⊢ ( ( bRoU ‘ 3 ) ∈ ℂ → ( bRoU ‘ 3 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) )
10	5 9	ax-mp	⊢ ( bRoU ‘ 3 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) )
11	8 10	pm3.2i	⊢ ( - 1 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∧ ( bRoU ‘ 3 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) )
12		eqid	⊢ ( Z[]l ‘ ( bRoU ‘ 3 ) ) = ( Z[]l ‘ ( bRoU ‘ 3 ) )
13	12	lazsubcl	⊢ ( ( bRoU ‘ 3 ) ∈ ℂ → ( ( - 1 ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ∧ ( bRoU ‘ 3 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) → ( - 1 − ( bRoU ‘ 3 ) ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) ) ) )
14	5 11 13	mp2	⊢ ( - 1 − ( bRoU ‘ 3 ) ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) )
15	2 14	eqeltri	⊢ ( ( bRoU ‘ 3 ) ↑ 2 ) ∈ ( Z[]l ‘ ( bRoU ‘ 3 ) )