have s_ne_one : σ + t * I ≠ 1 := by
  contrapose! σ_gt; apply le_of_eq; apply And.left; simpa [Complex.ext_iff] using σ_gt
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
σ t : ℝ
σ_gt : 1 < σ
s_ne_one : ↑σ + ↑t * I ≠ 1
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖