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

Metamath Proof Explorer

Theorem ef2kpi

Description: If K is an integer, then the exponential of 2 Kpi i is 1 . (Contributed by Mario Carneiro, 9-May-2014)

Ref Expression
Assertion ef2kpi ( 𝐾 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 2cn ⊢ 2 ∈ ℂ
3 picn ⊢ π ∈ ℂ
4 2 3 mulcli ⊢ ( 2 · π ) ∈ ℂ
5 1 4 mulcli ⊢ ( i · ( 2 · π ) ) ∈ ℂ
6 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
7 mulcom ⊢ ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · 𝐾 ) = ( 𝐾 · ( i · ( 2 · π ) ) ) )
8 5 6 7 sylancr ⊢ ( 𝐾 ∈ ℤ → ( ( i · ( 2 · π ) ) · 𝐾 ) = ( 𝐾 · ( i · ( 2 · π ) ) ) )
9 8 fveq2d ⊢ ( 𝐾 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) = ( exp ‘ ( 𝐾 · ( i · ( 2 · π ) ) ) ) )
10 efexp ⊢ ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( 𝐾 · ( i · ( 2 · π ) ) ) ) = ( ( exp ‘ ( i · ( 2 · π ) ) ) ↑ 𝐾 ) )
11 5 10 mpan ⊢ ( 𝐾 ∈ ℤ → ( exp ‘ ( 𝐾 · ( i · ( 2 · π ) ) ) ) = ( ( exp ‘ ( i · ( 2 · π ) ) ) ↑ 𝐾 ) )
12 ef2pi ⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = 1
13 12 oveq1i ⊢ ( ( exp ‘ ( i · ( 2 · π ) ) ) ↑ 𝐾 ) = ( 1 ↑ 𝐾 )
14 1exp ⊢ ( 𝐾 ∈ ℤ → ( 1 ↑ 𝐾 ) = 1 )
15 13 14 eqtrid ⊢ ( 𝐾 ∈ ℤ → ( ( exp ‘ ( i · ( 2 · π ) ) ) ↑ 𝐾 ) = 1 )
16 9 11 15 3eqtrd ⊢ ( 𝐾 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) = 1 )