Theorem brucn

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

	Ref	Expression
Assertion	brucn	Could not format assertion : No typesetting found for |- ( N e. NN -> ( bRoU ` N ) e. CC ) 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		2cn	$$⊢2\in ℂ$$
3		picn	$$⊢\mathrm{\pi }\in ℂ$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5	3 4	mulcli	$$⊢\mathrm{\pi }\mathrm{i}\in ℂ$$
6	2 5	mulcli	$$⊢2\mathrm{\pi }\mathrm{i}\in ℂ$$
7	6	a1i	$$⊢N\in \mathbb{N}\to 2\mathrm{\pi }\mathrm{i}\in ℂ$$
8		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
9		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
10	7 8 9	divcld	$$⊢N\in \mathbb{N}\to \frac{2\mathrm{\pi }\mathrm{i}}{N}\in ℂ$$
11	10	efcld	$$⊢N\in \mathbb{N}\to {\mathrm{e}}^{\frac{2\mathrm{\pi }\mathrm{i}}{N}}\in ℂ$$
12	1 11	eqeltrd	Could not format ( N e. NN -> ( bRoU ` N ) e. CC ) : No typesetting found for |- ( N e. NN -> ( bRoU ` N ) e. CC ) with typecode |-