Theorem ef2pi

Description: The exponential of 2pi i is 1 . (Contributed by Mario Carneiro, 9-May-2014)

	Ref	Expression
Assertion	ef2pi	$$⊢{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}=1$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		picn	$$⊢\mathrm{\pi }\in ℂ$$
3	1 2	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
4		efival	$$⊢2\mathrm{\pi }\in ℂ\to {\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}=\cos 2\mathrm{\pi }+\mathrm{i}\sin 2\mathrm{\pi }$$
5	3 4	ax-mp	$$⊢{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}=\cos 2\mathrm{\pi }+\mathrm{i}\sin 2\mathrm{\pi }$$
6		cos2pi	$$⊢\cos 2\mathrm{\pi }=1$$
7		sin2pi	$$⊢\sin 2\mathrm{\pi }=0$$
8	7	oveq2i	$$⊢\mathrm{i}\sin 2\mathrm{\pi }=\mathrm{i}\cdot 0$$
9		it0e0	$$⊢\mathrm{i}\cdot 0=0$$
10	8 9	eqtri	$$⊢\mathrm{i}\sin 2\mathrm{\pi }=0$$
11	6 10	oveq12i	$$⊢\cos 2\mathrm{\pi }+\mathrm{i}\sin 2\mathrm{\pi }=1+0$$
12		1p0e1	$$⊢1+0=1$$
13	11 12	eqtri	$$⊢\cos 2\mathrm{\pi }+\mathrm{i}\sin 2\mathrm{\pi }=1$$
14	5 13	eqtri	$$⊢{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}=1$$