apply intervalIntegral.integral_deriv_eq_sub'
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I) = ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)
case hderiv
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ (deriv fun {σ₂} => ζ (↑σ₂ + ↑t * I)) = fun y => deriv ζ (↑y + ↑t * I)

case hdiff
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∀ x ∈ [[σ₁, σ₂]], DifferentiableAt ℝ (fun {σ₂} => ζ (↑σ₂ + ↑t * I)) x

case hcont
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => deriv ζ (↑y + ↑t * I)) [[σ₁, σ₂]]