rw [this, abs_eq_self.mpr <| Real.rpow_nonneg n_gt_0'.le _]
case neg.calc_1
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
this : ‖↑n ^ (-s)‖ = ↑n ^ (-s.re)
⊢ ‖↑n ^ (-s)‖ = |↑n ^ (-σ)|
case neg.calc_1
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
this : ‖↑n ^ (-s)‖ = ↑n ^ (-s.re)
⊢ ↑n ^ (-s.re) = ↑n ^ (-σ)