Theorem bruval3

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

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

Proof

Step	Hyp	Ref	Expression
1		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 |-
2		picn	$$⊢\mathrm{\pi }\in ℂ$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4	2 3	mulcomi	$$⊢\mathrm{\pi }\mathrm{i}=\mathrm{i}\mathrm{\pi }$$
5	4	a1i	$$⊢N\in \mathbb{N}\to \mathrm{\pi }\mathrm{i}=\mathrm{i}\mathrm{\pi }$$
6	5	oveq2d	$$⊢N\in \mathbb{N}\to 2\mathrm{\pi }\mathrm{i}=2\mathrm{i}\mathrm{\pi }$$
7		2cnd	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
8	3	a1i	$$⊢N\in \mathbb{N}\to \mathrm{i}\in ℂ$$
9	2	a1i	$$⊢N\in \mathbb{N}\to \mathrm{\pi }\in ℂ$$
10	7 8 9	mul12d	$$⊢N\in \mathbb{N}\to 2\mathrm{i}\mathrm{\pi }=\mathrm{i}2\mathrm{\pi }$$
11	6 10	eqtrd	$$⊢N\in \mathbb{N}\to 2\mathrm{\pi }\mathrm{i}=\mathrm{i}2\mathrm{\pi }$$
12	11	oveq1d	$$⊢N\in \mathbb{N}\to \frac{2\mathrm{\pi }\mathrm{i}}{N}=\frac{\mathrm{i}2\mathrm{\pi }}{N}$$
13		2picn	$$⊢2\mathrm{\pi }\in ℂ$$
14	13	a1i	$$⊢N\in \mathbb{N}\to 2\mathrm{\pi }\in ℂ$$
15		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
16		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
17	8 14 15 16	div23d	$$⊢N\in \mathbb{N}\to \frac{\mathrm{i}2\mathrm{\pi }}{N}=\left(\frac{\mathrm{i}}{N}\right)2\mathrm{\pi }$$
18	8 15 14 16	div32d	$$⊢N\in \mathbb{N}\to \left(\frac{\mathrm{i}}{N}\right)2\mathrm{\pi }=\mathrm{i}\left(\frac{2\mathrm{\pi }}{N}\right)$$
19	12 17 18	3eqtrd	$$⊢N\in \mathbb{N}\to \frac{2\mathrm{\pi }\mathrm{i}}{N}=\mathrm{i}\left(\frac{2\mathrm{\pi }}{N}\right)$$
20	19	fveq2d	$$⊢N\in \mathbb{N}\to {\mathrm{e}}^{\frac{2\mathrm{\pi }\mathrm{i}}{N}}={\mathrm{e}}^{\mathrm{i}\left(\frac{2\mathrm{\pi }}{N}\right)}$$
21	14 15 16	divcld	$$⊢N\in \mathbb{N}\to \frac{2\mathrm{\pi }}{N}\in ℂ$$
22		efival	$$⊢\frac{2\mathrm{\pi }}{N}\in ℂ\to {\mathrm{e}}^{\mathrm{i}\left(\frac{2\mathrm{\pi }}{N}\right)}=\cos \left(\frac{2\mathrm{\pi }}{N}\right)+\mathrm{i}\sin \left(\frac{2\mathrm{\pi }}{N}\right)$$
23	21 22	syl	$$⊢N\in \mathbb{N}\to {\mathrm{e}}^{\mathrm{i}\left(\frac{2\mathrm{\pi }}{N}\right)}=\cos \left(\frac{2\mathrm{\pi }}{N}\right)+\mathrm{i}\sin \left(\frac{2\mathrm{\pi }}{N}\right)$$
24	1 20 23	3eqtrd	Could not format ( N e. NN -> ( bRoU ` N ) = ( ( cos ` ( ( 2 x. _pi ) / N ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / N ) ) ) ) ) : No typesetting found for |- ( N e. NN -> ( bRoU ` N ) = ( ( cos ` ( ( 2 x. _pi ) / N ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / N ) ) ) ) ) with typecode |-