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 |
|
mulcl |
⊢ ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · 𝐾 ) ∈ ℂ ) |
8 |
5 6 7
|
sylancr |
⊢ ( 𝐾 ∈ ℤ → ( ( i · ( 2 · π ) ) · 𝐾 ) ∈ ℂ ) |
9 |
|
efadd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( i · ( 2 · π ) ) · 𝐾 ) ∈ ℂ ) → ( exp ‘ ( 𝐴 + ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) ) |
10 |
8 9
|
sylan2 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( 𝐴 + ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) ) |
11 |
|
ef2kpi |
⊢ ( 𝐾 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) = 1 ) |
12 |
11
|
oveq2d |
⊢ ( 𝐾 ∈ ℤ → ( ( exp ‘ 𝐴 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( ( exp ‘ 𝐴 ) · 1 ) ) |
13 |
|
efcl |
⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ ) |
14 |
13
|
mulid1d |
⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) · 1 ) = ( exp ‘ 𝐴 ) ) |
15 |
12 14
|
sylan9eqr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( ( exp ‘ 𝐴 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( exp ‘ 𝐴 ) ) |
16 |
10 15
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( 𝐴 + ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( exp ‘ 𝐴 ) ) |