Theorem rpgamcl

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

	Ref	Expression
Assertion	rpgamcl	$$⊢A\in {ℝ}^{+}\to \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		eflgam	$$⊢A\in \left(ℂ\setminus \left(\mathbb{Z}\setminus \mathbb{N}\right)\right)\to {\mathrm{e}}^{\log \mathrm{\Gamma }\left(A\right)}=\mathrm{\Gamma }\left(A\right)$$
3	1 2	syl	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log \mathrm{\Gamma }\left(A\right)}=\mathrm{\Gamma }\left(A\right)$$
4		relgamcl	$$⊢A\in {ℝ}^{+}\to \log \mathrm{\Gamma }\left(A\right)\in ℝ$$
5	4	rpefcld	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log \mathrm{\Gamma }\left(A\right)}\in {ℝ}^{+}$$
6	3 5	eqeltrrd	$$⊢A\in {ℝ}^{+}\to \mathrm{\Gamma }\left(A\right)\in {ℝ}^{+}$$