Theorem bruval3

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

	Ref	Expression
Assertion	bruval3	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( ( cos ‘ ( ( 2 · π ) / 𝑁 ) ) + ( i · ( sin ‘ ( ( 2 · π ) / 𝑁 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bruval	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) )
2		picn	⊢ π ∈ ℂ
3		ax-icn	⊢ i ∈ ℂ
4	2 3	mulcomi	⊢ ( π · i ) = ( i · π )
5	4	a1i	⊢ ( 𝑁 ∈ ℕ → ( π · i ) = ( i · π ) )
6	5	oveq2d	⊢ ( 𝑁 ∈ ℕ → ( 2 · ( π · i ) ) = ( 2 · ( i · π ) ) )
7		2cnd	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
8	3	a1i	⊢ ( 𝑁 ∈ ℕ → i ∈ ℂ )
9	2	a1i	⊢ ( 𝑁 ∈ ℕ → π ∈ ℂ )
10	7 8 9	mul12d	⊢ ( 𝑁 ∈ ℕ → ( 2 · ( i · π ) ) = ( i · ( 2 · π ) ) )
11	6 10	eqtrd	⊢ ( 𝑁 ∈ ℕ → ( 2 · ( π · i ) ) = ( i · ( 2 · π ) ) )
12	11	oveq1d	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · ( π · i ) ) / 𝑁 ) = ( ( i · ( 2 · π ) ) / 𝑁 ) )
13		2picn	⊢ ( 2 · π ) ∈ ℂ
14	13	a1i	⊢ ( 𝑁 ∈ ℕ → ( 2 · π ) ∈ ℂ )
15		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
16		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
17	8 14 15 16	div23d	⊢ ( 𝑁 ∈ ℕ → ( ( i · ( 2 · π ) ) / 𝑁 ) = ( ( i / 𝑁 ) · ( 2 · π ) ) )
18	8 15 14 16	div32d	⊢ ( 𝑁 ∈ ℕ → ( ( i / 𝑁 ) · ( 2 · π ) ) = ( i · ( ( 2 · π ) / 𝑁 ) ) )
19	12 17 18	3eqtrd	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · ( π · i ) ) / 𝑁 ) = ( i · ( ( 2 · π ) / 𝑁 ) ) )
20	19	fveq2d	⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) = ( exp ‘ ( i · ( ( 2 · π ) / 𝑁 ) ) ) )
21	14 15 16	divcld	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · π ) / 𝑁 ) ∈ ℂ )
22		efival	⊢ ( ( ( 2 · π ) / 𝑁 ) ∈ ℂ → ( exp ‘ ( i · ( ( 2 · π ) / 𝑁 ) ) ) = ( ( cos ‘ ( ( 2 · π ) / 𝑁 ) ) + ( i · ( sin ‘ ( ( 2 · π ) / 𝑁 ) ) ) ) )
23	21 22	syl	⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( i · ( ( 2 · π ) / 𝑁 ) ) ) = ( ( cos ‘ ( ( 2 · π ) / 𝑁 ) ) + ( i · ( sin ‘ ( ( 2 · π ) / 𝑁 ) ) ) ) )
24	1 20 23	3eqtrd	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( ( cos ‘ ( ( 2 · π ) / 𝑁 ) ) + ( i · ( sin ‘ ( ( 2 · π ) / 𝑁 ) ) ) ) )