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	No typesetting found for |- W = ( bRoU ` 3 ) with typecode |-
Assertion	bru3sqbru	$$⊢W^2=-1-W$$

Proof

Step	Hyp	Ref	Expression
1		bru3eq.w	Could not format W = ( bRoU ` 3 ) : No typesetting found for |- W = ( bRoU ` 3 ) with typecode |-
2		ax-1cn	$$⊢1\in ℂ$$
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	1 5	eqeltri	$$⊢W\in ℂ$$
7	2 6	addcomi	$$⊢1+W=W+1$$
8	7	oveq2i	$$⊢W^2+1+W=W^2+W+1$$
9	6	sqcli	$$⊢W^2\in ℂ$$
10	9 6 2	addassi	$$⊢W^2+W+1=W^2+W+1$$
11	1	bru3eq	$$⊢W^2+W+1=0$$
12	8 10 11	3eqtr2i	$$⊢W^2+1+W=0$$
13	2 6	addcli	$$⊢1+W\in ℂ$$
14		addeq0	$$⊢\left(W^2\in ℂ\wedge 1+W\in ℂ\right)\to \left(W^2+1+W=0\leftrightarrow W^2=-\left(1+W\right)\right)$$
15	9 13 14	mp2an	$$⊢W^2+1+W=0\leftrightarrow W^2=-\left(1+W\right)$$
16	12 15	mpbi	$$⊢W^2=-\left(1+W\right)$$
17		negdi2	$$⊢\left(1\in ℂ\wedge W\in ℂ\right)\to -\left(1+W\right)=-1-W$$
18	2 6 17	mp2an	$$⊢-\left(1+W\right)=-1-W$$
19	16 18	eqtri	$$⊢W^2=-1-W$$