apply HasDerivAt.sum ?_ |>.add ?_ |>.add ?_ |>.add ?_
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt
    (fun s =>
      ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1))
    (∑ n ∈ Finset.range (N + 1), -1 / ↑n ^ s * ↑(↑n).log +
          (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) +
        ↑(↑N).log * ↑N ^ (-s) / 2 +
      ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
        s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log))
    s
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ∀ i ∈ Finset.range (N + 1), HasDerivAt (fun x => 1 / ↑i ^ x) (-1 / ↑i ^ s * ↑(↑i).log) s

N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (1 - x) / (1 - x)) (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) s

N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (-x) / 2) (↑(↑N).log * ↑N ^ (-s) / 2) s

N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => x * ∫ (x_1 : ℝ) in Ioi ↑N, (↑⌊x_1⌋ + 1 / 2 - ↑x_1) / ↑x_1 ^ (x + 1))
    ((1 * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1)) +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-s - 1) * -↑x.log)
    s