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

Metamath Proof Explorer

Theorem ef2pi

Description: The exponential of 2pi i is 1 . (Contributed by Mario Carneiro, 9-May-2014)

Ref Expression
Assertion ef2pi ( exp ‘ ( i · ( 2 · π ) ) ) = 1

Proof

Step Hyp Ref Expression
1 2cn ⊢ 2 ∈ ℂ
2 picn ⊢ π ∈ ℂ
3 1 2 mulcli ⊢ ( 2 · π ) ∈ ℂ
4 efival ⊢ ( ( 2 · π ) ∈ ℂ → ( exp ‘ ( i · ( 2 · π ) ) ) = ( ( cos ‘ ( 2 · π ) ) + ( i · ( sin ‘ ( 2 · π ) ) ) ) )
5 3 4 ax-mp ⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = ( ( cos ‘ ( 2 · π ) ) + ( i · ( sin ‘ ( 2 · π ) ) ) )
6 cos2pi ⊢ ( cos ‘ ( 2 · π ) ) = 1
7 sin2pi ⊢ ( sin ‘ ( 2 · π ) ) = 0
8 7 oveq2i ⊢ ( i · ( sin ‘ ( 2 · π ) ) ) = ( i · 0 )
9 it0e0 ⊢ ( i · 0 ) = 0
10 8 9 eqtri ⊢ ( i · ( sin ‘ ( 2 · π ) ) ) = 0
11 6 10 oveq12i ⊢ ( ( cos ‘ ( 2 · π ) ) + ( i · ( sin ‘ ( 2 · π ) ) ) ) = ( 1 + 0 )
12 1p0e1 ⊢ ( 1 + 0 ) = 1
13 11 12 eqtri ⊢ ( ( cos ‘ ( 2 · π ) ) + ( i · ( sin ‘ ( 2 · π ) ) ) ) = 1
14 5 13 eqtri ⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = 1