Theorem bru3cj

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

	Ref	Expression
Hypothesis	bru3eq.w	⊢ 𝑊 = ( bRoU ‘ 3 )
Assertion	bru3cj	⊢ ( ∗ ‘ 𝑊 ) = ( 𝑊 ↑ 2 )

Proof

Step	Hyp	Ref	Expression
1		bru3eq.w	⊢ 𝑊 = ( bRoU ‘ 3 )
2		3nn	⊢ 3 ∈ ℕ
3		bruval2	⊢ ( 3 ∈ ℕ → ( bRoU ‘ 3 ) = ( - 1 ↑𝑐 ( 2 / 3 ) ) )
4	2 3	ax-mp	⊢ ( bRoU ‘ 3 ) = ( - 1 ↑𝑐 ( 2 / 3 ) )
5	1 4	eqtri	⊢ 𝑊 = ( - 1 ↑𝑐 ( 2 / 3 ) )
6	5	fveq2i	⊢ ( ∗ ‘ 𝑊 ) = ( ∗ ‘ ( - 1 ↑𝑐 ( 2 / 3 ) ) )
7		neg1cn	⊢ - 1 ∈ ℂ
8		2cn	⊢ 2 ∈ ℂ
9		3cn	⊢ 3 ∈ ℂ
10		3ne0	⊢ 3 ≠ 0
11	8 9 10	divcli	⊢ ( 2 / 3 ) ∈ ℂ
12	7 11	pm3.2i	⊢ ( - 1 ∈ ℂ ∧ ( 2 / 3 ) ∈ ℂ )
13		cxpcl	⊢ ( ( - 1 ∈ ℂ ∧ ( 2 / 3 ) ∈ ℂ ) → ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ )
14	12 13	ax-mp	⊢ ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ
15		exp1	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ → ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) = ( - 1 ↑𝑐 ( 2 / 3 ) ) )
16	14 15	ax-mp	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) = ( - 1 ↑𝑐 ( 2 / 3 ) )
17	16	eqcomi	⊢ ( - 1 ↑𝑐 ( 2 / 3 ) ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 )
18	17	fveq2i	⊢ ( ∗ ‘ ( - 1 ↑𝑐 ( 2 / 3 ) ) ) = ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) )
19		1z	⊢ 1 ∈ ℤ
20	2 19	pm3.2i	⊢ ( 3 ∈ ℕ ∧ 1 ∈ ℤ )
21		root1cj	⊢ ( ( 3 ∈ ℕ ∧ 1 ∈ ℤ ) → ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ ( 3 − 1 ) ) )
22	20 21	ax-mp	⊢ ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ ( 3 − 1 ) )
23	18 22	eqtri	⊢ ( ∗ ‘ ( - 1 ↑𝑐 ( 2 / 3 ) ) ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ ( 3 − 1 ) )
24	5	eqcomi	⊢ ( - 1 ↑𝑐 ( 2 / 3 ) ) = 𝑊
25		3m1e2	⊢ ( 3 − 1 ) = 2
26	24 25	oveq12i	⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ ( 3 − 1 ) ) = ( 𝑊 ↑ 2 )
27	6 23 26	3eqtri	⊢ ( ∗ ‘ 𝑊 ) = ( 𝑊 ↑ 2 )