case mp
x : ℂ
⊢ exp x = 1 → ∃ n, x = ↑n * (2 * ↑π * I)

case mpr
x : ℂ
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) → exp x = 1
x : ℂ
⊢ exp x = 1 ↔ ∃ n, x = ↑n * (2 * ↑π * I)
constructor
case mp
x : ℂ
h : exp x = 1
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
case mp
x : ℂ
⊢ exp x = 1 → ∃ n, x = ↑n * (2 * ↑π * I)
intro h
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
case mp
x : ℂ
h : exp x = 1
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos x.im (-π) with ⟨n, hn, -⟩
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x = ↑(-n) * (2 * ↑π * I)
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
use -n
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x + ↑n * (2 * ↑π * I) = 0
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x = ↑(-n) * (2 * ↑π * I)
rw [Int.cast_neg, neg_mul, eq_neg_iff_add_eq_zero]
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π
⊢ x + ↑n * (2 * ↑π * I) = 0
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x + ↑n * (2 * ↑π * I) = 0
have : (x + n * (2 * π * I)).im ∈ Set.Ioc (-π) π := by simpa [two_mul, mul_add] using hn
no goals
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π
⊢ x + ↑n * (2 * ↑π * I) = 0
rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]
no goals
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π
simpa [two_mul, mul_add] using hn
case mpr.intro
n : ℤ
⊢ exp (↑n * (2 * ↑π * I)) = 1
case mpr
x : ℂ
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) → exp x = 1
rintro ⟨n, rfl⟩
no goals
case mpr.intro
n : ℤ
⊢ exp (↑n * (2 * ↑π * I)) = 1
exact (exp_periodic.int_mul n).eq.trans exp_zero