Theorem bruval2

Description: An alternate way to express the basic N -th root of unity, see cxpeq . (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	bruval2	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2	1	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
3		picn	⊢ π ∈ ℂ
4		ax-icn	⊢ i ∈ ℂ
5	3 4	mulcli	⊢ ( π · i ) ∈ ℂ
6	5	a1i	⊢ ( 𝑁 ∈ ℕ → ( π · i ) ∈ ℂ )
7		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
8		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
9	2 6 7 8	div23d	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · ( π · i ) ) / 𝑁 ) = ( ( 2 / 𝑁 ) · ( π · i ) ) )
10		logm1	⊢ ( log ‘ - 1 ) = ( i · π )
11	4 3	mulcomi	⊢ ( i · π ) = ( π · i )
12	10 11	eqtr2i	⊢ ( π · i ) = ( log ‘ - 1 )
13	12	a1i	⊢ ( 𝑁 ∈ ℕ → ( π · i ) = ( log ‘ - 1 ) )
14	13	oveq2d	⊢ ( 𝑁 ∈ ℕ → ( ( 2 / 𝑁 ) · ( π · i ) ) = ( ( 2 / 𝑁 ) · ( log ‘ - 1 ) ) )
15	9 14	eqtrd	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · ( π · i ) ) / 𝑁 ) = ( ( 2 / 𝑁 ) · ( log ‘ - 1 ) ) )
16	15	fveq2d	⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) = ( exp ‘ ( ( 2 / 𝑁 ) · ( log ‘ - 1 ) ) ) )
17		bruval	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) )
18		neg1cn	⊢ - 1 ∈ ℂ
19	18	a1i	⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℂ )
20		neg1ne0	⊢ - 1 ≠ 0
21	20	a1i	⊢ ( 𝑁 ∈ ℕ → - 1 ≠ 0 )
22	2 7 8	divcld	⊢ ( 𝑁 ∈ ℕ → ( 2 / 𝑁 ) ∈ ℂ )
23	19 21 22	cxpefd	⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) = ( exp ‘ ( ( 2 / 𝑁 ) · ( log ‘ - 1 ) ) ) )
24	16 17 23	3eqtr4d	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) )