Zeta_eq_int_derivZeta

@[blueprint  (title := "Zeta-eq-int-derivZeta")  (statement := /--  For any $t\ne0$ (so we don't pass through the pole), and $\sigma_1 < \sigma_2$,  $$  \int_{\sigma_1}^{\sigma_2}\zeta'(\sigma + it) dt =  \zeta(\sigma_2+it) - \zeta(\sigma_1+it).  $$  -/)  (proof := /-- This is the fundamental theorem of calculus. -/)  (latexEnv := "lemma")]lemma Zeta_eq_int_derivZeta {σ₁ σ₂ t : ℝ} (t_ne_zero : t ≠ 0) :    (∫ σ in σ₁..σ₂, ζ' (σ + t * I)) = ζ (σ₂ + t * I) - ζ (σ₁ + t * I) := by  have diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (σ + t * I) := by    intro σ    refine differentiableAt_riemannZeta ?_    contrapose! t_ne_zero; apply And.right; simpa [Complex.ext_iff] using t_ne_zero  apply intervalIntegral.integral_deriv_eq_sub'  · exact deriv_fun_re diff  · intro s _    apply DifferentiableAt.comp    · exact (diff s).restrictScalars ℝ    · exact DifferentiableAt.add_const (c := t * I) <| differentiableAt_ofReal _  · apply ContinuousOn.comp (g := ζ') ?_ ?_ (mapsTo_image _ _)    · apply HasDerivAt.continuousOn (f' := deriv <| ζ')      intro x hx      apply hasDerivAt_deriv_iff.mpr      replace hx : x ≠ 1 := by        contrapose! hx        simp only [hx, mem_image, Complex.ext_iff, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im,          I_im, mul_one, sub_self, add_zero, one_re, add_im, mul_im, zero_add, one_im, not_exists,          not_and]        exact fun _ _ _ ↦ t_ne_zero      exact differentiableAt_deriv_riemannZeta hx    · exact continuous_ofReal.continuousOn.add continuousOn_const