Theorem relgamcl

Description: The log-Gamma function is real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Assertion	relgamcl	$$⊢A\in {ℝ}^{+}\to \log \mathrm{\Gamma }\left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		rpdmgm	$$⊢A\in {ℝ}^{+}\to A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)$$
2		lgamcl	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to \log \mathrm{\Gamma }\left(A\right)\in ℂ$$
3	1 2	syl	$$⊢A\in {ℝ}^{+}\to \log \mathrm{\Gamma }\left(A\right)\in ℂ$$
4		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
5	4	recnd	$$⊢A\in {ℝ}^{+}\to \log A\in ℂ$$
6	3 5	pncand	$$⊢A\in {ℝ}^{+}\to \log \mathrm{\Gamma }\left(A\right)+\log A-\log A=\log \mathrm{\Gamma }\left(A\right)$$
7		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
8		1zzd	$$⊢A\in {ℝ}^{+}\to 1\in \mathbb{Z}$$
9		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)$$
10	9 1	lgamcvg	$$⊢A\in {ℝ}^{+}\to 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)⇝\left(\log \mathrm{\Gamma }\left(A\right)+\log A\right)$$
11		simpl	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to A\in {ℝ}^{+}$$
12	11	rpred	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to A\in ℝ$$
13		simpr	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to m\in \mathbb{N}$$
14	13	peano2nnd	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to m+1\in \mathbb{N}$$
15	14	nnrpd	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to m+1\in {ℝ}^{+}$$
16	13	nnrpd	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to m\in {ℝ}^{+}$$
17	15 16	rpdivcld	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to \frac{m+1}{m}\in {ℝ}^{+}$$
18	17	relogcld	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to \log \left(\frac{m+1}{m}\right)\in ℝ$$
19	12 18	remulcld	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to A\log \left(\frac{m+1}{m}\right)\in ℝ$$
20	11 16	rpdivcld	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to \frac{A}{m}\in {ℝ}^{+}$$
21		1rp	$$⊢1\in {ℝ}^{+}$$
22	21	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to 1\in {ℝ}^{+}$$
23	20 22	rpaddcld	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to \left(\frac{A}{m}\right)+1\in {ℝ}^{+}$$
24	23	relogcld	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to \log \left(\left(\frac{A}{m}\right)+1\right)\in ℝ$$
25	19 24	resubcld	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \mathbb{N}\right)\to A\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{A}{m}\right)+1\right)\in ℝ$$
26	25	fmpttd	$$⊢A\in {ℝ}^{+}\to \left(m\in \mathbb{N}⟼A\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{A}{m}\right)+1\right)\right):\mathbb{N}⟶ℝ$$
27	26	ffvelrnda	$$⊢\left(A\in {ℝ}^{+}\wedge n\in \mathbb{N}\right)\to \left(m\in \mathbb{N}⟼A\log \left(\frac{m+1}{m}\right)-\log \left(\left(\frac{A}{m}\right)+1\right)\right)\left(n\right)\in ℝ$$
28	7 8 27	serfre	$$⊢A\in {ℝ}^{+}\to 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):\mathbb{N}⟶ℝ$$
29	28	ffvelrnda	$$⊢\left(A\in {ℝ}^{+}\wedge n\in \mathbb{N}\right)\to 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)\left(n\right)\in ℝ$$
30	7 8 10 29	climrecl	$$⊢A\in {ℝ}^{+}\to \log \mathrm{\Gamma }\left(A\right)+\log A\in ℝ$$
31	30 4	resubcld	$$⊢A\in {ℝ}^{+}\to \log \mathrm{\Gamma }\left(A\right)+\log A-\log A\in ℝ$$
32	6 31	eqeltrrd	$$⊢A\in {ℝ}^{+}\to \log \mathrm{\Gamma }\left(A\right)\in ℝ$$