have : ‖(n : ℂ) ^ (-s)‖ = n ^ (-s.re) := abs_cpow_eq_rpow_re_of_pos n_gt_0' (-s)
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
⊢ ‖↑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)‖ = |↑n ^ (-σ)|