Theorem: ZetaSum_aux1_5b (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => 1 / u ^ (s.re + 1)) MeasureTheory.volume a b
Tactic:
refine continuousOn_const.div ?_ ?_ |>.intervalIntegrable_of_Icc (le_of_lt a_lt_b)
State after:
case refine_1
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ContinuousOn (fun u => u ^ (s.re + 1)) (Icc a b)

case refine_2
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∀ x ∈ Icc a b, x ^ (s.re + 1) ≠ 0

State before:
case refine_1
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ContinuousOn (fun u => u ^ (s.re + 1)) (Icc a b)
Tactic:
exact continuousOn_id.rpow_const fun x hx ↦ Or.inl (ne_of_gt <| ZetaSum_aux1_1' apos hx)
State after:
no goals

State before:
case refine_2
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∀ x ∈ Icc a b, x ^ (s.re + 1) ≠ 0
Tactic:
exact fun x hx h ↦ by rw [Real.rpow_eq_zero] at h <;> linarith [ZetaSum_aux1_1' apos hx]
State after:
no goals

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
x : ℝ
hx : x ∈ Icc a b
h : x ^ (s.re + 1) = 0
⊢ False
Tactic:
rw [Real.rpow_eq_zero] at h <;> linarith [ZetaSum_aux1_1' apos hx]
State after:
no goals