Theorem lgamcvg

Description: The series G converges to log_G ( A ) + log ( A ) . (Contributed by Mario Carneiro, 6-Jul-2017)

	Ref	Expression
Hypotheses	lgamcvg.g	$$⊢G=\left(m\in \mathbb{N}⟼A\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{A}{m}\right)+1\right)\right)$$
	lgamcvg.a	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
Assertion	lgamcvg	$$⊢\phi \to seq1\left(+,G\right)⇝\left(\log \mathrm{\Gamma }\left(A\right)+\log A\right)$$

Proof

Step	Hyp	Ref	Expression
1		lgamcvg.g	$$⊢G=\left(m\in \mathbb{N}⟼A\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{A}{m}\right)+1\right)\right)$$
2		lgamcvg.a	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
3		eqid	$$⊢\left\{x\in ℂ|\left(\left|x\right|\le y\wedge \forall k\in {\mathbb{N}}_0\frac{1}{y}\le \left|x+k\right|\right)\right\}=\left\{x\in ℂ|\left(\left|x\right|\le y\wedge \forall k\in {\mathbb{N}}_0\frac{1}{y}\le \left|x+k\right|\right)\right\}$$
4	3 2 1	lgamcvglem	$$⊢\phi \to \left(\log \mathrm{\Gamma }\left(A\right)\in ℂ\wedge seq1\left(+,G\right)⇝\left(\log \mathrm{\Gamma }\left(A\right)+\log A\right)\right)$$
5	4	simprd	$$⊢\phi \to seq1\left(+,G\right)⇝\left(\log \mathrm{\Gamma }\left(A\right)+\log A\right)$$