Theorem: sum_eq_int_deriv
Proof state before:
φ : ℝ → ℂ
a b : ℝ
a_lt_b : a < b
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
P : ℝ → ℝ → Prop :=
  fun a₁ b₁ =>
    (∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x) →
      ContinuousOn (deriv φ) [[a₁, b₁]] →
        ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊b₁⌋, φ ↑n =
          (∫ (x : ℝ) in a₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
            ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
a₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
⊢ I₂ + I₃ = I₁
Tactic:
apply intervalIntegral.integral_add_adjacent_intervals <;>
apply (HasDerivAt.continuousOn <| fun x hx ↦ φDiff₁ x ?_ ).intervalIntegrable
Proof state after:
φ : ℝ → ℂ
a b : ℝ
a_lt_b : a < b
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
P : ℝ → ℝ → Prop :=
  fun a₁ b₁ =>
    (∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x) →
      ContinuousOn (deriv φ) [[a₁, b₁]] →
        ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊b₁⌋, φ ↑n =
          (∫ (x : ℝ) in a₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
            ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
a₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
x : ℝ
hx : x ∈ [[a₁, ↑k₁]]
⊢ x ∈ [[a₁, b₁]]

φ : ℝ → ℂ
a b : ℝ
a_lt_b : a < b
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
P : ℝ → ℝ → Prop :=
  fun a₁ b₁ =>
    (∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x) →
      ContinuousOn (deriv φ) [[a₁, b₁]] →
        ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊b₁⌋, φ ↑n =
          (∫ (x : ℝ) in a₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
            ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
a₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
x : ℝ
hx : x ∈ [[↑k₁, b₁]]
⊢ x ∈ [[a₁, b₁]]