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 ) |