[STATEMENT]
lemma euler_60_decimals:
  "\<bar>exp 1 - 2.718281828459045235360287471352662497757247093699959574966968\<bar> 
      \<le> inverse (10^60::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>exp 1 - 2718281828459045235360287471352662497757247093699959574966968 / 10 ^ 60\<bar> \<le> inverse (10 ^ 60)
[PROOF STEP]
by (rule approx_coarsen, rule exp_1_approx[of 48])
     (simp_all add: eval_euler_approx eval_fact)