a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r) = (↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)
⊢ (∫ (x : ℝ) in a..b, x ^ r) = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, x ^ r) = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
have :
  (∫ x in a..b, (x : ℂ) ^ (r : ℂ)) = ((b : ℂ) ^ (r + 1 : ℂ) - (a : ℂ) ^ (r + 1 : ℂ)) / (r + 1) :=
  integral_cpow h'
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (∫ (x : ℝ) in a..b, x ^ r) = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r) = (↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)
⊢ (∫ (x : ℝ) in a..b, x ^ r) = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
apply_fun Complex.re at this
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (∫ (x : ℝ) in a..b, x ^ r) = (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re

case h.e'_3
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (∫ (x : ℝ) in a..b, x ^ r) = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
convert this
case inl
a b : ℝ
n : ℕ
r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]

case inr
a b : ℝ
n : ℕ
r : ℝ
h✝ : r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
cases h
case inl.h
a b : ℝ
n : ℕ
r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re
case inl
a b : ℝ
n : ℕ
r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
left
no goals
case inl.h
a b : ℝ
n : ℕ
r : ℝ
h✝ : -1 < r
⊢ -1 < (↑r).re
rwa [Complex.ofReal_re]
case inr.h
a b : ℝ
n : ℕ
r : ℝ
h✝ : r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
case inr
a b : ℝ
n : ℕ
r : ℝ
h✝ : r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
right
no goals
case inr.h
a b : ℝ
n : ℕ
r : ℝ
h✝ : r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
rwa [← Complex.ofReal_one, ← Complex.ofReal_neg, Ne.def, Complex.ofReal_inj]
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r) = (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r).re
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (∫ (x : ℝ) in a..b, x ^ r) = (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re
simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.ofReal_mul_re]
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r) = (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r).re
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r) = (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r).re
have : Complex.re = IsROrC.re := by rfl
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r) =
    (if a ≤ b then 1 else -1) * ∫ (a : ℝ) in Ι a b, ↑IsROrC.re (↑a ^ ↑r)

case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ MeasureTheory.Integrable fun x => ↑x ^ ↑r
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r) = (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r).re
rw [this, ← integral_re]
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ MeasureTheory.Integrable fun x => ↑x ^ ↑r
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r) =
    (if a ≤ b then 1 else -1) * ∫ (a : ℝ) in Ι a b, ↑IsROrC.re (↑a ^ ↑r)

case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ MeasureTheory.Integrable fun x => ↑x ^ ↑r
rfl
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ MeasureTheory.Integrable fun x => ↑x ^ ↑r
refine' intervalIntegrable_iff.mp _
case h.e'_2.inl
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
h' : -1 < (↑r).re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b

case h.e'_2.inr
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
h' : ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b
case h.e'_2
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b
cases' h' with h' h'
no goals
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ Complex.re = ↑IsROrC.re
rfl
no goals
case h.e'_2.inl
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
h' : -1 < (↑r).re
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b
exact intervalIntegrable_cpow' h'
no goals
case h.e'_2.inr
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this✝ : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
this : Complex.re = ↑IsROrC.re
h' : ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ IntervalIntegrable (fun x => ↑x ^ ↑r) MeasureTheory.volume a b
exact intervalIntegrable_cpow (Or.inr h'.2)
case h.e'_3
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ ↑(r + 1) - ↑a ^ ↑(r + 1)) / ↑(r + 1)).re
case h.e'_3
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
rw [(by push_cast; rfl : (r : ℂ) + 1 = ((r + 1 : ℝ) : ℂ))]
case h.e'_3
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * ((↑b ^ ↑(r + 1)).re - (↑a ^ ↑(r + 1)).re)
case h.e'_3
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) = ((↑b ^ ↑(r + 1) - ↑a ^ ↑(r + 1)) / ↑(r + 1)).re
simp_rw [div_eq_inv_mul, ← Complex.ofReal_inv, Complex.ofReal_mul_re, Complex.sub_re]
no goals
case h.e'_3
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (r + 1)⁻¹ * (b ^ (r + 1) - a ^ (r + 1)) = (r + 1)⁻¹ * ((↑b ^ ↑(r + 1)).re - (↑a ^ ↑(r + 1)).re)
rfl
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ↑r + 1 = ↑r + 1
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ↑r + 1 = ↑(r + 1)
push_cast
no goals
a b : ℝ
n : ℕ
r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ ¬0 ∈ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ ¬0 ∈ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ ↑r + 1 = ↑r + 1
rfl