Theorem bru3cj

Description: The complex conjugate of 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	bru3cj	$$⊢\bar{W}=W^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		bruval2	Could not format ( 3 e. NN -> ( bRoU ` 3 ) = ( -u 1 ^c ( 2 / 3 ) ) ) : No typesetting found for |- ( 3 e. NN -> ( bRoU ` 3 ) = ( -u 1 ^c ( 2 / 3 ) ) ) with typecode |-
4	2 3	ax-mp	Could not format ( bRoU ` 3 ) = ( -u 1 ^c ( 2 / 3 ) ) : No typesetting found for |- ( bRoU ` 3 ) = ( -u 1 ^c ( 2 / 3 ) ) with typecode |-
5	1 4	eqtri	$$⊢W={\left(-1\right)}^{\frac{2}{3}}$$
6	5	fveq2i	$$⊢\bar{W}=\overline{{\left(-1\right)}^{\frac{2}{3}}}$$
7		neg1cn	$$⊢-1\in ℂ$$
8		2cn	$$⊢2\in ℂ$$
9		3cn	$$⊢3\in ℂ$$
10		3ne0	$$⊢3\ne 0$$
11	8 9 10	divcli	$$⊢\frac{2}{3}\in ℂ$$
12	7 11	pm3.2i	$$⊢\left(-1\in ℂ\wedge \frac{2}{3}\in ℂ\right)$$
13		cxpcl	$$⊢\left(-1\in ℂ\wedge \frac{2}{3}\in ℂ\right)\to {\left(-1\right)}^{\frac{2}{3}}\in ℂ$$
14	12 13	ax-mp	$$⊢{\left(-1\right)}^{\frac{2}{3}}\in ℂ$$
15		exp1	$$⊢{\left(-1\right)}^{\frac{2}{3}}\in ℂ\to {\left({-1}^{\frac{2}{3}}\right)}^1={\left(-1\right)}^{\frac{2}{3}}$$
16	14 15	ax-mp	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^1={\left(-1\right)}^{\frac{2}{3}}$$
17	16	eqcomi	$$⊢{\left(-1\right)}^{\frac{2}{3}}={\left({-1}^{\frac{2}{3}}\right)}^1$$
18	17	fveq2i	$$⊢\overline{{\left(-1\right)}^{\frac{2}{3}}}=\stackrel{‾}{{\left({-1}^{\frac{2}{3}}\right)}^1}$$
19		1z	$$⊢1\in \mathbb{Z}$$
20	2 19	pm3.2i	$$⊢\left(3\in \mathbb{N}\wedge 1\in \mathbb{Z}\right)$$
21		root1cj	$$⊢\left(3\in \mathbb{N}\wedge 1\in \mathbb{Z}\right)\to \stackrel{‾}{{\left({-1}^{\frac{2}{3}}\right)}^1}={\left({-1}^{\frac{2}{3}}\right)}^{3-1}$$
22	20 21	ax-mp	$$⊢\stackrel{‾}{{\left({-1}^{\frac{2}{3}}\right)}^1}={\left({-1}^{\frac{2}{3}}\right)}^{3-1}$$
23	18 22	eqtri	$$⊢\overline{{\left(-1\right)}^{\frac{2}{3}}}={\left({-1}^{\frac{2}{3}}\right)}^{3-1}$$
24	5	eqcomi	$$⊢{\left(-1\right)}^{\frac{2}{3}}=W$$
25		3m1e2	$$⊢3-1=2$$
26	24 25	oveq12i	$$⊢{\left({-1}^{\frac{2}{3}}\right)}^{3-1}=W^2$$
27	6 23 26	3eqtri	$$⊢\bar{W}=W^2$$