a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ (∫ (x : ℝ) in a..b, Complex.exp (c * ↑x)) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
⊢ (∫ (x : ℝ) in a..b, Complex.exp (c * ↑x)) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
have D : ∀ x : ℝ, HasDerivAt (fun y : ℝ => Complex.exp (c * y) / c) (Complex.exp (c * x)) x := by
  intro x
  conv => congr
  rw [← mul_div_cancel (Complex.exp (c * x)) hc]
  apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
  simpa only [mul_one] using ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ Complex.exp (c * ↑b) / c - Complex.exp (c * ↑a) / c = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c

a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ContinuousOn (fun x => Complex.exp (c * ↑x)) [[a, b]]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ (∫ (x : ℝ) in a..b, Complex.exp (c * ↑x)) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
rw [integral_deriv_eq_sub' _ (funext fun x => (D x).deriv) fun x _ => (D x).differentiableAt]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
⊢ ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
intro x
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
conv => congr
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x) * c / c) x
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
rw [← mul_div_cancel (Complex.exp (c * x)) hc]
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun x => c * ↑x) c x
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x) * c / c) x
apply ((Complex.hasDerivAt_exp _).comp x _).div_const c
no goals
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
x : ℝ
⊢ HasDerivAt (fun x => c * ↑x) c x
simpa only [mul_one] using ((hasDerivAt_id (x : ℂ)).const_mul _).comp_ofReal
no goals
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ Complex.exp (c * ↑b) / c - Complex.exp (c * ↑a) / c = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
ring
case h
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ Continuous fun x => Complex.exp (c * ↑x)
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ ContinuousOn (fun x => Complex.exp (c * ↑x)) [[a, b]]
apply Continuous.continuousOn
no goals
case h
a b : ℝ
n : ℕ
c : ℂ
hc : c ≠ 0
D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x
⊢ Continuous fun x => Complex.exp (c * ↑x)
continuity