# Metamath Proof Explorer

## 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 }}=\mathrm{cos}\mathrm{\pi }+\mathrm{i}\mathrm{sin}\mathrm{\pi }$
3 1 2 ax-mp ${⊢}{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}=\mathrm{cos}\mathrm{\pi }+\mathrm{i}\mathrm{sin}\mathrm{\pi }$
4 cospi ${⊢}\mathrm{cos}\mathrm{\pi }=-1$
5 sinpi ${⊢}\mathrm{sin}\mathrm{\pi }=0$
6 5 oveq2i ${⊢}\mathrm{i}\mathrm{sin}\mathrm{\pi }=\mathrm{i}\cdot 0$
7 it0e0 ${⊢}\mathrm{i}\cdot 0=0$
8 6 7 eqtri ${⊢}\mathrm{i}\mathrm{sin}\mathrm{\pi }=0$
9 4 8 oveq12i ${⊢}\mathrm{cos}\mathrm{\pi }+\mathrm{i}\mathrm{sin}\mathrm{\pi }=-1+0$
10 neg1cn ${⊢}-1\in ℂ$
11 10 addid1i ${⊢}-1+0=-1$
12 9 11 eqtri ${⊢}\mathrm{cos}\mathrm{\pi }+\mathrm{i}\mathrm{sin}\mathrm{\pi }=-1$
13 3 12 eqtri ${⊢}{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}=-1$