Metamath Proof Explorer

Theorem gamp1

Description: The functional equation of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017)

Ref Expression
Assertion gamp1 
|- ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` ( A + 1 ) ) = ( ( _G ` A ) x. A ) )

Proof

Step Hyp Ref Expression
1 lgamp1 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` ( A + 1 ) ) = ( ( log_G ` A ) + ( log ` A ) ) )
2 1 fveq2d 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` ( A + 1 ) ) ) = ( exp ` ( ( log_G ` A ) + ( log ` A ) ) ) )
3 lgamcl 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` A ) e. CC )
4 eldifi 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> A e. CC )
5 id 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> A e. ( CC \ ( ZZ \ NN ) ) )
6 5 dmgmn0 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> A =/= 0 )
7 4 6 logcld 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log ` A ) e. CC )
8 efadd 
 |-  ( ( ( log_G ` A ) e. CC /\ ( log ` A ) e. CC ) -> ( exp ` ( ( log_G ` A ) + ( log ` A ) ) ) = ( ( exp ` ( log_G ` A ) ) x. ( exp ` ( log ` A ) ) ) )
9 3 7 8 syl2anc 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( ( log_G ` A ) + ( log ` A ) ) ) = ( ( exp ` ( log_G ` A ) ) x. ( exp ` ( log ` A ) ) ) )
10 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
11 4 6 10 syl2anc 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log ` A ) ) = A )
12 11 oveq2d 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( ( exp ` ( log_G ` A ) ) x. ( exp ` ( log ` A ) ) ) = ( ( exp ` ( log_G ` A ) ) x. A ) )
13 2 9 12 3eqtrd 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` ( A + 1 ) ) ) = ( ( exp ` ( log_G ` A ) ) x. A ) )
14 1nn0 
 |-  1 e. NN0
15 14 a1i 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> 1 e. NN0 )
16 5 15 dmgmaddnn0 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( A + 1 ) e. ( CC \ ( ZZ \ NN ) ) )
17 eflgam 
 |-  ( ( A + 1 ) e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` ( A + 1 ) ) ) = ( _G ` ( A + 1 ) ) )
18 16 17 syl 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` ( A + 1 ) ) ) = ( _G ` ( A + 1 ) ) )
19 eflgam 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` A ) ) = ( _G ` A ) )
20 19 oveq1d 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( ( exp ` ( log_G ` A ) ) x. A ) = ( ( _G ` A ) x. A ) )
21 13 18 20 3eqtr3d 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( _G ` ( A + 1 ) ) = ( ( _G ` A ) x. A ) )