Theorem brucn

Description: The basic N -th root of unity is a complex number. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	brucn	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		bruval	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) )
2		2cn	⊢ 2 ∈ ℂ
3		picn	⊢ π ∈ ℂ
4		ax-icn	⊢ i ∈ ℂ
5	3 4	mulcli	⊢ ( π · i ) ∈ ℂ
6	2 5	mulcli	⊢ ( 2 · ( π · i ) ) ∈ ℂ
7	6	a1i	⊢ ( 𝑁 ∈ ℕ → ( 2 · ( π · i ) ) ∈ ℂ )
8		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
9		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
10	7 8 9	divcld	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · ( π · i ) ) / 𝑁 ) ∈ ℂ )
11	10	efcld	⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) ∈ ℂ )
12	1 11	eqeltrd	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) ∈ ℂ )