ring_nf
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
x : ℝ
hx : x ∈ [[↑a, ↑b]]
⊢ s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1))) = -((↑⌊x⌋ + 2⁻¹ - ↑x) * (-s * ↑x ^ (-(s + 1))))
no goals