[STATEMENT]
lemma exp_approx'':
  assumes "n > 0" "0 \<le> x" "x \<le> 1"
  shows   "\<bar>exp (x::real) - (\<Sum>k\<le>n. x^k / fact k)\<bar> \<le> 1 / fact n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
0 \<le> x
x \<le> 1
[PROOF STEP]
have "\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> x ^ n / fact n"
[PROOF STATE]
proof (prove)
using this:
0 < n
0 \<le> x
x \<le> 1

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> x ^ n / fact n
[PROOF STEP]
by (rule exp_approx')
[PROOF STATE]
proof (state)
this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> x ^ n / fact n

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> x ^ n / fact n

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
0 \<le> x
x \<le> 1
[PROOF STEP]
have "\<dots> \<le> 1 / fact n"
[PROOF STATE]
proof (prove)
using this:
0 < n
0 \<le> x
x \<le> 1

goal (1 subgoal):
 1. x ^ n / fact n \<le> 1 / fact n
[PROOF STEP]
by (simp add: field_split_simps power_le_one)
[PROOF STATE]
proof (state)
this:
x ^ n / fact n \<le> 1 / fact n

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n

goal (1 subgoal):
 1. \<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>exp x - (\<Sum>k\<le>n. x ^ k / fact k)\<bar> \<le> 1 / fact n

goal:
No subgoals!
[PROOF STEP]
qed