Metamath Proof Explorer

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 e. RR+ -> ( _G ` A ) e. RR+ )

Proof

Step Hyp Ref Expression
1 rpdmgm 
 |-  ( A e. RR+ -> A e. ( CC \ ( ZZ \ NN ) ) )
2 eflgam 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` A ) ) = ( _G ` A ) )
3 1 2 syl 
 |-  ( A e. RR+ -> ( exp ` ( log_G ` A ) ) = ( _G ` A ) )
4 relgamcl 
 |-  ( A e. RR+ -> ( log_G ` A ) e. RR )
5 4 rpefcld 
 |-  ( A e. RR+ -> ( exp ` ( log_G ` A ) ) e. RR+ )
6 3 5 eqeltrrd 
 |-  ( A e. RR+ -> ( _G ` A ) e. RR+ )