Theorem ef2kpi

Description: If K is an integer, then the exponential of 2 Kpi i is 1 . (Contributed by Mario Carneiro, 9-May-2014)

	Ref	Expression
Assertion	ef2kpi	$$⊢K\in \mathbb{Z}\to {\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }K}=1$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		2cn	$$⊢2\in ℂ$$
3		picn	$$⊢\mathrm{\pi }\in ℂ$$
4	2 3	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
5	1 4	mulcli	$$⊢\mathrm{i}2\mathrm{\pi }\in ℂ$$
6		zcn	$$⊢K\in \mathbb{Z}\to K\in ℂ$$
7		mulcom	$$⊢\left(\mathrm{i}2\mathrm{\pi }\in ℂ\wedge K\in ℂ\right)\to \mathrm{i}2\mathrm{\pi }K=K\mathrm{i}2\mathrm{\pi }$$
8	5 6 7	sylancr	$$⊢K\in \mathbb{Z}\to \mathrm{i}2\mathrm{\pi }K=K\mathrm{i}2\mathrm{\pi }$$
9	8	fveq2d	$$⊢K\in \mathbb{Z}\to {\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }K}={\mathrm{e}}^{K\mathrm{i}2\mathrm{\pi }}$$
10		efexp	$$⊢\left(\mathrm{i}2\mathrm{\pi }\in ℂ\wedge K\in \mathbb{Z}\right)\to {\mathrm{e}}^{K\mathrm{i}2\mathrm{\pi }}={{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}}^K$$
11	5 10	mpan	$$⊢K\in \mathbb{Z}\to {\mathrm{e}}^{K\mathrm{i}2\mathrm{\pi }}={{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}}^K$$
12		ef2pi	$$⊢{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}=1$$
13	12	oveq1i	$$⊢{{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}}^K=1^K$$
14		1exp	$$⊢K\in \mathbb{Z}\to 1^K=1$$
15	13 14	eqtrid	$$⊢K\in \mathbb{Z}\to {{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}}^K=1$$
16	9 11 15	3eqtrd	$$⊢K\in \mathbb{Z}\to {\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }K}=1$$