internlm/Lean-Github huggingface dataset:
Theorem: sum_eq_int_deriv
Proof state before:
case h.e'_3
φ : ℝ → ℂ
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₃
hI : I₂ + I₃ = I₁
hJ : J₂ + J₃ = J₁
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₁ =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂ +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃)
Tactic:
rw [← hI, ← hJ]
Proof state after:
case h.e'_3
φ : ℝ → ℂ
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₃
hI : I₂ + I₃ = I₁
hJ : J₂ + J₃ = J₁
⊢ I₂ + I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - (J₂ + J₃) =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂ +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃)
Theorem: sum_eq_int_deriv
Proof state before:
case h.e'_3
φ : ℝ → ℂ
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₃
hI : I₂ + I₃ = I₁
hJ : J₂ + J₃ = J₁
⊢ I₂ + I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - (J₂ + J₃) =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂ +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃)
Tactic:
ring
Proof state after:
no goals
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₃
x : ℝ
hx : x ∈ [[a₁, ↑k₁]]
⊢ x ∈ [[a₁, b₁]]
Tactic:
exact subs.1 hx
Proof state after:
no goals
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₃
x : ℝ
hx : x ∈ [[↑k₁, b₁]]
⊢ x ∈ [[a₁, b₁]]
Tactic:
exact subs.2 hx
Proof state after:
no goals
Theorem: sum_eq_int_deriv
Proof state before:
case hab
φ : ℝ → ℂ
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₃
hI : I₂ + I₃ = I₁
⊢ [[a₁, ↑k₁]] ⊆ [[a₁, b₁]]
Tactic:
exact subs.1
Proof state after:
no goals
Theorem: sum_eq_int_deriv
Proof state before:
case hbc
φ : ℝ → ℂ
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₃
hI : I₂ + I₃ = I₁
⊢ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
Tactic:
exact subs.2
Proof state after:
no goals
Theorem: xpos_of_uIcc
Proof state before:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : x ∈ [[↑a, ↑b]]
⊢ 0 < x
Tactic:
rw [uIcc_of_le (by exact_mod_cast ha.2.le), mem_Icc] at x_in
Proof state after:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : ↑a ≤ x ∧ x ≤ ↑b
⊢ 0 < x
Theorem: xpos_of_uIcc
Proof state before:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : ↑a ≤ x ∧ x ≤ ↑b
⊢ 0 < x
Tactic:
linarith [(by exact_mod_cast ha.1 : (0 : ℝ) < a)]
Proof state after:
no goals
Theorem: xpos_of_uIcc
Proof state before:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : x ∈ [[↑a, ↑b]]
⊢ ↑a ≤ ↑b
Tactic:
exact_mod_cast ha.2.le
Proof state after:
no goals
Theorem: xpos_of_uIcc
Proof state before:
a b : ℕ
ha : a ∈ Ioo 0 b
x : ℝ
x_in : ↑a ≤ x ∧ x ≤ ↑b
⊢ 0 < ↑a
Tactic:
exact_mod_cast ha.1
Proof state after:
no goals
Theorem: ZetaSum_aux1₁
Proof state before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ ∫ (x : ℝ) in ↑a..↑b, 1 / ↑x ^ s = (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s)
Tactic:
convert integral_cpow (a := a) (b := b) (r := -s) ?_ using 1
Proof state after:
case h.e'_2
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ ∫ (x : ℝ) in ↑a..↑b, 1 / ↑x ^ s = ∫ (x : ℝ) in ↑a..↑b, ↑x ^ (-s)

case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) = (↑↑b ^ (-s + 1) - ↑↑a ^ (-s + 1)) / (-s + 1)

a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ -1 < (-s).re ∨ -s ≠ -1 ∧ 0 ∉ [[↑a, ↑b]]
Theorem: ZetaSum_aux1₁
Proof state before:
case h.e'_2
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ ∫ (x : ℝ) in ↑a..↑b, 1 / ↑x ^ s = ∫ (x : ℝ) in ↑a..↑b, ↑x ^ (-s)
Tactic:
refine intervalIntegral.integral_congr fun x hx ↦ one_div_cpow_eq ?_
Proof state after:
case h.e'_2
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
x : ℝ
hx : x ∈ [[↑a, ↑b]]
⊢ x ≠ 0
Theorem: ZetaSum_aux1₁
Proof state before:
case h.e'_2
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
x : ℝ
hx : x ∈ [[↑a, ↑b]]
⊢ x ≠ 0
Tactic:
exact (xpos_of_uIcc ha hx).ne'
Proof state after:
no goals
Theorem: ZetaSum_aux1₁
Proof state before:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) = (↑↑b ^ (-s + 1) - ↑↑a ^ (-s + 1)) / (-s + 1)
Tactic:
norm_cast
Proof state after:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) = (↑b ^ (-s + 1) - ↑a ^ (-s + 1)) / (-s + 1)
Theorem: ZetaSum_aux1₁
Proof state before:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) = (↑b ^ (-s + 1) - ↑a ^ (-s + 1)) / (-s + 1)
Tactic:
rw [(by ring : -s + 1 = 1 - s)]
Proof state after:
no goals
Theorem: ZetaSum_aux1₁
Proof state before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ -s + 1 = 1 - s
Tactic:
ring
Proof state after:
no goals
Theorem: ZetaSum_aux1₁
Proof state before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ -1 < (-s).re ∨ -s ≠ -1 ∧ 0 ∉ [[↑a, ↑b]]
Tactic:
right
Proof state after:
case h
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ -s ≠ -1 ∧ 0 ∉ [[↑a, ↑b]]
Theorem: ZetaSum_aux1₁
Proof state before:
case h
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ -s ≠ -1 ∧ 0 ∉ [[↑a, ↑b]]
Tactic:
refine ⟨neg_s_ne_neg_one s_ne_one, ?_⟩
Proof state after:
case h
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ 0 ∉ [[↑a, ↑b]]
Theorem: ZetaSum_aux1₁
Proof state before:
case h
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ 0 ∉ [[↑a, ↑b]]
Tactic:
exact fun hx ↦ (lt_self_iff_false 0).mp <| xpos_of_uIcc ha hx
Proof state after:
no goals
Theorem: ZetaSum_aux1φDiff
Proof state before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ HasDerivAt (fun t => 1 / ↑t ^ s) (deriv (fun t => 1 / ↑t ^ s) x) x
Tactic:
apply hasDerivAt_deriv_iff.mpr <| DifferentiableAt.div (differentiableAt_const _) ?_ ?_
Proof state after:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℝ (fun x => ↑x ^ s) x

s : ℂ
x : ℝ
xpos : 0 < x
⊢ ↑x ^ s ≠ 0
Theorem: ZetaSum_aux1φDiff
Proof state before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ DifferentiableAt ℝ (fun x => ↑x ^ s) x
Tactic:
exact Real.differentiableAt_cpow_const_of_ne s xpos
Proof state after:
no goals
Theorem: ZetaSum_aux1φDiff
Proof state before:
s : ℂ
x : ℝ
xpos : 0 < x
⊢ ↑x ^ s ≠ 0
Tactic:
simp [cpow_eq_zero_iff, xpos.ne']
Proof state after:
no goals
Theorem: ZetaSum_aux1φderiv
Proof state before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
let r := -s - 1
Proof state after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Theorem: ZetaSum_aux1φderiv
Proof state before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
have r_add1_ne_zero : r + 1 ≠ 0 := fun hr ↦ by simp [neg_ne_zero.mpr s_ne_zero, r] at hr
Proof state after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Theorem: ZetaSum_aux1φderiv
Proof state before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
have r_ne_neg1 : r ≠ -1 := fun hr ↦ (hr ▸ r_add1_ne_zero) <| by norm_num
Proof state after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Theorem: ZetaSum_aux1φderiv
Proof state before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
have hasDeriv := hasDerivAt_ofReal_cpow xpos.ne' r_ne_neg1
Proof state after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Theorem: ZetaSum_aux1φderiv
Proof state before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
have := hasDeriv.deriv ▸ deriv_const_mul (-s) (hasDeriv).differentiableAt
Proof state after:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Theorem: ZetaSum_aux1φderiv
Proof state before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ deriv (fun t => 1 / ↑t ^ s) x = (fun x => -s * ↑x ^ (-(s + 1))) x
Tactic:
convert this using 2
Proof state after:
case h.e'_2.h.e'_6
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ (fun t => 1 / ↑t ^ s) = fun y => -s * (↑y ^ (r + 1) / (r + 1))

case h.e'_3.h.e'_6
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ ↑x ^ (-(s + 1)) = ↑x ^ r
Theorem: ZetaSum_aux1φderiv
Proof state before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
hr : r + 1 = 0
⊢ False
Tactic:
simp [neg_ne_zero.mpr s_ne_zero, r] at hr
Proof state after:
no goals
Theorem: ZetaSum_aux1φderiv
Proof state before:
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
hr : r = -1
⊢ -1 + 1 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaSum_aux1φderiv
Proof state before:
case h.e'_2.h.e'_6
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ (fun t => 1 / ↑t ^ s) = fun y => -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
ext y
Proof state after:
case h.e'_2.h.e'_6.h
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Theorem: ZetaSum_aux1φderiv
Proof state before:
case h.e'_2.h.e'_6.h
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
by_cases y_zero : (y : ℂ) = 0
Proof state after:
case pos
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))

case neg
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ¬↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Theorem: ZetaSum_aux1φderiv
Proof state before:
case pos
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
simp only [y_zero, ofReal_zero, ne_eq, s_ne_zero, not_false_eq_true, zero_cpow, div_zero,
r_add1_ne_zero, zero_div, mul_zero]
Proof state after:
no goals
Theorem: ZetaSum_aux1φderiv
Proof state before:
case neg
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ¬↑y = 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
have : (y : ℂ) ^ s ≠ 0 := fun hy ↦ y_zero ((cpow_eq_zero_iff _ _).mp hy).1
Proof state after:
case neg
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this✝ : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ¬↑y = 0
this : ↑y ^ s ≠ 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Theorem: ZetaSum_aux1φderiv
Proof state before:
case neg
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this✝ : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
y : ℝ
y_zero : ¬↑y = 0
this : ↑y ^ s ≠ 0
⊢ 1 / ↑y ^ s = -s * (↑y ^ (r + 1) / (r + 1))
Tactic:
field_simp [r, mul_assoc, ← Complex.cpow_add]
Proof state after:
no goals
Theorem: ZetaSum_aux1φderiv
Proof state before:
case h.e'_3.h.e'_6
s : ℂ
s_ne_zero : s ≠ 0
x : ℝ
xpos : 0 < x
r : ℂ := -s - 1
r_add1_ne_zero : r + 1 ≠ 0
r_ne_neg1 : r ≠ -1
hasDeriv : HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
this : deriv (fun y => -s * (↑y ^ (r + 1) / (r + 1))) x = -s * ↑x ^ r
⊢ ↑x ^ (-(s + 1)) = ↑x ^ r
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ZetaSum_aux1derivφCont
Proof 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
Proof 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]]
Theorem: ZetaSum_aux1derivφCont
Proof 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
Proof 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
Theorem: ZetaSum_aux1derivφCont
Proof 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
Proof state after:
no goals