Metamath Proof Explorer


Theorem efper

Description: The exponential function is periodic. (Contributed by Paul Chapman, 21-Apr-2008) (Proof shortened by Mario Carneiro, 10-May-2014)

Ref Expression
Assertion efper ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( 𝐴 + ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( exp ‘ 𝐴 ) )

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