x : ℝ
hx : abs' x ≤ 1
n : ℕ
hn : 0 < n
hxc : ↑Complex.abs ↑x ≤ 1
⊢ abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ abs' x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
x : ℝ
hx : abs' x ≤ 1
n : ℕ
hn : 0 < n
⊢ abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ abs' x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
have hxc : Complex.abs x ≤ 1 := by exact_mod_cast hx
no goals
x : ℝ
hx : abs' x ≤ 1
n : ℕ
hn : 0 < n
hxc : ↑Complex.abs ↑x ≤ 1
⊢ abs' (exp x - ∑ m in range n, x ^ m / ↑(Nat.factorial m)) ≤ abs' x ^ n * (↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n))
convert exp_bound hxc hn using 2 <;>
simp only [← abs_ofReal, ← ofReal_sub, ← ofReal_exp, ← ofReal_sum, ← ofReal_pow,
  ← ofReal_div, ← ofReal_nat_cast]
no goals
x : ℝ
hx : abs' x ≤ 1
n : ℕ
hn : 0 < n
⊢ ↑Complex.abs ↑x ≤ 1
exact_mod_cast hx