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 syl5eq ( 𝐾 ∈ ℤ → ( ( exp ‘ ( i · ( 2 · π ) ) ) ↑ 𝐾 ) = 1 )
16 9 11 15 3eqtrd ( 𝐾 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) = 1 )