Theorem root1id

Description: Property of an N -th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Assertion	root1id	$$⊢N\in \mathbb{N}\to {\left({-1}^{\frac{2}{N}}\right)}^N=1$$

Proof

Step	Hyp	Ref	Expression
1		neg1cn	$$⊢-1\in ℂ$$
2	1	a1i	$$⊢N\in \mathbb{N}\to -1\in ℂ$$
3		2re	$$⊢2\in ℝ$$
4		nndivre	$$⊢\left(2\in ℝ\wedge N\in \mathbb{N}\right)\to \frac{2}{N}\in ℝ$$
5	3 4	mpan	$$⊢N\in \mathbb{N}\to \frac{2}{N}\in ℝ$$
6	5	recnd	$$⊢N\in \mathbb{N}\to \frac{2}{N}\in ℂ$$
7		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
8	2 6 7	cxpmul2d	$$⊢N\in \mathbb{N}\to {\left(-1\right)}^{\left(\frac{2}{N}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}={\left({-1}^{\frac{2}{N}}\right)}^N$$
9		2cnd	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
10		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
11		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
12	9 10 11	divcan1d	$$⊢N\in \mathbb{N}\to \left(\frac{2}{N}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=2$$
13	12	oveq2d	$$⊢N\in \mathbb{N}\to {\left(-1\right)}^{\left(\frac{2}{N}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}={\left(-1\right)}^2$$
14		2nn0	$$⊢2\in {\mathbb{N}}_0$$
15		cxpexp	$$⊢\left(-1\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to {\left(-1\right)}^2={\left(-1\right)}^2$$
16	1 14 15	mp2an	$$⊢{\left(-1\right)}^2={\left(-1\right)}^2$$
17		ax-1cn	$$⊢1\in ℂ$$
18		sqneg	$$⊢1\in ℂ\to {\left(-1\right)}^2=1^2$$
19	17 18	ax-mp	$$⊢{\left(-1\right)}^2=1^2$$
20		sq1	$$⊢1^2=1$$
21	16 19 20	3eqtri	$$⊢{\left(-1\right)}^2=1$$
22	13 21	eqtrdi	$$⊢N\in \mathbb{N}\to {\left(-1\right)}^{\left(\frac{2}{N}\right)\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}=1$$
23	8 22	eqtr3d	$$⊢N\in \mathbb{N}\to {\left({-1}^{\frac{2}{N}}\right)}^N=1$$