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

Metamath Proof Explorer

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