[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ HasDerivAt exp (exp x) x
[PROOFSTEP]
rw [hasDerivAt_iff_isLittleO_nhds_zero]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ (fun h => exp (x + h) - exp x - h • exp x) =o[𝓝 0] fun h => h
[PROOFSTEP]
have : (1 : ℕ) < 2 := by norm_num
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ 1 < 2
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ (fun h => exp (x + h) - exp x - h • exp x) =o[𝓝 0] fun h => h
[PROOFSTEP]
refine' (IsBigO.of_bound ‖exp x‖ _).trans_isLittleO (isLittleO_pow_id this)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖exp (x + x_1) - exp x - x_1 • exp x‖ ≤ ‖exp x‖ * ‖x_1 ^ 2‖
[PROOFSTEP]
filter_upwards [Metric.ball_mem_nhds (0 : ℂ) zero_lt_one]
[GOAL]
case h
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), a ∈ Metric.ball 0 1 → ‖exp (x + a) - exp x - a • exp x‖ ≤ ‖exp x‖ * ‖a ^ 2‖
[PROOFSTEP]
simp only [Metric.mem_ball, dist_zero_right, norm_pow]
[GOAL]
case h
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), ‖a‖ < 1 → ‖exp (x + a) - exp x - a • exp x‖ ≤ ‖exp x‖ * ‖a‖ ^ 2
[PROOFSTEP]
exact fun z hz => exp_bound_sq x z hz.le
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
⊢ deriv^[n + 1] exp = exp
[PROOFSTEP]
rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
⊢ ∀ {n : ℕ∞}, ContDiff 𝕜 n exp
[PROOFSTEP]
refine' @(contDiff_all_iff_nat.2 fun n => ?_)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
⊢ ContDiff 𝕜 (↑n) exp
[PROOFSTEP]
have : ContDiff ℂ (↑n) exp := by
  induction' n with n ihn
  · exact contDiff_zero.2 continuous_exp
  · rw [contDiff_succ_iff_deriv]
    use differentiable_exp
    rwa [deriv_exp]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
⊢ ContDiff ℂ (↑n) exp
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
⊢ ContDiff ℂ (↑Nat.zero) exp
[PROOFSTEP]
exact contDiff_zero.2 continuous_exp
[GOAL]
case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ ContDiff ℂ (↑(Nat.succ n)) exp
[PROOFSTEP]
rw [contDiff_succ_iff_deriv]
[GOAL]
case succ
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ Differentiable ℂ exp ∧ ContDiff ℂ (↑n) (deriv exp)
[PROOFSTEP]
use differentiable_exp
[GOAL]
case right
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
ihn : ContDiff ℂ (↑n) exp
⊢ ContDiff ℂ (↑n) (deriv exp)
[PROOFSTEP]
rwa [deriv_exp]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
n : ℕ
this : ContDiff ℂ (↑n) exp
⊢ ContDiff 𝕜 (↑n) exp
[PROOFSTEP]
exact this.restrict_scalars 𝕜
[GOAL]
x y z : ℝ
n : ℕ
⊢ deriv^[n + 1] exp = exp
[PROOFSTEP]
rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
