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	$⊢ (A \in ℂ \land K \in ℤ) \to e^{A + i 2 π K} = e^{A}$

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		2cn	$⊢ 2 \in ℂ$
3		picn	$⊢ π \in ℂ$
4	2 3	mulcli	$⊢ 2 π \in ℂ$
5	1 4	mulcli	$⊢ i 2 π \in ℂ$
6		zcn	$⊢ K \in ℤ \to K \in ℂ$
7		mulcl	$⊢ (i 2 π \in ℂ \land K \in ℂ) \to i 2 π K \in ℂ$
8	5 6 7	sylancr	$⊢ K \in ℤ \to i 2 π K \in ℂ$
9		efadd	$⊢ (A \in ℂ \land i 2 π K \in ℂ) \to e^{A + i 2 π K} = e^{A} e^{i 2 π K}$
10	8 9	sylan2	$⊢ (A \in ℂ \land K \in ℤ) \to e^{A + i 2 π K} = e^{A} e^{i 2 π K}$
11		ef2kpi	$⊢ K \in ℤ \to e^{i 2 π K} = 1$
12	11	oveq2d	$⊢ K \in ℤ \to e^{A} e^{i 2 π K} = e^{A} \cdot 1$
13		efcl	$⊢ A \in ℂ \to e^{A} \in ℂ$
14	13	mulid1d	$⊢ A \in ℂ \to e^{A} \cdot 1 = e^{A}$
15	12 14	sylan9eqr	$⊢ (A \in ℂ \land K \in ℤ) \to e^{A} e^{i 2 π K} = e^{A}$
16	10 15	eqtrd	$⊢ (A \in ℂ \land K \in ℤ) \to e^{A + i 2 π K} = e^{A}$

Metamath Proof Explorer