183 also have "\<dots> / fact n = (\<Sum>k\<le>n. 1 / (fact n / (\<Prod>i=k+1..n. real i)))" |
183 also have "\<dots> / fact n = (\<Sum>k\<le>n. 1 / (fact n / (\<Prod>i=k+1..n. real i)))" |
184 by (simp add: setsum_divide_distrib) |
184 by (simp add: setsum_divide_distrib) |
185 also have "\<dots> = (\<Sum>k\<le>n. 1 / fact k)" |
185 also have "\<dots> = (\<Sum>k\<le>n. 1 / fact k)" |
186 proof (intro setsum.cong refl) |
186 proof (intro setsum.cong refl) |
187 fix k assume k: "k \<in> {..n}" |
187 fix k assume k: "k \<in> {..n}" |
188 have "fact n = (\<Prod>i=1..n. real i)" by (rule fact_altdef) |
188 have "fact n = (\<Prod>i=1..n. real i)" by (simp add: fact_setprod) |
189 also from k have "{1..n} = {1..k} \<union> {k+1..n}" by auto |
189 also from k have "{1..n} = {1..k} \<union> {k+1..n}" by auto |
190 also have "setprod real \<dots> / (\<Prod>i=k+1..n. real i) = (\<Prod>i=1..k. real i)" |
190 also have "setprod real \<dots> / (\<Prod>i=k+1..n. real i) = (\<Prod>i=1..k. real i)" |
191 by (subst nonzero_divide_eq_eq, simp, subst setprod.union_disjoint [symmetric]) auto |
191 by (subst nonzero_divide_eq_eq, simp, subst setprod.union_disjoint [symmetric]) auto |
192 also have "\<dots> = fact k" by (simp only: fact_altdef) |
192 also have "\<dots> = fact k" by (simp add: fact_setprod) |
193 finally show "1 / (fact n / setprod real {k + 1..n}) = 1 / fact k" by simp |
193 finally show "1 / (fact n / setprod real {k + 1..n}) = 1 / fact k" by simp |
194 qed |
194 qed |
195 also have "\<dots> = euler_approx n" by (simp add: euler_approx_def field_simps) |
195 also have "\<dots> = euler_approx n" by (simp add: euler_approx_def field_simps) |
196 finally show ?thesis by (simp add: euler_approx_aux_def) |
196 finally show ?thesis by (simp add: euler_approx_aux_def) |
197 qed |
197 qed |