n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : abs' x ≤ 1
⊢ abs' (exp x - ∑ m in range m, x ^ m / ↑(Nat.factorial m)) ≤ abs' x ^ m / ↑(Nat.factorial m) * ((↑m + 1) / ↑m)
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : abs' x ≤ 1
⊢ abs' (exp x - expNear m x 0) ≤ abs' x ^ m / ↑(Nat.factorial m) * ((↑m + 1) / ↑m)
simp [expNear]
case h.e'_4
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : abs' x ≤ 1
⊢ abs' x ^ m / ↑(Nat.factorial m) * ((↑m + 1) / ↑m) = abs' x ^ m * (↑(Nat.succ m) / (↑(Nat.factorial m) * ↑m))

n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : abs' x ≤ 1
⊢ 0 < m
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : abs' x ≤ 1
⊢ abs' (exp x - ∑ m in range m, x ^ m / ↑(Nat.factorial m)) ≤ abs' x ^ m / ↑(Nat.factorial m) * ((↑m + 1) / ↑m)
convert exp_bound (n := m) h ?_ using 1
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : abs' x ≤ 1
⊢ 0 < m
case h.e'_4
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : abs' x ≤ 1
⊢ abs' x ^ m / ↑(Nat.factorial m) * ((↑m + 1) / ↑m) = abs' x ^ m * (↑(Nat.succ m) / (↑(Nat.factorial m) * ↑m))

n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : abs' x ≤ 1
⊢ 0 < m
field_simp [mul_comm]
no goals
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : abs' x ≤ 1
⊢ 0 < m
linarith