simp [U, s_ne_one, reS_pos]
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ s ∈ {z | z ≠ 1 ∧ 0 < z.re}
no goals