Theorem ef2kpi

Description: If K is an integer, then the exponential of 2 Kpi i is 1 . (Contributed by Mario Carneiro, 9-May-2014)

	Ref	Expression
Assertion	ef2kpi	⊢ ( 𝐾 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) = 1 )

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		mulcom	⊢ ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · 𝐾 ) = ( 𝐾 · ( i · ( 2 · π ) ) ) )
8	5 6 7	sylancr	⊢ ( 𝐾 ∈ ℤ → ( ( i · ( 2 · π ) ) · 𝐾 ) = ( 𝐾 · ( i · ( 2 · π ) ) ) )
9	8	fveq2d	⊢ ( 𝐾 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) = ( exp ‘ ( 𝐾 · ( i · ( 2 · π ) ) ) ) )
10		efexp	⊢ ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( 𝐾 · ( i · ( 2 · π ) ) ) ) = ( ( exp ‘ ( i · ( 2 · π ) ) ) ↑ 𝐾 ) )
11	5 10	mpan	⊢ ( 𝐾 ∈ ℤ → ( exp ‘ ( 𝐾 · ( i · ( 2 · π ) ) ) ) = ( ( exp ‘ ( i · ( 2 · π ) ) ) ↑ 𝐾 ) )
12		ef2pi	⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = 1
13	12	oveq1i	⊢ ( ( exp ‘ ( i · ( 2 · π ) ) ) ↑ 𝐾 ) = ( 1 ↑ 𝐾 )
14		1exp	⊢ ( 𝐾 ∈ ℤ → ( 1 ↑ 𝐾 ) = 1 )
15	13 14	eqtrid	⊢ ( 𝐾 ∈ ℤ → ( ( exp ‘ ( i · ( 2 · π ) ) ) ↑ 𝐾 ) = 1 )
16	9 11 15	3eqtrd	⊢ ( 𝐾 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐾 ) ) = 1 )