src/HOL/Analysis/Gamma_Function.thy
changeset 65578 e4997c181cce
parent 64969 a6953714799d
child 65587 16a8991ab398
     1.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Tue Apr 25 08:38:23 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Tue Apr 25 16:39:54 2017 +0100
     1.3 @@ -1880,7 +1880,7 @@
     1.4    show "G x \<ge> Gamma x"
     1.5    proof (rule tendsto_upperbound)
     1.6      from G_lower[of x] show "eventually (\<lambda>n. Gamma_series x n \<le> G x) sequentially"
     1.7 -      using eventually_ge_at_top[of "1::nat"] x by (auto elim!: eventually_mono)
     1.8 +      using  x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "1::nat"]])
     1.9    qed (simp_all add: Gamma_series_LIMSEQ)
    1.10  next
    1.11    show "G x \<le> Gamma x"
    1.12 @@ -1891,7 +1891,7 @@
    1.13      thus "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x" by simp
    1.14    next
    1.15      from G_upper[of x] show "eventually (\<lambda>n. Gamma_series x n * (1 + x / real n) \<ge> G x) sequentially"
    1.16 -      using eventually_ge_at_top[of "2::nat"] x by (auto elim!: eventually_mono)
    1.17 +      using x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "2::nat"]])
    1.18    qed simp_all
    1.19  qed
    1.20  
    1.21 @@ -2472,9 +2472,9 @@
    1.22    let ?r' = "\<lambda>n. exp (z * of_real (ln (of_nat (Suc n) / of_nat n)))"
    1.23    from z have z': "z \<noteq> 0" by auto
    1.24  
    1.25 -  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" using eventually_gt_at_top[of "0::nat"]
    1.26 +  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" 
    1.27      using z by (auto simp: divide_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac
    1.28 -                     elim!: eventually_mono dest: pochhammer_eq_0_imp_nonpos_Int)
    1.29 +                     intro: eventually_mono eventually_gt_at_top[of "0::nat"] dest: pochhammer_eq_0_imp_nonpos_Int)
    1.30    moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))"
    1.31      by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all
    1.32    ultimately show "?r \<longlonglongrightarrow> 1" by (force dest!: Lim_transform_eventually)