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