simp_rw [div_cpow_eq_cpow_neg, neg_add, ← sub_eq_add_neg]
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
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