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

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 mulridd ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) · 1 ) = ( exp ‘ 𝐴 ) )
15 12 14 sylan9eqr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( ( exp ‘ 𝐴 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( exp ‘ 𝐴 ) )
16 10 15 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( 𝐴 + ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( exp ‘ 𝐴 ) )