Theorem bru3val

Description: An alternate way to express 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	bru3val	$$⊢W=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$

Proof

Step	Hyp	Ref	Expression
1		bru3eq.w	Could not format W = ( bRoU ` 3 ) : No typesetting found for |- W = ( bRoU ` 3 ) with typecode |-
2		3nn	$$⊢3\in \mathbb{N}$$
3		bruval3	Could not format ( 3 e. NN -> ( bRoU ` 3 ) = ( ( cos ` ( ( 2 x. _pi ) / 3 ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / 3 ) ) ) ) ) : No typesetting found for |- ( 3 e. NN -> ( bRoU ` 3 ) = ( ( cos ` ( ( 2 x. _pi ) / 3 ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / 3 ) ) ) ) ) with typecode |-
4	2 3	ax-mp	Could not format ( bRoU ` 3 ) = ( ( cos ` ( ( 2 x. _pi ) / 3 ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / 3 ) ) ) ) : No typesetting found for |- ( bRoU ` 3 ) = ( ( cos ` ( ( 2 x. _pi ) / 3 ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / 3 ) ) ) ) with typecode |-
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6		3re	$$⊢3\in ℝ$$
7		3pos	$$⊢0<3$$
8	6 7	sqrtpclii	$$⊢\sqrt{3}\in ℝ$$
9	8	recni	$$⊢\sqrt{3}\in ℂ$$
10		2cn	$$⊢2\in ℂ$$
11		2ne0	$$⊢2\ne 0$$
12	5 9 10 11	divassi	$$⊢\frac{\mathrm{i}\sqrt{3}}{2}=\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
13	12	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)$$
14		neg1cn	$$⊢-1\in ℂ$$
15	5 9	mulcli	$$⊢\mathrm{i}\sqrt{3}\in ℂ$$
16	14 15 10 11	divdiri	$$⊢\frac{-1+\mathrm{i}\sqrt{3}}{2}=\left(\frac{-1}{2}\right)+\left(\frac{\mathrm{i}\sqrt{3}}{2}\right)$$
17		picn	$$⊢\mathrm{\pi }\in ℂ$$
18		3cn	$$⊢3\in ℂ$$
19		3ne0	$$⊢3\ne 0$$
20	10 17 18 19	divassi	$$⊢\frac{2\mathrm{\pi }}{3}=2\left(\frac{\mathrm{\pi }}{3}\right)$$
21	20	fveq2i	$$⊢\cos \left(\frac{2\mathrm{\pi }}{3}\right)=\cos 2\left(\frac{\mathrm{\pi }}{3}\right)$$
22	17 18 19	divcli	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ$$
23		cos2t	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ\to \cos 2\left(\frac{\mathrm{\pi }}{3}\right)=2{\cos \left(\frac{\mathrm{\pi }}{3}\right)}^2-1$$
24	22 23	ax-mp	$$⊢\cos 2\left(\frac{\mathrm{\pi }}{3}\right)=2{\cos \left(\frac{\mathrm{\pi }}{3}\right)}^2-1$$
25		sincos3rdpi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}\right)$$
26	25	simpri	$$⊢\cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}$$
27	26	oveq1i	$$⊢{\cos \left(\frac{\mathrm{\pi }}{3}\right)}^2={\left(\frac{1}{2}\right)}^2$$
28	10 11	sqrecii	$$⊢{\left(\frac{1}{2}\right)}^2=\frac{1}{2^2}$$
29	27 28	eqtri	$$⊢{\cos \left(\frac{\mathrm{\pi }}{3}\right)}^2=\frac{1}{2^2}$$
30	29	oveq2i	$$⊢2{\cos \left(\frac{\mathrm{\pi }}{3}\right)}^2=2\left(\frac{1}{2^2}\right)$$
31	30	oveq1i	$$⊢2{\cos \left(\frac{\mathrm{\pi }}{3}\right)}^2-1=2\left(\frac{1}{2^2}\right)-1$$
32	24 31	eqtri	$$⊢\cos 2\left(\frac{\mathrm{\pi }}{3}\right)=2\left(\frac{1}{2^2}\right)-1$$
33	10	sqvali	$$⊢2^2=2\cdot 2$$
34	33	oveq2i	$$⊢\frac{1}{2^2}=\frac{1}{2\cdot 2}$$
35	34	oveq2i	$$⊢2\left(\frac{1}{2^2}\right)=2\left(\frac{1}{2\cdot 2}\right)$$
36		ax-1cn	$$⊢1\in ℂ$$
37	10 10	mulcli	$$⊢2\cdot 2\in ℂ$$
38		2t2e4	$$⊢2\cdot 2=4$$
39		4ne0	$$⊢4\ne 0$$
40	38 39	eqnetri	$$⊢2\cdot 2\ne 0$$
41	10 36 37 40	divassi	$$⊢\frac{2\cdot 1}{2\cdot 2}=2\left(\frac{1}{2\cdot 2}\right)$$
42		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
43		divcan5	$$⊢\left(1\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{2\cdot 1}{2\cdot 2}=\frac{1}{2}$$
44	36 42 42 43	mp3an	$$⊢\frac{2\cdot 1}{2\cdot 2}=\frac{1}{2}$$
45	41 44	eqtr3i	$$⊢2\left(\frac{1}{2\cdot 2}\right)=\frac{1}{2}$$
46	35 45	eqtri	$$⊢2\left(\frac{1}{2^2}\right)=\frac{1}{2}$$
47	46	oveq1i	$$⊢2\left(\frac{1}{2^2}\right)-1=\left(\frac{1}{2}\right)-1$$
48		2div2e1	$$⊢\frac{2}{2}=1$$
49	48	eqcomi	$$⊢1=\frac{2}{2}$$
50	49	oveq2i	$$⊢\left(\frac{1}{2}\right)-1=\left(\frac{1}{2}\right)-\left(\frac{2}{2}\right)$$
51		divsubdir	$$⊢\left(1\in ℂ\wedge 2\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{1-2}{2}=\left(\frac{1}{2}\right)-\left(\frac{2}{2}\right)$$
52	36 10 42 51	mp3an	$$⊢\frac{1-2}{2}=\left(\frac{1}{2}\right)-\left(\frac{2}{2}\right)$$
53	50 52	eqtr4i	$$⊢\left(\frac{1}{2}\right)-1=\frac{1-2}{2}$$
54	10 36	negsubdi2i	$$⊢-\left(2-1\right)=1-2$$
55		2m1e1	$$⊢2-1=1$$
56	55	negeqi	$$⊢-\left(2-1\right)=-1$$
57	54 56	eqtr3i	$$⊢1-2=-1$$
58	57	oveq1i	$$⊢\frac{1-2}{2}=\frac{-1}{2}$$
59	47 53 58	3eqtri	$$⊢2\left(\frac{1}{2^2}\right)-1=\frac{-1}{2}$$
60	21 32 59	3eqtri	$$⊢\cos \left(\frac{2\mathrm{\pi }}{3}\right)=\frac{-1}{2}$$
61	20	fveq2i	$$⊢\sin \left(\frac{2\mathrm{\pi }}{3}\right)=\sin 2\left(\frac{\mathrm{\pi }}{3}\right)$$
62		sin2t	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ\to \sin 2\left(\frac{\mathrm{\pi }}{3}\right)=2\sin \left(\frac{\mathrm{\pi }}{3}\right)\cos \left(\frac{\mathrm{\pi }}{3}\right)$$
63	22 62	ax-mp	$$⊢\sin 2\left(\frac{\mathrm{\pi }}{3}\right)=2\sin \left(\frac{\mathrm{\pi }}{3}\right)\cos \left(\frac{\mathrm{\pi }}{3}\right)$$
64		oveq12	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}\right)\to \sin \left(\frac{\mathrm{\pi }}{3}\right)\cos \left(\frac{\mathrm{\pi }}{3}\right)=\left(\frac{\sqrt{3}}{2}\right)\left(\frac{1}{2}\right)$$
65	25 64	ax-mp	$$⊢\sin \left(\frac{\mathrm{\pi }}{3}\right)\cos \left(\frac{\mathrm{\pi }}{3}\right)=\left(\frac{\sqrt{3}}{2}\right)\left(\frac{1}{2}\right)$$
66	65	oveq2i	$$⊢2\sin \left(\frac{\mathrm{\pi }}{3}\right)\cos \left(\frac{\mathrm{\pi }}{3}\right)=2\left(\frac{\sqrt{3}}{2}\right)\left(\frac{1}{2}\right)$$
67	9 10 11	divcli	$$⊢\frac{\sqrt{3}}{2}\in ℂ$$
68	67 10 11	divreci	$$⊢\frac{\frac{\sqrt{3}}{2}}{2}=\left(\frac{\sqrt{3}}{2}\right)\left(\frac{1}{2}\right)$$
69	68	eqcomi	$$⊢\left(\frac{\sqrt{3}}{2}\right)\left(\frac{1}{2}\right)=\frac{\frac{\sqrt{3}}{2}}{2}$$
70	69	oveq2i	$$⊢2\left(\frac{\sqrt{3}}{2}\right)\left(\frac{1}{2}\right)=2\left(\frac{\frac{\sqrt{3}}{2}}{2}\right)$$
71	67 10 11	divcan2i	$$⊢2\left(\frac{\frac{\sqrt{3}}{2}}{2}\right)=\frac{\sqrt{3}}{2}$$
72	66 70 71	3eqtri	$$⊢2\sin \left(\frac{\mathrm{\pi }}{3}\right)\cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}$$
73	61 63 72	3eqtri	$$⊢\sin \left(\frac{2\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}$$
74	73	oveq2i	$$⊢\mathrm{i}\sin \left(\frac{2\mathrm{\pi }}{3}\right)=\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
75	60 74	oveq12i	$$⊢\cos \left(\frac{2\mathrm{\pi }}{3}\right)+\mathrm{i}\sin \left(\frac{2\mathrm{\pi }}{3}\right)=\left(\frac{-1}{2}\right)+\mathrm{i}\left(\frac{\sqrt{3}}{2}\right)$$
76	13 16 75	3eqtr4ri	$$⊢\cos \left(\frac{2\mathrm{\pi }}{3}\right)+\mathrm{i}\sin \left(\frac{2\mathrm{\pi }}{3}\right)=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$
77	1 4 76	3eqtri	$$⊢W=\frac{-1+\mathrm{i}\sqrt{3}}{2}$$