a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
⊢ (∫ (x : ℝ) in a..b, x⁻¹) = Real.log (b / a)
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, x⁻¹) = Real.log (b / a)
have h' := fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h
no goals
a b : ℝ
n : ℕ
h : ¬0 ∈ [[a, b]]
h' : ∀ (x : ℝ), x ∈ [[a, b]] → x ≠ 0
⊢ (∫ (x : ℝ) in a..b, x⁻¹) = Real.log (b / a)
rw [integral_deriv_eq_sub' _ deriv_log' (fun x hx => differentiableAt_log (h' x hx))
    (continuousOn_inv₀.mono <| subset_compl_singleton_iff.mpr h),
  log_div (h' b right_mem_uIcc) (h' a left_mem_uIcc)]