Theorem bru3eq

Description: The basic 3rd root of unity _om satisfies the equation _om ^ 2 + _om + 1 = 0 . (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Hypothesis	bru3eq.w	No typesetting found for |- W = ( bRoU ` 3 ) with typecode |-
Assertion	bru3eq	$$⊢W^2+W+1=0$$

Proof

Step	Hyp	Ref	Expression
1		bru3eq.w	Could not format W = ( bRoU ` 3 ) : No typesetting found for |- W = ( bRoU ` 3 ) with typecode |-
2	1	bru3sq	$$⊢W^2=\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
3	1	bru3val	$$⊢W=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$
4	2 3	oveq12i	$$⊢W^2+W=\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)+\left(\frac{-1+\mathrm{i}\sqrt{3}}{2}\right)$$
5	4	oveq1i	$$⊢W^2+W+1=\left(\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)\right)+\left(\frac{-1+\mathrm{i}\sqrt{3}}{2}\right)+1$$
6		ax-1cn	$$⊢1\in ℂ$$
7		2cn	$$⊢2\in ℂ$$
8		2ne0	$$⊢2\ne 0$$
9		divneg	$$⊢\left(1\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to -\frac{1}{2}=\frac{-1}{2}$$
10	6 7 8 9	mp3an	$$⊢-\frac{1}{2}=\frac{-1}{2}$$
11	10	oveq2i	$$⊢2\left(-\frac{1}{2}\right)=2\left(\frac{-1}{2}\right)$$
12		halfcn	$$⊢\frac{1}{2}\in ℂ$$
13	7 12	mulneg2i	$$⊢2\left(-\frac{1}{2}\right)=-2\left(\frac{1}{2}\right)$$
14		2thalfe1	$$⊢2\left(\frac{1}{2}\right)=1$$
15	14	negeqi	$$⊢-2\left(\frac{1}{2}\right)=-1$$
16	13 15	eqtri	$$⊢2\left(-\frac{1}{2}\right)=-1$$
17		neg1cn	$$⊢-1\in ℂ$$
18	17 7 8	divcli	$$⊢\frac{-1}{2}\in ℂ$$
19	18	2timesi	$$⊢2\left(\frac{-1}{2}\right)=\left(\frac{-1}{2}\right)+\left(\frac{-1}{2}\right)$$
20	11 16 19	3eqtr3ri	$$⊢\left(\frac{-1}{2}\right)+\left(\frac{-1}{2}\right)=-1$$
21	20	oveq1i	$$⊢\left(\frac{-1}{2}\right)+\left(\frac{-1}{2}\right)+1=-1+1$$
22		ax-icn	$$⊢\mathrm{i}\in ℂ$$
23		3re	$$⊢3\in ℝ$$
24		3pos	$$⊢0<3$$
25	23 24	sqrtpclii	$$⊢\sqrt{3}\in ℝ$$
26	25	recni	$$⊢\sqrt{3}\in ℂ$$
27	22 26	mulcli	$$⊢\mathrm{i}\sqrt{3}\in ℂ$$
28	17 27 7 8	divdiri	$$⊢\frac{-1+\mathrm{i}\sqrt{3}}{2}=\left(\frac{-1}{2}\right)+\left(\frac{\mathrm{i}\sqrt{3}}{2}\right)$$
29	22 26 7 8	divassi	$$⊢\frac{\mathrm{i}\sqrt{3}}{2}=\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
30	29	oveq2i	$$⊢\left(\frac{-1}{2}\right)+\left(\frac{\mathrm{i}\sqrt{3}}{2}\right)=\left(\frac{-1}{2}\right)+\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
31	28 30	eqtri	$$⊢\frac{-1+\mathrm{i}\sqrt{3}}{2}=\left(\frac{-1}{2}\right)+\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
32	31	oveq2i	$$⊢\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)+\left(\frac{-1+\mathrm{i}\sqrt{3}}{2}\right)=\left(\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)\right)+\left(\frac{-1}{2}\right)+\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
33	26 7 8	divcli	$$⊢\frac{\sqrt{3}}{2}\in ℂ$$
34	22 33	mulcli	$$⊢\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)\in ℂ$$
35		nppcan3	$$⊢\left(\frac{-1}{2}\in ℂ\wedge \mathrm{i}\left(\frac{\sqrt{3}}{2}\right)\in ℂ\wedge \frac{-1}{2}\in ℂ\right)\to \left(\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)\right)+\left(\frac{-1}{2}\right)+\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)=\left(\frac{-1}{2}\right)+\left(\frac{-1}{2}\right)$$
36	18 34 18 35	mp3an	$$⊢\left(\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)\right)+\left(\frac{-1}{2}\right)+\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)=\left(\frac{-1}{2}\right)+\left(\frac{-1}{2}\right)$$
37	32 36	eqtri	$$⊢\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)+\left(\frac{-1+\mathrm{i}\sqrt{3}}{2}\right)=\left(\frac{-1}{2}\right)+\left(\frac{-1}{2}\right)$$
38	37	oveq1i	$$⊢\left(\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)\right)+\left(\frac{-1+\mathrm{i}\sqrt{3}}{2}\right)+1=\left(\frac{-1}{2}\right)+\left(\frac{-1}{2}\right)+1$$
39	6 6	negsubdii	$$⊢-\left(1-1\right)=-1+1$$
40	21 38 39	3eqtr4i	$$⊢\left(\left(\frac{-1}{2}\right)-\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)\right)+\left(\frac{-1+\mathrm{i}\sqrt{3}}{2}\right)+1=-\left(1-1\right)$$
41		1m1e0	$$⊢1-1=0$$
42	41	negeqi	$$⊢-\left(1-1\right)=-0$$
43		neg0	$$⊢-0=0$$
44	42 43	eqtri	$$⊢-\left(1-1\right)=0$$
45	5 40 44	3eqtri	$$⊢W^2+W+1=0$$