apply mul_le_mul ?_ (ZetaBnd_aux1b N Npos hσ.1) (norm_nonneg _) (by positivity)
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ * ‖∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ 2 * |t| * (↑N ^ (-σ) / σ)
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ ≤ 2 * |t|