Theorem bruval

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

	Ref	Expression
Assertion	bruval	|- ( N e. NN -> ( bRoU ` N ) = ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( n = N -> ( ( 2 x. ( _pi x. _i ) ) / n ) = ( ( 2 x. ( _pi x. _i ) ) / N ) )
2	1	fveq2d	|- ( n = N -> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) = ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) )
3		df-bru	|- bRoU = ( n e. NN |-> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) )
4		fvex	|- ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) e. _V
5	2 3 4	fvmpt	|- ( N e. NN -> ( bRoU ` N ) = ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) )