Theorem: ZetaSum_aux1derivφCont (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
s : ℂ
s_ne_zero : s ≠ 0
a b : ℕ
ha : a ∈ Ioo 0 b
⊢ ContinuousOn (deriv fun t => 1 / ↑t ^ s) [[↑a, ↑b]]
Tactic:
have : EqOn _ (fun (t : ℝ) ↦ -s * (t : ℂ) ^ (-(s + 1))) [[a, b]] :=
  fun x hx ↦ ZetaSum_aux1φderiv s_ne_zero <| xpos_of_uIcc ha hx
State after:
s : ℂ
s_ne_zero : s ≠ 0
a b : ℕ
ha : a ∈ Ioo 0 b
this : EqOn (fun x => deriv (fun t => 1 / ↑t ^ s) x) (fun t => -s * ↑t ^ (-(s + 1))) [[↑a, ↑b]]
⊢ ContinuousOn (deriv fun t => 1 / ↑t ^ s) [[↑a, ↑b]]

State before:
s : ℂ
s_ne_zero : s ≠ 0
a b : ℕ
ha : a ∈ Ioo 0 b
this : EqOn (fun x => deriv (fun t => 1 / ↑t ^ s) x) (fun t => -s * ↑t ^ (-(s + 1))) [[↑a, ↑b]]
⊢ ContinuousOn (deriv fun t => 1 / ↑t ^ s) [[↑a, ↑b]]
Tactic:
refine continuous_ofReal.continuousOn.cpow_const ?_ |>.const_smul (c := -s) |>.congr this
State after:
s : ℂ
s_ne_zero : s ≠ 0
a b : ℕ
ha : a ∈ Ioo 0 b
this : EqOn (fun x => deriv (fun t => 1 / ↑t ^ s) x) (fun t => -s * ↑t ^ (-(s + 1))) [[↑a, ↑b]]
⊢ ∀ a_1 ∈ [[↑a, ↑b]], ↑a_1 ∈ slitPlane

State before:
s : ℂ
s_ne_zero : s ≠ 0
a b : ℕ
ha : a ∈ Ioo 0 b
this : EqOn (fun x => deriv (fun t => 1 / ↑t ^ s) x) (fun t => -s * ↑t ^ (-(s + 1))) [[↑a, ↑b]]
⊢ ∀ a_1 ∈ [[↑a, ↑b]], ↑a_1 ∈ slitPlane
Tactic:
exact fun x hx ↦ ofReal_mem_slitPlane.mpr <| xpos_of_uIcc ha hx
State after:
no goals