Metamath Proof Explorer

Theorem gamcl

Description: The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017)

Ref Expression
Assertion gamcl 
|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` A ) e. CC )

Proof

Step Hyp Ref Expression
1 gamf 
 |-  _G : ( CC \ ( ZZ \ NN ) ) --> CC
2 1 ffvelrni 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` A ) e. CC )