Metamath Proof Explorer

Theorem gamigam

Description: The Gamma function is the inverse of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017)

Ref Expression
Assertion gamigam 
|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` A ) = ( 1 / ( 1/_G ` A ) ) )

Proof

Step Hyp Ref Expression
1 igamgam 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( 1/_G ` A ) = ( 1 / ( _G ` A ) ) )
2 1 oveq2d 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( 1 / ( 1/_G ` A ) ) = ( 1 / ( 1 / ( _G ` A ) ) ) )
3 gamcl 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` A ) e. CC )
4 gamne0 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` A ) =/= 0 )
5 3 4 recrecd 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( 1 / ( 1 / ( _G ` A ) ) ) = ( _G ` A ) )
6 2 5 eqtr2d 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` A ) = ( 1 / ( 1/_G ` A ) ) )