rw [Asymptotics.isBigO_iff] at this
this : (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
this : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 1, ‖ζ ↑x‖ ≤ c * ‖1 / (↑x - 1)‖
⊢ ∃ c, ∃ (_ : 0 < c), ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)