Theorem bruval

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

	Ref	Expression
Assertion	bruval	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = 𝑁 → ( ( 2 · ( π · i ) ) / 𝑛 ) = ( ( 2 · ( π · i ) ) / 𝑁 ) )
2	1	fveq2d	⊢ ( 𝑛 = 𝑁 → ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑛 ) ) = ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) )
3		df-bru	⊢ bRoU = ( 𝑛 ∈ ℕ ↦ ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑛 ) ) )
4		fvex	⊢ ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) ∈ V
5	2 3 4	fvmpt	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( exp ‘ ( ( 2 · ( π · i ) ) / 𝑁 ) ) )