intro N
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
⊢ let N := ⌊|t|⌋₊;
  ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log