Metamath Proof Explorer

Theorem gam1

Description: The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017)

Ref Expression
Assertion gam1 
|- ( _G ` 1 ) = 1

Proof

Step Hyp Ref Expression
1 lgam1 
 |-  ( log_G ` 1 ) = 0
2 1 fveq2i 
 |-  ( exp ` ( log_G ` 1 ) ) = ( exp ` 0 )
3 ax-1cn 
 |-  1 e. CC
4 1nn 
 |-  1 e. NN
5 eldifn 
 |-  ( 1 e. ( ZZ \ NN ) -> -. 1 e. NN )
6 4 5 mt2 
 |-  -. 1 e. ( ZZ \ NN )
7 eldif 
 |-  ( 1 e. ( CC \ ( ZZ \ NN ) ) <-> ( 1 e. CC /\ -. 1 e. ( ZZ \ NN ) ) )
8 3 6 7 mpbir2an 
 |-  1 e. ( CC \ ( ZZ \ NN ) )
9 eflgam 
 |-  ( 1 e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` 1 ) ) = ( _G ` 1 ) )
10 8 9 ax-mp 
 |-  ( exp ` ( log_G ` 1 ) ) = ( _G ` 1 )
11 ef0 
 |-  ( exp ` 0 ) = 1
12 2 10 11 3eqtr3i 
 |-  ( _G ` 1 ) = 1