[STATEMENT]
lemma Gamma_residue:
  "residue Gamma (-of_nat n) = (-1) ^ n / fact n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. residue Gamma (- of_nat n) = (- 1) ^ n / fact n
[PROOF STEP]
proof (rule residue_simple')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. open ?s
 2. - of_nat n \<in> ?s
 3. Gamma holomorphic_on ?s - {- of_nat n}
 4. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- 1) ^ n / fact n
[PROOF STEP]
show "open (- (\<int>\<^sub>\<le>\<^sub>0 - {-of_nat n}) :: complex set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (- (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}))
[PROOF STEP]
by (intro open_Compl closed_subset_Ints) auto
[PROOF STATE]
proof (state)
this:
open (- (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}))

goal (3 subgoals):
 1. - of_nat n \<in> - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n})
 2. Gamma holomorphic_on - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}) - {- of_nat n}
 3. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- 1) ^ n / fact n
[PROOF STEP]
show "Gamma holomorphic_on (- (\<int>\<^sub>\<le>\<^sub>0 - {-of_nat n}) - {- of_nat n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gamma holomorphic_on - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}) - {- of_nat n}
[PROOF STEP]
by (rule holomorphic_Gamma) auto
[PROOF STATE]
proof (state)
this:
Gamma holomorphic_on - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n}) - {- of_nat n}

goal (2 subgoals):
 1. - of_nat n \<in> - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n})
 2. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- 1) ^ n / fact n
[PROOF STEP]
show "(\<lambda>w. Gamma w * (w - (-of_nat n))) \<midarrow>(-of_nat n)\<rightarrow> (- 1) ^ n / fact n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- (1::'a)) ^ n / fact n
[PROOF STEP]
using Gamma_residues[of n]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>z. Gamma z * (z + of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- (1::?'a)) ^ n / fact n

goal (1 subgoal):
 1. (\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- (1::'a)) ^ n / fact n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n\<rightarrow> (- (1::?'a1)) ^ n / fact n

goal (1 subgoal):
 1. - of_nat n \<in> - (\<int>\<^sub>\<le>\<^sub>0 - {- of_nat n})
[PROOF STEP]
qed auto