Theorem bruval

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

	Ref	Expression
Assertion	bruval	Could not format assertion : No typesetting found for |- ( N e. NN -> ( bRoU ` N ) = ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢n=N\to \frac{2\mathrm{\pi }\mathrm{i}}{n}=\frac{2\mathrm{\pi }\mathrm{i}}{N}$$
2	1	fveq2d	$$⊢n=N\to {\mathrm{e}}^{\frac{2\mathrm{\pi }\mathrm{i}}{n}}={\mathrm{e}}^{\frac{2\mathrm{\pi }\mathrm{i}}{N}}$$
3		df-bru	Could not format bRoU = ( n e. NN |-> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) ) : No typesetting found for |- bRoU = ( n e. NN |-> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / n ) ) ) with typecode |-
4		fvex	$$⊢{\mathrm{e}}^{\frac{2\mathrm{\pi }\mathrm{i}}{N}}\in \mathrm{V}$$
5	2 3 4	fvmpt	Could not format ( N e. NN -> ( bRoU ` N ) = ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) ) : No typesetting found for |- ( N e. NN -> ( bRoU ` N ) = ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) ) with typecode |-