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	⊢ ( 𝐴 ∈ ℝ+ → ( Γ ‘ 𝐴 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		rpdmgm	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
2		eflgam	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( exp ‘ ( log Γ ‘ 𝐴 ) ) = ( Γ ‘ 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( log Γ ‘ 𝐴 ) ) = ( Γ ‘ 𝐴 ) )
4		relgamcl	⊢ ( 𝐴 ∈ ℝ+ → ( log Γ ‘ 𝐴 ) ∈ ℝ )
5	4	rpefcld	⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( log Γ ‘ 𝐴 ) ) ∈ ℝ+ )
6	3 5	eqeltrrd	⊢ ( 𝐴 ∈ ℝ+ → ( Γ ‘ 𝐴 ) ∈ ℝ+ )