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 ( exp ‘ ( i · π ) ) = - 1

Proof

Step Hyp Ref Expression
1 picn ⊢ π ∈ ℂ
2 efival ⊢ ( π ∈ ℂ → ( exp ‘ ( i · π ) ) = ( ( cos ‘ π ) + ( i · ( sin ‘ π ) ) ) )
3 1 2 ax-mp ⊢ ( exp ‘ ( 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 ⊢ ( exp ‘ ( i · π ) ) = - 1