Metamath Proof Explorer

Theorem lgamgulm

Description: The series G is uniformly convergent on the compact region U , which describes a circle of radius R with holes of size 1 / R around the poles of the gamma function. (Contributed by Mario Carneiro, 3-Jul-2017)

		Ref	Expression
	Hypotheses	lgamgulm.r	$⊢ φ \to R \in ℕ$
		lgamgulm.u	$⊢ U = \{x \in ℂ \| (\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|)\}$
		lgamgulm.g	$⊢ G = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
	Assertion	lgamgulm	$⊢ φ \to seq 1 (\circ_{f} +, G) \in dom \underset{u}{⇝} (U)$

Proof

Step	Hyp	Ref	Expression
1		lgamgulm.r	$⊢ φ \to R \in ℕ$
2		lgamgulm.u	$⊢ U = \{x \in ℂ \| (\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|)\}$
3		lgamgulm.g	$⊢ G = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
4		eqid	$⊢ (m \in ℕ ⟼ if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π)) = (m \in ℕ ⟼ if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π))$
5	1 2 3 4	lgamgulmlem6	$⊢ φ \to (seq 1 (\circ_{f} +, G) \in dom \underset{u}{⇝} (U) \land (seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ 1) \to \exists r \in ℝ \forall z \in U \|1\| \leq r))$
6	5	simpld	$⊢ φ \to seq 1 (\circ_{f} +, G) \in dom \underset{u}{⇝} (U)$