Metamath Proof Explorer

Theorem lgamgulm2

Description: Rewrite the limit of the sequence G in terms of the log-Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r 
|- ( ph -> R e. NN )
lgamgulm.u 
|- U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
lgamgulm.g 
|- G = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
Assertion lgamgulm2 
|- ( ph -> ( A. z e. U ( log_G ` z ) e. CC /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lgamgulm.r 
 |-  ( ph -> R e. NN )
2 lgamgulm.u 
 |-  U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
3 lgamgulm.g 
 |-  G = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
4 1 2 lgamgulmlem1 
 |-  ( ph -> U C_ ( CC \ ( ZZ \ NN ) ) )
5 4 sselda 
 |-  ( ( ph /\ z e. U ) -> z e. ( CC \ ( ZZ \ NN ) ) )
6 ovex 
 |-  ( sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) - ( log ` z ) ) e. _V
7 df-lgam 
 |-  log_G = ( z e. ( CC \ ( ZZ \ NN ) ) |-> ( sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) - ( log ` z ) ) )
8 7 fvmpt2 
 |-  ( ( z e. ( CC \ ( ZZ \ NN ) ) /\ ( sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) - ( log ` z ) ) e. _V ) -> ( log_G ` z ) = ( sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) - ( log ` z ) ) )
9 5 6 8 sylancl 
 |-  ( ( ph /\ z e. U ) -> ( log_G ` z ) = ( sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) - ( log ` z ) ) )
10 nnuz 
 |-  NN = ( ZZ>= ` 1 )
11 1zzd 
 |-  ( ( ph /\ z e. U ) -> 1 e. ZZ )
12 oveq1 
 |-  ( m = n -> ( m + 1 ) = ( n + 1 ) )
13 id 
 |-  ( m = n -> m = n )
14 12 13 oveq12d 
 |-  ( m = n -> ( ( m + 1 ) / m ) = ( ( n + 1 ) / n ) )
15 14 fveq2d 
 |-  ( m = n -> ( log ` ( ( m + 1 ) / m ) ) = ( log ` ( ( n + 1 ) / n ) ) )
16 15 oveq2d 
 |-  ( m = n -> ( z x. ( log ` ( ( m + 1 ) / m ) ) ) = ( z x. ( log ` ( ( n + 1 ) / n ) ) ) )
17 oveq2 
 |-  ( m = n -> ( z / m ) = ( z / n ) )
18 17 fvoveq1d 
 |-  ( m = n -> ( log ` ( ( z / m ) + 1 ) ) = ( log ` ( ( z / n ) + 1 ) ) )
19 16 18 oveq12d 
 |-  ( m = n -> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) = ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) )
20 eqid 
 |-  ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) = ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) )
21 ovex 
 |-  ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) e. _V
22 19 20 21 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ` n ) = ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) )
23 22 adantl 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ` n ) = ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) )
24 5 eldifad 
 |-  ( ( ph /\ z e. U ) -> z e. CC )
25 24 adantr 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> z e. CC )
26 simpr 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> n e. NN )
27 26 peano2nnd 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( n + 1 ) e. NN )
28 27 nnrpd 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( n + 1 ) e. RR+ )
29 26 nnrpd 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> n e. RR+ )
30 28 29 rpdivcld 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( ( n + 1 ) / n ) e. RR+ )
31 30 relogcld 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( log ` ( ( n + 1 ) / n ) ) e. RR )
32 31 recnd 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( log ` ( ( n + 1 ) / n ) ) e. CC )
33 25 32 mulcld 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( z x. ( log ` ( ( n + 1 ) / n ) ) ) e. CC )
34 26 nncnd 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> n e. CC )
35 26 nnne0d 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> n =/= 0 )
36 25 34 35 divcld 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( z / n ) e. CC )
37 1cnd 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> 1 e. CC )
38 36 37 addcld 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( ( z / n ) + 1 ) e. CC )
39 5 adantr 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> z e. ( CC \ ( ZZ \ NN ) ) )
40 39 26 dmgmdivn0 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( ( z / n ) + 1 ) =/= 0 )
41 38 40 logcld 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( log ` ( ( z / n ) + 1 ) ) e. CC )
42 33 41 subcld 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) e. CC )
43 1z 
 |-  1 e. ZZ
44 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( oF + , G ) Fn ( ZZ>= ` 1 ) )
45 43 44 ax-mp 
 |-  seq 1 ( oF + , G ) Fn ( ZZ>= ` 1 )
46 10 fneq2i 
 |-  ( seq 1 ( oF + , G ) Fn NN <-> seq 1 ( oF + , G ) Fn ( ZZ>= ` 1 ) )
47 45 46 mpbir 
 |-  seq 1 ( oF + , G ) Fn NN
48 1 2 3 lgamgulm 
 |-  ( ph -> seq 1 ( oF + , G ) e. dom ( ~~>u ` U ) )
49 ulmdm 
 |-  ( seq 1 ( oF + , G ) e. dom ( ~~>u ` U ) <-> seq 1 ( oF + , G ) ( ~~>u ` U ) ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) )
50 48 49 sylib 
 |-  ( ph -> seq 1 ( oF + , G ) ( ~~>u ` U ) ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) )
51 ulmf2 
 |-  ( ( seq 1 ( oF + , G ) Fn NN /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) ) -> seq 1 ( oF + , G ) : NN --> ( CC ^m U ) )
52 47 50 51 sylancr 
 |-  ( ph -> seq 1 ( oF + , G ) : NN --> ( CC ^m U ) )
53 52 adantr 
 |-  ( ( ph /\ z e. U ) -> seq 1 ( oF + , G ) : NN --> ( CC ^m U ) )
54 simpr 
 |-  ( ( ph /\ z e. U ) -> z e. U )
55 seqex 
 |-  seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) e. _V
56 55 a1i 
 |-  ( ( ph /\ z e. U ) -> seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) e. _V )
57 3 a1i 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> G = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) )
58 57 seqeq3d 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> seq 1 ( oF + , G ) = seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) )
59 58 fveq1d 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( seq 1 ( oF + , G ) ` n ) = ( seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) ` n ) )
60 cnex 
 |-  CC e. _V
61 2 60 rabex2 
 |-  U e. _V
62 61 a1i 
 |-  ( ( ph /\ n e. NN ) -> U e. _V )
63 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
64 63 10 eleqtrdi 
 |-  ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
65 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
66 65 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) C_ NN )
67 ovexd 
 |-  ( ( ( ph /\ n e. NN ) /\ ( m e. NN /\ z e. U ) ) -> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) e. _V )
68 62 64 66 67 seqof2 
 |-  ( ( ph /\ n e. NN ) -> ( seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) ` n ) = ( z e. U |-> ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) ) )
69 68 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) ` n ) = ( z e. U |-> ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) ) )
70 59 69 eqtrd 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( seq 1 ( oF + , G ) ` n ) = ( z e. U |-> ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) ) )
71 70 fveq1d 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( ( seq 1 ( oF + , G ) ` n ) ` z ) = ( ( z e. U |-> ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) ) ` z ) )
72 54 adantr 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> z e. U )
73 fvex 
 |-  ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) e. _V
74 eqid 
 |-  ( z e. U |-> ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) ) = ( z e. U |-> ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) )
75 74 fvmpt2 
 |-  ( ( z e. U /\ ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) e. _V ) -> ( ( z e. U |-> ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) ) ` z ) = ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) )
76 72 73 75 sylancl 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( ( z e. U |-> ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) ) ` z ) = ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) )
77 71 76 eqtrd 
 |-  ( ( ( ph /\ z e. U ) /\ n e. NN ) -> ( ( seq 1 ( oF + , G ) ` n ) ` z ) = ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) )
78 50 adantr 
 |-  ( ( ph /\ z e. U ) -> seq 1 ( oF + , G ) ( ~~>u ` U ) ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) )
79 10 11 53 54 56 77 78 ulmclm 
 |-  ( ( ph /\ z e. U ) -> seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ~~> ( ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) ` z ) )
80 10 11 23 42 79 isumclim 
 |-  ( ( ph /\ z e. U ) -> sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) = ( ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) ` z ) )
81 ulmcl 
 |-  ( seq 1 ( oF + , G ) ( ~~>u ` U ) ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) -> ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) : U --> CC )
82 50 81 syl 
 |-  ( ph -> ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) : U --> CC )
83 82 ffvelrnda 
 |-  ( ( ph /\ z e. U ) -> ( ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) ` z ) e. CC )
84 80 83 eqeltrd 
 |-  ( ( ph /\ z e. U ) -> sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) e. CC )
85 5 dmgmn0 
 |-  ( ( ph /\ z e. U ) -> z =/= 0 )
86 24 85 logcld 
 |-  ( ( ph /\ z e. U ) -> ( log ` z ) e. CC )
87 84 86 subcld 
 |-  ( ( ph /\ z e. U ) -> ( sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) - ( log ` z ) ) e. CC )
88 9 87 eqeltrd 
 |-  ( ( ph /\ z e. U ) -> ( log_G ` z ) e. CC )
89 88 ralrimiva 
 |-  ( ph -> A. z e. U ( log_G ` z ) e. CC )
90 ffn 
 |-  ( ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) : U --> CC -> ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) Fn U )
91 50 81 90 3syl 
 |-  ( ph -> ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) Fn U )
92 nfcv 
 |-  F/_ z ( ~~>u ` U )
93 nfcv 
 |-  F/_ z 1
94 nfcv 
 |-  F/_ z oF +
95 nfcv 
 |-  F/_ z NN
96 nfmpt1 
 |-  F/_ z ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) )
97 95 96 nfmpt 
 |-  F/_ z ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
98 3 97 nfcxfr 
 |-  F/_ z G
99 93 94 98 nfseq 
 |-  F/_ z seq 1 ( oF + , G )
100 92 99 nffv 
 |-  F/_ z ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) )
101 100 dffn5f 
 |-  ( ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) Fn U <-> ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) = ( z e. U |-> ( ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) ` z ) ) )
102 91 101 sylib 
 |-  ( ph -> ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) = ( z e. U |-> ( ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) ` z ) ) )
103 9 oveq1d 
 |-  ( ( ph /\ z e. U ) -> ( ( log_G ` z ) + ( log ` z ) ) = ( ( sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) - ( log ` z ) ) + ( log ` z ) ) )
104 84 86 npcand 
 |-  ( ( ph /\ z e. U ) -> ( ( sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) - ( log ` z ) ) + ( log ` z ) ) = sum_ n e. NN ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) )
105 103 104 80 3eqtrrd 
 |-  ( ( ph /\ z e. U ) -> ( ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) ` z ) = ( ( log_G ` z ) + ( log ` z ) ) )
106 105 mpteq2dva 
 |-  ( ph -> ( z e. U |-> ( ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) ` z ) ) = ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) )
107 102 106 eqtrd 
 |-  ( ph -> ( ( ~~>u ` U ) ` seq 1 ( oF + , G ) ) = ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) )
108 50 107 breqtrd 
 |-  ( ph -> seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) )
109 89 108 jca 
 |-  ( ph -> ( A. z e. U ( log_G ` z ) e. CC /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) ) )