Metamath Proof Explorer

Theorem lgamcvglem

Description: Lemma for lgamf and lgamcvg . (Contributed by Mario Carneiro, 8-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 lgamucov.u 
 |-  U = { x e. CC | ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) }
2 lgamucov.a 
 |-  ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
3 lgamcvglem.g 
 |-  G = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) )
4 1 2 lgamucov2 
 |-  ( ph -> E. r e. NN A e. U )
5 fveq2 
 |-  ( z = A -> ( log_G ` z ) = ( log_G ` A ) )
6 5 eleq1d 
 |-  ( z = A -> ( ( log_G ` z ) e. CC <-> ( log_G ` A ) e. CC ) )
7 simprl 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> r e. NN )
8 fveq2 
 |-  ( x = t -> ( abs ` x ) = ( abs ` t ) )
9 8 breq1d 
 |-  ( x = t -> ( ( abs ` x ) <_ r <-> ( abs ` t ) <_ r ) )
10 fvoveq1 
 |-  ( x = t -> ( abs ` ( x + k ) ) = ( abs ` ( t + k ) ) )
11 10 breq2d 
 |-  ( x = t -> ( ( 1 / r ) <_ ( abs ` ( x + k ) ) <-> ( 1 / r ) <_ ( abs ` ( t + k ) ) ) )
12 11 ralbidv 
 |-  ( x = t -> ( A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) <-> A. k e. NN0 ( 1 / r ) <_ ( abs ` ( t + k ) ) ) )
13 9 12 anbi12d 
 |-  ( x = t -> ( ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) <-> ( ( abs ` t ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( t + k ) ) ) ) )
14 13 cbvrabv 
 |-  { x e. CC | ( ( abs ` x ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( x + k ) ) ) } = { t e. CC | ( ( abs ` t ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( t + k ) ) ) }
15 1 14 eqtri 
 |-  U = { t e. CC | ( ( abs ` t ) <_ r /\ A. k e. NN0 ( 1 / r ) <_ ( abs ` ( t + k ) ) ) }
16 eqid 
 |-  ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
17 7 15 16 lgamgulm2 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> ( A. z e. U ( log_G ` z ) e. CC /\ seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) ) )
18 17 simpld 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> A. z e. U ( log_G ` z ) e. CC )
19 simprr 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> A e. U )
20 6 18 19 rspcdva 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> ( log_G ` A ) e. CC )
21 nnuz 
 |-  NN = ( ZZ>= ` 1 )
22 1zzd 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> 1 e. ZZ )
23 1z 
 |-  1 e. ZZ
24 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) Fn ( ZZ>= ` 1 ) )
25 23 24 ax-mp 
 |-  seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) Fn ( ZZ>= ` 1 )
26 21 fneq2i 
 |-  ( seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) Fn NN <-> seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) Fn ( ZZ>= ` 1 ) )
27 25 26 mpbir 
 |-  seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) Fn NN
28 17 simprd 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) )
29 ulmf2 
 |-  ( ( seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) Fn NN /\ seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) ( ~~>u ` U ) ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) ) -> seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) : NN --> ( CC ^m U ) )
30 27 28 29 sylancr 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> seq 1 ( oF + , ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ) : NN --> ( CC ^m U ) )
31 seqex 
 |-  seq 1 ( + , G ) e. _V
32 31 a1i 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> seq 1 ( + , G ) e. _V )
33 cnex 
 |-  CC e. _V
34 1 33 rabex2 
 |-  U e. _V
35 34 a1i 
 |-  ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) -> U e. _V )
36 simpr 
 |-  ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) -> n e. NN )
37 36 21 eleqtrdi 
 |-  ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
38 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
39 38 a1i 
 |-  ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) -> ( 1 ... n ) C_ NN )
40 ovexd 
 |-  ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ ( m e. NN /\ z e. U ) ) -> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) e. _V )
41 35 37 39 40 seqof2 
 |-  ( ( ( ph /\ ( r e. NN /\ A 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 ) ) )
42 simplr 
 |-  ( ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ z = A ) /\ m e. NN ) -> z = A )
43 42 oveq1d 
 |-  ( ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ z = A ) /\ m e. NN ) -> ( z x. ( log ` ( ( m + 1 ) / m ) ) ) = ( A x. ( log ` ( ( m + 1 ) / m ) ) ) )
44 42 oveq1d 
 |-  ( ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ z = A ) /\ m e. NN ) -> ( z / m ) = ( A / m ) )
45 44 fvoveq1d 
 |-  ( ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ z = A ) /\ m e. NN ) -> ( log ` ( ( z / m ) + 1 ) ) = ( log ` ( ( A / m ) + 1 ) ) )
46 43 45 oveq12d 
 |-  ( ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ z = A ) /\ m e. NN ) -> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) = ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) )
47 46 mpteq2dva 
 |-  ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ z = A ) -> ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) = ( m e. NN |-> ( ( A x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( A / m ) + 1 ) ) ) ) )
48 47 3 eqtr4di 
 |-  ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ z = A ) -> ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) = G )
49 48 seqeq3d 
 |-  ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ z = A ) -> seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) = seq 1 ( + , G ) )
50 49 fveq1d 
 |-  ( ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) /\ z = A ) -> ( seq 1 ( + , ( m e. NN |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) ) ` n ) = ( seq 1 ( + , G ) ` n ) )
51 simplrr 
 |-  ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) -> A e. U )
52 fvexd 
 |-  ( ( ( ph /\ ( r e. NN /\ A e. U ) ) /\ n e. NN ) -> ( seq 1 ( + , G ) ` n ) e. _V )
53 41 50 51 52 fvmptd 
 |-  ( ( ( ph /\ ( r e. NN /\ A 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 ) ` A ) = ( seq 1 ( + , G ) ` n ) )
54 21 22 30 19 32 53 28 ulmclm 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> seq 1 ( + , G ) ~~> ( ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) ` A ) )
55 fveq2 
 |-  ( z = A -> ( log ` z ) = ( log ` A ) )
56 5 55 oveq12d 
 |-  ( z = A -> ( ( log_G ` z ) + ( log ` z ) ) = ( ( log_G ` A ) + ( log ` A ) ) )
57 eqid 
 |-  ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) = ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) )
58 ovex 
 |-  ( ( log_G ` A ) + ( log ` A ) ) e. _V
59 56 57 58 fvmpt 
 |-  ( A e. U -> ( ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) ` A ) = ( ( log_G ` A ) + ( log ` A ) ) )
60 19 59 syl 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> ( ( z e. U |-> ( ( log_G ` z ) + ( log ` z ) ) ) ` A ) = ( ( log_G ` A ) + ( log ` A ) ) )
61 54 60 breqtrd 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> seq 1 ( + , G ) ~~> ( ( log_G ` A ) + ( log ` A ) ) )
62 20 61 jca 
 |-  ( ( ph /\ ( r e. NN /\ A e. U ) ) -> ( ( log_G ` A ) e. CC /\ seq 1 ( + , G ) ~~> ( ( log_G ` A ) + ( log ` A ) ) ) )
63 4 62 rexlimddv 
 |-  ( ph -> ( ( log_G ` A ) e. CC /\ seq 1 ( + , G ) ~~> ( ( log_G ` A ) + ( log ` A ) ) ) )