x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x
suffices im (log x * (n⁻¹ : ℂ)) ∈ Ioc (-π) π by
  rw [← cpow_nat_cast, ← cpow_mul _ this.1 this.2, inv_mul_cancel, cpow_one]
  exact_mod_cast hn
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
rw [mul_comm, ← ofReal_nat_cast, ← ofReal_inv, ofReal_mul_im, ← div_eq_inv_mul]
x : ℂ
n : ℕ
hn : 0 < n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
rw [← pos_iff_ne_zero] at hn
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
x : ℂ
n : ℕ
hn : 0 < n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
have hn' : 0 < (n : ℝ) := by assumption_mod_cast
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
have hn1 : 1 ≤ (n : ℝ) := by exact_mod_cast Nat.succ_le_iff.2 hn
case left
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ -π < (log x).im / ↑n

case right
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im / ↑n ≤ π
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im / ↑n ∈ Set.Ioc (-π) π
constructor
x : ℂ
n : ℕ
hn : n ≠ 0
this : (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
⊢ ↑n ≠ 0
x : ℂ
n : ℕ
hn : n ≠ 0
this : (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
⊢ (x ^ (↑n)⁻¹) ^ n = x
rw [← cpow_nat_cast, ← cpow_mul _ this.1 this.2, inv_mul_cancel, cpow_one]
no goals
x : ℂ
n : ℕ
hn : n ≠ 0
this : (log x * (↑n)⁻¹).im ∈ Set.Ioc (-π) π
⊢ ↑n ≠ 0
exact_mod_cast hn
no goals
x : ℂ
n : ℕ
hn : 0 < n
⊢ 0 < ↑n
assumption_mod_cast
no goals
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ 1 ≤ ↑n
exact_mod_cast Nat.succ_le_iff.2 hn
case left
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ -π * ↑n < (log x).im
case left
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ -π < (log x).im / ↑n
rw [lt_div_iff hn']
no goals
case left
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ -π * ↑n < (log x).im
calc
  -π * n ≤ -π * 1 := mul_le_mul_of_nonpos_left hn1 (neg_nonpos.2 Real.pi_pos.le)
  _ = -π := (mul_one _)
  _ < im (log x) := neg_pi_lt_log_im _
case right
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im ≤ π * ↑n
case right
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im / ↑n ≤ π
rw [div_le_iff hn']
no goals
case right
x : ℂ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
hn1 : 1 ≤ ↑n
⊢ (log x).im ≤ π * ↑n
calc
  im (log x) ≤ π := log_im_le_pi _
  _ = π * 1 := (mul_one π).symm
  _ ≤ π * n := mul_le_mul_of_nonneg_left hn1 Real.pi_pos.le