Theorem gamcvg2

Description: An infinite product expression for the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Hypotheses	gamcvg2.f	$$⊢F=\left(m\in \mathbb{N}⟼\frac{{\left(\frac{m+1}{m}\right)}^A}{\left(\frac{A}{m}\right)+1}\right)$$
	gamcvg2.a	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
Assertion	gamcvg2	$$⊢\phi \to seq1\left(\times ,F\right)⇝\mathrm{\Gamma }\left(A\right)A$$

Proof

Step	Hyp	Ref	Expression
1		gamcvg2.f	$$⊢F=\left(m\in \mathbb{N}⟼\frac{{\left(\frac{m+1}{m}\right)}^A}{\left(\frac{A}{m}\right)+1}\right)$$
2		gamcvg2.a	$$⊢\phi \to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
3		eqid	$$⊢\left(m\in \mathbb{N}⟼A\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{A}{m}\right)+1\right)\right)=\left(m\in \mathbb{N}⟼A\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{A}{m}\right)+1\right)\right)$$
4	1 2 3	gamcvg2lem	$$⊢\phi \to \exp \circ seq1\left(+,\left(m\in \mathbb{N}⟼A\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{A}{m}\right)+1\right)\right)\right)=seq1\left(\times ,F\right)$$
5	3 2	gamcvg	$$⊢\phi \to \left(\exp \circ seq1\left(+,\left(m\in \mathbb{N}⟼A\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{A}{m}\right)+1\right)\right)\right)\right)⇝\mathrm{\Gamma }\left(A\right)A$$
6	4 5	eqbrtrrd	$$⊢\phi \to seq1\left(\times ,F\right)⇝\mathrm{\Gamma }\left(A\right)A$$