Theorem bruval2

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

	Ref	Expression
Assertion	bruval2	Could not format assertion : No typesetting found for |- ( N e. NN -> ( bRoU ` N ) = ( -u 1 ^c ( 2 / N ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2	1	a1i	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
3		picn	$$⊢\mathrm{\pi }\in ℂ$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5	3 4	mulcli	$$⊢\mathrm{\pi }\mathrm{i}\in ℂ$$
6	5	a1i	$$⊢N\in \mathbb{N}\to \mathrm{\pi }\mathrm{i}\in ℂ$$
7		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
8		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
9	2 6 7 8	div23d	$$⊢N\in \mathbb{N}\to \frac{2\mathrm{\pi }\mathrm{i}}{N}=\left(\frac{2}{N}\right)\mathrm{\pi }\mathrm{i}$$
10		logm1	$$⊢\log -1=\mathrm{i}\mathrm{\pi }$$
11	4 3	mulcomi	$$⊢\mathrm{i}\mathrm{\pi }=\mathrm{\pi }\mathrm{i}$$
12	10 11	eqtr2i	$$⊢\mathrm{\pi }\mathrm{i}=\log -1$$
13	12	a1i	$$⊢N\in \mathbb{N}\to \mathrm{\pi }\mathrm{i}=\log -1$$
14	13	oveq2d	$$⊢N\in \mathbb{N}\to \left(\frac{2}{N}\right)\mathrm{\pi }\mathrm{i}=\left(\frac{2}{N}\right)\log -1$$
15	9 14	eqtrd	$$⊢N\in \mathbb{N}\to \frac{2\mathrm{\pi }\mathrm{i}}{N}=\left(\frac{2}{N}\right)\log -1$$
16	15	fveq2d	$$⊢N\in \mathbb{N}\to {\mathrm{e}}^{\frac{2\mathrm{\pi }\mathrm{i}}{N}}={\mathrm{e}}^{\left(\frac{2}{N}\right)\log -1}$$
17		bruval	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 |-
18		neg1cn	$$⊢-1\in ℂ$$
19	18	a1i	$$⊢N\in \mathbb{N}\to -1\in ℂ$$
20		neg1ne0	$$⊢-1\ne 0$$
21	20	a1i	$$⊢N\in \mathbb{N}\to -1\ne 0$$
22	2 7 8	divcld	$$⊢N\in \mathbb{N}\to \frac{2}{N}\in ℂ$$
23	19 21 22	cxpefd	$$⊢N\in \mathbb{N}\to {\left(-1\right)}^{\frac{2}{N}}={\mathrm{e}}^{\left(\frac{2}{N}\right)\log -1}$$
24	16 17 23	3eqtr4d	Could not format ( N e. NN -> ( bRoU ` N ) = ( -u 1 ^c ( 2 / N ) ) ) : No typesetting found for |- ( N e. NN -> ( bRoU ` N ) = ( -u 1 ^c ( 2 / N ) ) ) with typecode |-