Theorem: ZetaSum_aux1₁ (PrimeNumberTheoremAnd/ZetaBounds.lean)

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
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]]

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 ?_
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

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'
State after:
no goals

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
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)

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)]
State after:
no goals

State before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ -s + 1 = 1 - s
Tactic:
ring
State after:
no goals

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
State after:
case h
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ -s ≠ -1 ∧ 0 ∉ [[↑a, ↑b]]

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, ?_⟩
State after:
case h
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
ha : a ∈ Ioo 0 b
⊢ 0 ∉ [[↑a, ↑b]]

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
State after:
no goals