Theorem bru3sq

Description: The square of the basic 3rd root of unity. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Hypothesis	bru3eq.w	⊢ 𝑊 = ( bRoU ‘ 3 )
Assertion	bru3sq	⊢ ( 𝑊 ↑ 2 ) = ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bru3eq.w	⊢ 𝑊 = ( bRoU ‘ 3 )
2	1	bru3cj	⊢ ( ∗ ‘ 𝑊 ) = ( 𝑊 ↑ 2 )
3	1	bru3val	⊢ 𝑊 = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )
4	3	fveq2i	⊢ ( ∗ ‘ 𝑊 ) = ( ∗ ‘ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) )
5		neg1cn	⊢ - 1 ∈ ℂ
6		ax-icn	⊢ i ∈ ℂ
7		3re	⊢ 3 ∈ ℝ
8		3pos	⊢ 0 < 3
9	7 8	sqrtpclii	⊢ ( √ ‘ 3 ) ∈ ℝ
10	9	recni	⊢ ( √ ‘ 3 ) ∈ ℂ
11	6 10	mulcli	⊢ ( i · ( √ ‘ 3 ) ) ∈ ℂ
12		2cn	⊢ 2 ∈ ℂ
13		2ne0	⊢ 2 ≠ 0
14	5 11 12 13	divdiri	⊢ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) = ( ( - 1 / 2 ) + ( ( i · ( √ ‘ 3 ) ) / 2 ) )
15	6 10 12 13	divassi	⊢ ( ( i · ( √ ‘ 3 ) ) / 2 ) = ( i · ( ( √ ‘ 3 ) / 2 ) )
16	15	oveq2i	⊢ ( ( - 1 / 2 ) + ( ( i · ( √ ‘ 3 ) ) / 2 ) ) = ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) )
17	14 16	eqtri	⊢ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) = ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) )
18	17	fveq2i	⊢ ( ∗ ‘ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ) = ( ∗ ‘ ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) ) )
19		neg1rr	⊢ - 1 ∈ ℝ
20	19	rehalfcli	⊢ ( - 1 / 2 ) ∈ ℝ
21	9	rehalfcli	⊢ ( ( √ ‘ 3 ) / 2 ) ∈ ℝ
22		cjreim	⊢ ( ( ( - 1 / 2 ) ∈ ℝ ∧ ( ( √ ‘ 3 ) / 2 ) ∈ ℝ ) → ( ∗ ‘ ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) ) ) = ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) )
23	20 21 22	mp2an	⊢ ( ∗ ‘ ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) ) ) = ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) )
24	4 18 23	3eqtri	⊢ ( ∗ ‘ 𝑊 ) = ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) )
25	2 24	eqtr3i	⊢ ( 𝑊 ↑ 2 ) = ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) )