iterate 2 (rw [abs_cpow_eq_rpow_re_of_pos (by linarith [hx.1])])
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1)) =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑t * I + 1).re =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑u * I + 1).re