[STATEMENT]
lemma rGamma_series_LIMSEQ [tendsto_intros]:
  "rGamma_series z \<longlonglongrightarrow> rGamma z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
 2. z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<notin> \<int>\<^sub>\<le>\<^sub>0

goal (2 subgoals):
 1. z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
 2. z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
hence "z \<noteq> - of_nat n" for n
[PROOF STATE]
proof (prove)
using this:
z \<notin> \<int>\<^sub>\<le>\<^sub>0

goal (1 subgoal):
 1. z \<noteq> - of_nat n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<noteq> - of_nat ?n

goal (2 subgoals):
 1. z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
 2. z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
from rGamma_series_aux[OF this]
[PROOF STATE]
proof (chain)
picking this:
let fact' = \<lambda>n. prod of_nat {1..n}; exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e; pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n in (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real n) *\<^sub>R (1::'a)))) \<longlonglongrightarrow> rGamma z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
let fact' = \<lambda>n. prod of_nat {1..n}; exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e; pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n in (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real n) *\<^sub>R (1::'a)))) \<longlonglongrightarrow> rGamma z

goal (1 subgoal):
 1. rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
by (simp add: rGamma_series_def[abs_def] fact_prod pochhammer_Suc_prod
                  exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
[PROOF STATE]
proof (state)
this:
rGamma_series z \<longlonglongrightarrow> rGamma z

goal (1 subgoal):
 1. z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> rGamma z
[PROOF STEP]
qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)