a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = (↑b ^ (r + 1) - ↑a ^ (r + 1)) / (r + 1)
rw [sub_div]
case pos
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)

case neg
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
by_cases hab : (0 : ℝ) ∉ [[a, b]]
case h
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
⊢ -1 < r.re

case neg
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
case neg
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
replace h : -1 < r.re
case neg
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
⊢ ∀ (c : ℝ), (∫ (x : ℝ) in 0 ..c, ↑x ^ r) = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
case neg
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
suffices ∀ c : ℝ, (∫ x : ℝ in (0)..c, (x : ℂ) ^ r) =
    (c:ℂ) ^ (r + 1) / (r + 1) - (0:ℂ) ^ (r + 1) / (r + 1) by
  rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h)
    (@intervalIntegrable_cpow' 0 b r h), integral_symm, this a, this b, Complex.zero_cpow hr]
  ring
case neg
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ (∫ (x : ℝ) in 0 ..c, ↑x ^ r) = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
case neg
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
⊢ ∀ (c : ℝ), (∫ (x : ℝ) in 0 ..c, ↑x ^ r) = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
intro c
case neg.hcont
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ContinuousOn (fun c => ↑c ^ (r + 1) / (r + 1)) [[0, c]]

case neg.hderiv
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ (x : ℝ), x ∈ Set.Ioo (min 0 c) (max 0 c) → HasDerivWithinAt (fun c => ↑c ^ (r + 1) / (r + 1)) (↑x ^ r) (Set.Ioi x) x

case neg.hint
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (fun y => ↑y ^ r) MeasureTheory.volume 0 c
case neg
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ (∫ (x : ℝ) in 0 ..c, ↑x ^ r) = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
apply integral_eq_sub_of_hasDeriv_right
case inl
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re
⊢ r + 1 ≠ 0

case inr
a b : ℝ
n : ℕ
r : ℂ
h : r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ r + 1 ≠ 0
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ r + 1 ≠ 0
cases' h with h h
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re
⊢ (r + 1).re ≠ 0.re
case inl
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re
⊢ r + 1 ≠ 0
apply_fun Complex.re
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re
⊢ ¬r.re = -1
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re
⊢ (r + 1).re ≠ 0.re
rw [Complex.add_re, Complex.one_re, Complex.zero_re, Ne.def, add_eq_zero_iff_eq_neg]
no goals
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re
⊢ ¬r.re = -1
exact h.ne'
case inr
a b : ℝ
n : ℕ
r : ℂ
h : ¬r + 1 = 0 ∧ ¬0 ∈ [[a, b]]
⊢ r + 1 ≠ 0
case inr
a b : ℝ
n : ℕ
r : ℂ
h : r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ r + 1 ≠ 0
rw [Ne.def, ← add_eq_zero_iff_eq_neg] at h
no goals
case inr
a b : ℝ
n : ℕ
r : ℂ
h : ¬r + 1 = 0 ∧ ¬0 ∈ [[a, b]]
⊢ r + 1 ≠ 0
exact h.1
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b} => ↑b ^ (r + 1) / (r + 1)) (↑x ^ r) x
case pos
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
apply integral_eq_sub_of_hasDerivAt (fun x hx => ?_)
  (intervalIntegrable_cpow (r := r) <| Or.inr hab)
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ r ≠ -1
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b} => ↑b ^ (r + 1) / (r + 1)) (↑x ^ r) x
refine' hasDerivAt_ofReal_cpow (ne_of_mem_of_not_mem hx hab) _
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hab : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
hr : r = -1
⊢ r + 1 = 0
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ r ≠ -1
contrapose! hr
no goals
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hab : ¬0 ∈ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
hr : r = -1
⊢ r + 1 = 0
rwa [add_eq_zero_iff_eq_neg]
no goals
case h
a b : ℝ
n : ℕ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
⊢ -1 < r.re
tauto
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
this : ∀ (c : ℝ), (∫ (x : ℝ) in 0 ..c, ↑x ^ r) = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
⊢ -(↑a ^ (r + 1) / (r + 1) - 0 / (r + 1)) + (↑b ^ (r + 1) / (r + 1) - 0 / (r + 1)) =
    ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
this : ∀ (c : ℝ), (∫ (x : ℝ) in 0 ..c, ↑x ^ r) = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
⊢ (∫ (x : ℝ) in a..b, ↑x ^ r) = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
rw [← integral_add_adjacent_intervals (@intervalIntegrable_cpow' a 0 r h)
  (@intervalIntegrable_cpow' 0 b r h), integral_symm, this a, this b, Complex.zero_cpow hr]
no goals
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
this : ∀ (c : ℝ), (∫ (x : ℝ) in 0 ..c, ↑x ^ r) = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)
⊢ -(↑a ^ (r + 1) / (r + 1) - 0 / (r + 1)) + (↑b ^ (r + 1) / (r + 1) - 0 / (r + 1)) =
    ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)
ring
case neg.hcont
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ 0 < (r + 1).re
case neg.hcont
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ContinuousOn (fun c => ↑c ^ (r + 1) / (r + 1)) [[0, c]]
refine' ((Complex.continuous_ofReal_cpow_const _).div_const _).continuousOn
no goals
case neg.hcont
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ 0 < (r + 1).re
rwa [Complex.add_re, Complex.one_re, ← neg_lt_iff_pos_add]
case neg.hderiv.refine'_1
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ x ≠ 0

case neg.hderiv.refine'_2
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ r ≠ -1
case neg.hderiv
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ (x : ℝ), x ∈ Set.Ioo (min 0 c) (max 0 c) → HasDerivWithinAt (fun c => ↑c ^ (r + 1) / (r + 1)) (↑x ^ r) (Set.Ioi x) x
refine' fun x hx => (hasDerivAt_ofReal_cpow _ _).hasDerivWithinAt
case neg.hderiv.refine'_1.inl
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : c ≤ 0
⊢ x ≠ 0

case neg.hderiv.refine'_1.inr
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0
case neg.hderiv.refine'_1
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ x ≠ 0
rcases le_total c 0 with (hc | hc)
case neg.hderiv.refine'_1.inl
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) 0
hc : c ≤ 0
⊢ x ≠ 0
case neg.hderiv.refine'_1.inl
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : c ≤ 0
⊢ x ≠ 0
rw [max_eq_left hc] at hx
no goals
case neg.hderiv.refine'_1.inl
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) 0
hc : c ≤ 0
⊢ x ≠ 0
exact hx.2.ne
case neg.hderiv.refine'_1.inr
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo 0 (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0
case neg.hderiv.refine'_1.inr
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0
rw [min_eq_left hc] at hx
no goals
case neg.hderiv.refine'_1.inr
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo 0 (max 0 c)
hc : 0 ≤ c
⊢ x ≠ 0
exact hx.1.ne'
case neg.hderiv.refine'_2
a b : ℝ
n : ℕ
r : ℂ
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hr : r = -1
⊢ r + 1 = 0
case neg.hderiv.refine'_2
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
⊢ r ≠ -1
contrapose! hr
case neg.hderiv.refine'_2
a b : ℝ
n : ℕ
r : ℂ
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hr : r = -1
⊢ -1 + 1 = 0
case neg.hderiv.refine'_2
a b : ℝ
n : ℕ
r : ℂ
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hr : r = -1
⊢ r + 1 = 0
rw [hr]
no goals
case neg.hderiv.refine'_2
a b : ℝ
n : ℕ
r : ℂ
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) (max 0 c)
hr : r = -1
⊢ -1 + 1 = 0
ring
no goals
case neg.hint
a b : ℝ
n : ℕ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬¬0 ∈ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (fun y => ↑y ^ r) MeasureTheory.volume 0 c
exact intervalIntegrable_cpow' h