Metamath Proof Explorer

Theorem iprodgam

Description: An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018)

Ref Expression
Hypothesis iprodgam.1 
|- ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
Assertion iprodgam 
|- ( ph -> ( _G ` A ) = ( prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) / A ) )

Proof

Step Hyp Ref Expression
1 iprodgam.1 
 |-  ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
2 eflgam 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( exp ` ( log_G ` A ) ) = ( _G ` A ) )
3 1 2 syl 
 |-  ( ph -> ( exp ` ( log_G ` A ) ) = ( _G ` A ) )
4 oveq1 
 |-  ( z = A -> ( z x. ( log ` ( ( k + 1 ) / k ) ) ) = ( A x. ( log ` ( ( k + 1 ) / k ) ) ) )
5 oveq1 
 |-  ( z = A -> ( z / k ) = ( A / k ) )
6 5 fvoveq1d 
 |-  ( z = A -> ( log ` ( ( z / k ) + 1 ) ) = ( log ` ( ( A / k ) + 1 ) ) )
7 4 6 oveq12d 
 |-  ( z = A -> ( ( z x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( z / k ) + 1 ) ) ) = ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) )
8 7 sumeq2sdv 
 |-  ( z = A -> sum_ k e. NN ( ( z x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( z / k ) + 1 ) ) ) = sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) )
9 fveq2 
 |-  ( z = A -> ( log ` z ) = ( log ` A ) )
10 8 9 oveq12d 
 |-  ( z = A -> ( sum_ k e. NN ( ( z x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( z / k ) + 1 ) ) ) - ( log ` z ) ) = ( sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) - ( log ` A ) ) )
11 df-lgam 
 |-  log_G = ( z e. ( CC \ ( ZZ \ NN ) ) |-> ( sum_ k e. NN ( ( z x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( z / k ) + 1 ) ) ) - ( log ` z ) ) )
12 ovex 
 |-  ( sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) - ( log ` A ) ) e. _V
13 10 11 12 fvmpt 
 |-  ( A e. ( CC \ ( ZZ \ NN ) ) -> ( log_G ` A ) = ( sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) - ( log ` A ) ) )
14 1 13 syl 
 |-  ( ph -> ( log_G ` A ) = ( sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) - ( log ` A ) ) )
15 14 fveq2d 
 |-  ( ph -> ( exp ` ( log_G ` A ) ) = ( exp ` ( sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) - ( log ` A ) ) ) )
16 nnuz 
 |-  NN = ( ZZ>= ` 1 )
17 1zzd 
 |-  ( ph -> 1 e. ZZ )
18 oveq1 
 |-  ( j = k -> ( j + 1 ) = ( k + 1 ) )
19 id 
 |-  ( j = k -> j = k )
20 18 19 oveq12d 
 |-  ( j = k -> ( ( j + 1 ) / j ) = ( ( k + 1 ) / k ) )
21 20 fveq2d 
 |-  ( j = k -> ( log ` ( ( j + 1 ) / j ) ) = ( log ` ( ( k + 1 ) / k ) ) )
22 21 oveq2d 
 |-  ( j = k -> ( A x. ( log ` ( ( j + 1 ) / j ) ) ) = ( A x. ( log ` ( ( k + 1 ) / k ) ) ) )
23 oveq2 
 |-  ( j = k -> ( A / j ) = ( A / k ) )
24 23 fvoveq1d 
 |-  ( j = k -> ( log ` ( ( A / j ) + 1 ) ) = ( log ` ( ( A / k ) + 1 ) ) )
25 22 24 oveq12d 
 |-  ( j = k -> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) = ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) )
26 eqid 
 |-  ( j e. NN |-> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) ) = ( j e. NN |-> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) )
27 ovex 
 |-  ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) e. _V
28 25 26 27 fvmpt 
 |-  ( k e. NN -> ( ( j e. NN |-> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) ) ` k ) = ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) )
29 28 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( j e. NN |-> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) ) ` k ) = ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) )
30 1 eldifad 
 |-  ( ph -> A e. CC )
31 30 adantr 
 |-  ( ( ph /\ k e. NN ) -> A e. CC )
32 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
33 32 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
34 33 nncnd 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. CC )
35 nncn 
 |-  ( k e. NN -> k e. CC )
36 35 adantl 
 |-  ( ( ph /\ k e. NN ) -> k e. CC )
37 nnne0 
 |-  ( k e. NN -> k =/= 0 )
38 37 adantl 
 |-  ( ( ph /\ k e. NN ) -> k =/= 0 )
39 34 36 38 divcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( k + 1 ) / k ) e. CC )
40 33 nnne0d 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) =/= 0 )
41 34 36 40 38 divne0d 
 |-  ( ( ph /\ k e. NN ) -> ( ( k + 1 ) / k ) =/= 0 )
42 39 41 logcld 
 |-  ( ( ph /\ k e. NN ) -> ( log ` ( ( k + 1 ) / k ) ) e. CC )
43 31 42 mulcld 
 |-  ( ( ph /\ k e. NN ) -> ( A x. ( log ` ( ( k + 1 ) / k ) ) ) e. CC )
44 31 36 38 divcld 
 |-  ( ( ph /\ k e. NN ) -> ( A / k ) e. CC )
45 1cnd 
 |-  ( ( ph /\ k e. NN ) -> 1 e. CC )
46 44 45 addcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( A / k ) + 1 ) e. CC )
47 1 adantr 
 |-  ( ( ph /\ k e. NN ) -> A e. ( CC \ ( ZZ \ NN ) ) )
48 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
49 47 48 dmgmdivn0 
 |-  ( ( ph /\ k e. NN ) -> ( ( A / k ) + 1 ) =/= 0 )
50 46 49 logcld 
 |-  ( ( ph /\ k e. NN ) -> ( log ` ( ( A / k ) + 1 ) ) e. CC )
51 43 50 subcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) e. CC )
52 26 1 lgamcvg 
 |-  ( ph -> seq 1 ( + , ( j e. NN |-> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) ) ) ~~> ( ( log_G ` A ) + ( log ` A ) ) )
53 seqex 
 |-  seq 1 ( + , ( j e. NN |-> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) ) ) e. _V
54 ovex 
 |-  ( ( log_G ` A ) + ( log ` A ) ) e. _V
55 53 54 breldm 
 |-  ( seq 1 ( + , ( j e. NN |-> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) ) ) ~~> ( ( log_G ` A ) + ( log ` A ) ) -> seq 1 ( + , ( j e. NN |-> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) ) ) e. dom ~~> )
56 52 55 syl 
 |-  ( ph -> seq 1 ( + , ( j e. NN |-> ( ( A x. ( log ` ( ( j + 1 ) / j ) ) ) - ( log ` ( ( A / j ) + 1 ) ) ) ) ) e. dom ~~> )
57 16 17 29 51 56 isumcl 
 |-  ( ph -> sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) e. CC )
58 1 dmgmn0 
 |-  ( ph -> A =/= 0 )
59 30 58 logcld 
 |-  ( ph -> ( log ` A ) e. CC )
60 efsub 
 |-  ( ( sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) e. CC /\ ( log ` A ) e. CC ) -> ( exp ` ( sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) - ( log ` A ) ) ) = ( ( exp ` sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) / ( exp ` ( log ` A ) ) ) )
61 57 59 60 syl2anc 
 |-  ( ph -> ( exp ` ( sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) - ( log ` A ) ) ) = ( ( exp ` sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) / ( exp ` ( log ` A ) ) ) )
62 16 17 29 51 56 iprodefisum 
 |-  ( ph -> prod_ k e. NN ( exp ` ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) = ( exp ` sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) )
63 efsub 
 |-  ( ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) e. CC /\ ( log ` ( ( A / k ) + 1 ) ) e. CC ) -> ( exp ` ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) = ( ( exp ` ( A x. ( log ` ( ( k + 1 ) / k ) ) ) ) / ( exp ` ( log ` ( ( A / k ) + 1 ) ) ) ) )
64 43 50 63 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) = ( ( exp ` ( A x. ( log ` ( ( k + 1 ) / k ) ) ) ) / ( exp ` ( log ` ( ( A / k ) + 1 ) ) ) ) )
65 36 45 36 38 divdird 
 |-  ( ( ph /\ k e. NN ) -> ( ( k + 1 ) / k ) = ( ( k / k ) + ( 1 / k ) ) )
66 36 38 dividd 
 |-  ( ( ph /\ k e. NN ) -> ( k / k ) = 1 )
67 66 oveq1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( k / k ) + ( 1 / k ) ) = ( 1 + ( 1 / k ) ) )
68 65 67 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( k + 1 ) / k ) = ( 1 + ( 1 / k ) ) )
69 68 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( log ` ( ( k + 1 ) / k ) ) = ( log ` ( 1 + ( 1 / k ) ) ) )
70 69 oveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( A x. ( log ` ( ( k + 1 ) / k ) ) ) = ( A x. ( log ` ( 1 + ( 1 / k ) ) ) ) )
71 70 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( A x. ( log ` ( ( k + 1 ) / k ) ) ) ) = ( exp ` ( A x. ( log ` ( 1 + ( 1 / k ) ) ) ) ) )
72 1rp 
 |-  1 e. RR+
73 72 a1i 
 |-  ( ( ph /\ k e. NN ) -> 1 e. RR+ )
74 48 nnrpd 
 |-  ( ( ph /\ k e. NN ) -> k e. RR+ )
75 74 rpreccld 
 |-  ( ( ph /\ k e. NN ) -> ( 1 / k ) e. RR+ )
76 73 75 rpaddcld 
 |-  ( ( ph /\ k e. NN ) -> ( 1 + ( 1 / k ) ) e. RR+ )
77 76 rpcnd 
 |-  ( ( ph /\ k e. NN ) -> ( 1 + ( 1 / k ) ) e. CC )
78 76 rpne0d 
 |-  ( ( ph /\ k e. NN ) -> ( 1 + ( 1 / k ) ) =/= 0 )
79 77 78 31 cxpefd 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1 + ( 1 / k ) ) ^c A ) = ( exp ` ( A x. ( log ` ( 1 + ( 1 / k ) ) ) ) ) )
80 71 79 eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( A x. ( log ` ( ( k + 1 ) / k ) ) ) ) = ( ( 1 + ( 1 / k ) ) ^c A ) )
81 eflog 
 |-  ( ( ( ( A / k ) + 1 ) e. CC /\ ( ( A / k ) + 1 ) =/= 0 ) -> ( exp ` ( log ` ( ( A / k ) + 1 ) ) ) = ( ( A / k ) + 1 ) )
82 46 49 81 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( log ` ( ( A / k ) + 1 ) ) ) = ( ( A / k ) + 1 ) )
83 44 45 addcomd 
 |-  ( ( ph /\ k e. NN ) -> ( ( A / k ) + 1 ) = ( 1 + ( A / k ) ) )
84 82 83 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( log ` ( ( A / k ) + 1 ) ) ) = ( 1 + ( A / k ) ) )
85 80 84 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( exp ` ( A x. ( log ` ( ( k + 1 ) / k ) ) ) ) / ( exp ` ( log ` ( ( A / k ) + 1 ) ) ) ) = ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) )
86 64 85 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( exp ` ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) = ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) )
87 86 prodeq2dv 
 |-  ( ph -> prod_ k e. NN ( exp ` ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) = prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) )
88 62 87 eqtr3d 
 |-  ( ph -> ( exp ` sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) = prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) )
89 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
90 30 58 89 syl2anc 
 |-  ( ph -> ( exp ` ( log ` A ) ) = A )
91 88 90 oveq12d 
 |-  ( ph -> ( ( exp ` sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) ) / ( exp ` ( log ` A ) ) ) = ( prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) / A ) )
92 61 91 eqtrd 
 |-  ( ph -> ( exp ` ( sum_ k e. NN ( ( A x. ( log ` ( ( k + 1 ) / k ) ) ) - ( log ` ( ( A / k ) + 1 ) ) ) - ( log ` A ) ) ) = ( prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) / A ) )
93 15 92 eqtrd 
 |-  ( ph -> ( exp ` ( log_G ` A ) ) = ( prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) / A ) )
94 3 93 eqtr3d 
 |-  ( ph -> ( _G ` A ) = ( prod_ k e. NN ( ( ( 1 + ( 1 / k ) ) ^c A ) / ( 1 + ( A / k ) ) ) / A ) )