ZetaSum_aux1φderiv

lemma ZetaSum_aux1φderiv {s : ℂ} (s_ne_zero : s ≠ 0) {x : ℝ} (xpos : 0 < x) :    deriv (fun (t : ℝ) ↦ 1 / (t : ℂ) ^ s) x = (fun (x : ℝ) ↦ -s * (x : ℂ) ^ (-(s + 1))) x := by  let r := -s - 1  have r_add1_ne_zero : r + 1 ≠ 0 := fun hr ↦ by simp [neg_ne_zero.mpr s_ne_zero, r] at hr  have r_ne_neg1 : r ≠ -1 := fun hr ↦ (hr ▸ r_add1_ne_zero) <| by norm_num  have hasDeriv := hasDerivAt_ofReal_cpow_const' xpos.ne' r_ne_neg1  have := hasDeriv.deriv ▸ deriv_const_mul (-s) (hasDeriv).differentiableAt  convert! this using 2  · ext y    by_cases y_zero : (y : ℂ) = 0    · simp only [y_zero, ne_eq, s_ne_zero, not_false_eq_true, zero_cpow, div_zero,      r_add1_ne_zero, zero_div, mul_zero]    · have : (y : ℂ) ^ s ≠ 0 := fun hy ↦ y_zero ((cpow_eq_zero_iff _ _).mp hy).1      simp only [one_div, sub_add_cancel, cpow_neg, neg_mul, r]      field_simp  · simp only [r]    ring_nf