Theorem bru3sqbru

Description: The square of the basic 3rd root of unity expressed by the basic 3rd root of unity. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Hypothesis	bru3eq.w	⊢ 𝑊 = ( bRoU ‘ 3 )
Assertion	bru3sqbru	⊢ ( 𝑊 ↑ 2 ) = ( - 1 − 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		bru3eq.w	⊢ 𝑊 = ( bRoU ‘ 3 )
2		ax-1cn	⊢ 1 ∈ ℂ
3		3nn	⊢ 3 ∈ ℕ
4		brucn	⊢ ( 3 ∈ ℕ → ( bRoU ‘ 3 ) ∈ ℂ )
5	3 4	ax-mp	⊢ ( bRoU ‘ 3 ) ∈ ℂ
6	1 5	eqeltri	⊢ 𝑊 ∈ ℂ
7	2 6	addcomi	⊢ ( 1 + 𝑊 ) = ( 𝑊 + 1 )
8	7	oveq2i	⊢ ( ( 𝑊 ↑ 2 ) + ( 1 + 𝑊 ) ) = ( ( 𝑊 ↑ 2 ) + ( 𝑊 + 1 ) )
9	6	sqcli	⊢ ( 𝑊 ↑ 2 ) ∈ ℂ
10	9 6 2	addassi	⊢ ( ( ( 𝑊 ↑ 2 ) + 𝑊 ) + 1 ) = ( ( 𝑊 ↑ 2 ) + ( 𝑊 + 1 ) )
11	1	bru3eq	⊢ ( ( ( 𝑊 ↑ 2 ) + 𝑊 ) + 1 ) = 0
12	8 10 11	3eqtr2i	⊢ ( ( 𝑊 ↑ 2 ) + ( 1 + 𝑊 ) ) = 0
13	2 6	addcli	⊢ ( 1 + 𝑊 ) ∈ ℂ
14		addeq0	⊢ ( ( ( 𝑊 ↑ 2 ) ∈ ℂ ∧ ( 1 + 𝑊 ) ∈ ℂ ) → ( ( ( 𝑊 ↑ 2 ) + ( 1 + 𝑊 ) ) = 0 ↔ ( 𝑊 ↑ 2 ) = - ( 1 + 𝑊 ) ) )
15	9 13 14	mp2an	⊢ ( ( ( 𝑊 ↑ 2 ) + ( 1 + 𝑊 ) ) = 0 ↔ ( 𝑊 ↑ 2 ) = - ( 1 + 𝑊 ) )
16	12 15	mpbi	⊢ ( 𝑊 ↑ 2 ) = - ( 1 + 𝑊 )
17		negdi2	⊢ ( ( 1 ∈ ℂ ∧ 𝑊 ∈ ℂ ) → - ( 1 + 𝑊 ) = ( - 1 − 𝑊 ) )
18	2 6 17	mp2an	⊢ - ( 1 + 𝑊 ) = ( - 1 − 𝑊 )
19	16 18	eqtri	⊢ ( 𝑊 ↑ 2 ) = ( - 1 − 𝑊 )