# Metamath Proof Explorer

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