This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ e i ⁢ π = − 1

Proof

Step Hyp Ref Expression
1 picn ⊢ π ∈ ℂ
2 efival ⊢ π ∈ ℂ → e i ⁢ π = cos ⁡ π + i ⁢ sin ⁡ π
3 1 2 ax-mp ⊢ e i ⁢ π = cos ⁡ π + i ⁢ sin ⁡ π
4 cospi ⊢ cos ⁡ π = − 1
5 sinpi ⊢ sin ⁡ π = 0
6 5 oveq2i ⊢ i ⁢ sin ⁡ π = i ⋅ 0
7 it0e0 ⊢ i ⋅ 0 = 0
8 6 7 eqtri ⊢ i ⁢ sin ⁡ π = 0
9 4 8 oveq12i ⊢ cos ⁡ π + i ⁢ sin ⁡ π = - 1 + 0
10 neg1cn ⊢ − 1 ∈ ℂ
11 10 addridi ⊢ - 1 + 0 = − 1
12 9 11 eqtri ⊢ cos ⁡ π + i ⁢ sin ⁡ π = − 1
13 3 12 eqtri ⊢ e i ⁢ π = − 1