Theorem efipi

Description: The exponential of _i x. _pi is -u 1 . (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 10-May-2014)

	Ref	Expression
Assertion	efipi	$$⊢{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}=-1$$

Proof

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