bru3sq

Description: The square 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	bru3sq	$⊢ W^{2} = (\frac{- 1}{2}) - i (\frac{\sqrt{3}}{2})$

Step	Hyp	Ref	Expression
1		bru3eq.w	Could not format W = ( bRoU ` 3 ) : No typesetting found for \|- W = ( bRoU ` 3 ) with typecode \|-
2	1	bru3cj	$⊢ \overline{W} = W^{2}$
3	1	bru3val	$⊢ W = \frac{- 1 + i \sqrt{3}}{2}$
4	3	fveq2i	$⊢ \overline{W} = \overline{\frac{- 1 + i \sqrt{3}}{2}}$
5		neg1cn	$⊢ - 1 \in ℂ$
6		ax-icn	$⊢ i \in ℂ$
7		3re	$⊢ 3 \in ℝ$
8		3pos	$⊢ 0 < 3$
9	7 8	sqrtpclii	$⊢ \sqrt{3} \in ℝ$
10	9	recni	$⊢ \sqrt{3} \in ℂ$
11	6 10	mulcli	$⊢ i \sqrt{3} \in ℂ$
12		2cn	$⊢ 2 \in ℂ$
13		2ne0	$⊢ 2 \neq 0$
14	5 11 12 13	divdiri	$⊢ \frac{- 1 + i \sqrt{3}}{2} = (\frac{- 1}{2}) + (\frac{i \sqrt{3}}{2})$
15	6 10 12 13	divassi	$⊢ \frac{i \sqrt{3}}{2} = i (\frac{\sqrt{3}}{2})$
16	15	oveq2i	$⊢ (\frac{- 1}{2}) + (\frac{i \sqrt{3}}{2}) = (\frac{- 1}{2}) + i (\frac{\sqrt{3}}{2})$
17	14 16	eqtri	$⊢ \frac{- 1 + i \sqrt{3}}{2} = (\frac{- 1}{2}) + i (\frac{\sqrt{3}}{2})$
18	17	fveq2i	$⊢ \overline{\frac{- 1 + i \sqrt{3}}{2}} = \overline{(\frac{- 1}{2}) + i (\frac{\sqrt{3}}{2})}$
19		neg1rr	$⊢ - 1 \in ℝ$
20	19	rehalfcli	$⊢ \frac{- 1}{2} \in ℝ$
21	9	rehalfcli	$⊢ \frac{\sqrt{3}}{2} \in ℝ$
22		cjreim	$⊢ (\frac{- 1}{2} \in ℝ \land \frac{\sqrt{3}}{2} \in ℝ) \to \overline{(\frac{- 1}{2}) + i (\frac{\sqrt{3}}{2})} = (\frac{- 1}{2}) - i (\frac{\sqrt{3}}{2})$
23	20 21 22	mp2an	$⊢ \overline{(\frac{- 1}{2}) + i (\frac{\sqrt{3}}{2})} = (\frac{- 1}{2}) - i (\frac{\sqrt{3}}{2})$
24	4 18 23	3eqtri	$⊢ \overline{W} = (\frac{- 1}{2}) - i (\frac{\sqrt{3}}{2})$
25	2 24	eqtr3i	$⊢ W^{2} = (\frac{- 1}{2}) - i (\frac{\sqrt{3}}{2})$

Metamath Proof Explorer