Metamath Proof Explorer

Theorem lgamgulmlem6

Description: The series G is uniformly convergent on the compact region U , which describes a circle of radius R with holes of size 1 / R around the poles of the gamma function. (Contributed by Mario Carneiro, 9-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 ) ) ) ) )
lgamgulm.t 
|- T = ( m e. NN |-> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) )
Assertion lgamgulmlem6 
|- ( ph -> ( seq 1 ( oF + , G ) e. dom ( ~~>u ` U ) /\ ( seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) -> E. r e. RR A. z e. U ( abs ` O ) <_ r ) ) )

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 lgamgulm.t 
 |-  T = ( m e. NN |-> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 1zzd 
 |-  ( ph -> 1 e. ZZ )
7 cnex 
 |-  CC e. _V
8 2 7 rabex2 
 |-  U e. _V
9 8 a1i 
 |-  ( ph -> U e. _V )
10 1 2 lgamgulmlem1 
 |-  ( ph -> U C_ ( CC \ ( ZZ \ NN ) ) )
11 10 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> U C_ ( CC \ ( ZZ \ NN ) ) )
12 simpr 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> z e. U )
13 11 12 sseldd 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> z e. ( CC \ ( ZZ \ NN ) ) )
14 13 eldifad 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> z e. CC )
15 simplr 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> m e. NN )
16 15 peano2nnd 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( m + 1 ) e. NN )
17 16 nnrpd 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( m + 1 ) e. RR+ )
18 15 nnrpd 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> m e. RR+ )
19 17 18 rpdivcld 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( ( m + 1 ) / m ) e. RR+ )
20 19 relogcld 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( log ` ( ( m + 1 ) / m ) ) e. RR )
21 20 recnd 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( log ` ( ( m + 1 ) / m ) ) e. CC )
22 14 21 mulcld 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( z x. ( log ` ( ( m + 1 ) / m ) ) ) e. CC )
23 15 nncnd 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> m e. CC )
24 15 nnne0d 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> m =/= 0 )
25 14 23 24 divcld 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( z / m ) e. CC )
26 1cnd 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> 1 e. CC )
27 25 26 addcld 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( ( z / m ) + 1 ) e. CC )
28 13 15 dmgmdivn0 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( ( z / m ) + 1 ) =/= 0 )
29 27 28 logcld 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( log ` ( ( z / m ) + 1 ) ) e. CC )
30 22 29 subcld 
 |-  ( ( ( ph /\ m e. NN ) /\ z e. U ) -> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) e. CC )
31 30 fmpttd 
 |-  ( ( ph /\ m e. NN ) -> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) : U --> CC )
32 7 8 elmap 
 |-  ( ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) e. ( CC ^m U ) <-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) : U --> CC )
33 31 32 sylibr 
 |-  ( ( ph /\ m e. NN ) -> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) e. ( CC ^m U ) )
34 33 3 fmptd 
 |-  ( ph -> G : NN --> ( CC ^m U ) )
35 nnex 
 |-  NN e. _V
36 35 mptex 
 |-  ( m e. NN |-> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) ) e. _V
37 4 36 eqeltri 
 |-  T e. _V
38 37 a1i 
 |-  ( ph -> T e. _V )
39 1 adantr 
 |-  ( ( ph /\ m e. NN ) -> R e. NN )
40 39 nnred 
 |-  ( ( ph /\ m e. NN ) -> R e. RR )
41 2re 
 |-  2 e. RR
42 41 a1i 
 |-  ( ( ph /\ m e. NN ) -> 2 e. RR )
43 1red 
 |-  ( ( ph /\ m e. NN ) -> 1 e. RR )
44 40 43 readdcld 
 |-  ( ( ph /\ m e. NN ) -> ( R + 1 ) e. RR )
45 42 44 remulcld 
 |-  ( ( ph /\ m e. NN ) -> ( 2 x. ( R + 1 ) ) e. RR )
46 simpr 
 |-  ( ( ph /\ m e. NN ) -> m e. NN )
47 46 nnsqcld 
 |-  ( ( ph /\ m e. NN ) -> ( m ^ 2 ) e. NN )
48 45 47 nndivred 
 |-  ( ( ph /\ m e. NN ) -> ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) e. RR )
49 40 48 remulcld 
 |-  ( ( ph /\ m e. NN ) -> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) e. RR )
50 46 peano2nnd 
 |-  ( ( ph /\ m e. NN ) -> ( m + 1 ) e. NN )
51 50 nnrpd 
 |-  ( ( ph /\ m e. NN ) -> ( m + 1 ) e. RR+ )
52 46 nnrpd 
 |-  ( ( ph /\ m e. NN ) -> m e. RR+ )
53 51 52 rpdivcld 
 |-  ( ( ph /\ m e. NN ) -> ( ( m + 1 ) / m ) e. RR+ )
54 53 relogcld 
 |-  ( ( ph /\ m e. NN ) -> ( log ` ( ( m + 1 ) / m ) ) e. RR )
55 40 54 remulcld 
 |-  ( ( ph /\ m e. NN ) -> ( R x. ( log ` ( ( m + 1 ) / m ) ) ) e. RR )
56 39 peano2nnd 
 |-  ( ( ph /\ m e. NN ) -> ( R + 1 ) e. NN )
57 56 nnrpd 
 |-  ( ( ph /\ m e. NN ) -> ( R + 1 ) e. RR+ )
58 57 52 rpmulcld 
 |-  ( ( ph /\ m e. NN ) -> ( ( R + 1 ) x. m ) e. RR+ )
59 58 relogcld 
 |-  ( ( ph /\ m e. NN ) -> ( log ` ( ( R + 1 ) x. m ) ) e. RR )
60 pire 
 |-  _pi e. RR
61 60 a1i 
 |-  ( ( ph /\ m e. NN ) -> _pi e. RR )
62 59 61 readdcld 
 |-  ( ( ph /\ m e. NN ) -> ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) e. RR )
63 55 62 readdcld 
 |-  ( ( ph /\ m e. NN ) -> ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) e. RR )
64 49 63 ifcld 
 |-  ( ( ph /\ m e. NN ) -> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) e. RR )
65 64 4 fmptd 
 |-  ( ph -> T : NN --> RR )
66 65 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( T ` n ) e. RR )
67 1 2 3 4 lgamgulmlem5 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( G ` n ) ` y ) ) <_ ( T ` n ) )
68 1 2 3 4 lgamgulmlem4 
 |-  ( ph -> seq 1 ( + , T ) e. dom ~~> )
69 5 6 9 34 38 66 67 68 mtest 
 |-  ( ph -> seq 1 ( oF + , G ) e. dom ( ~~>u ` U ) )
70 1zzd 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> 1 e. ZZ )
71 8 a1i 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> U e. _V )
72 34 adantr 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> G : NN --> ( CC ^m U ) )
73 37 a1i 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> T e. _V )
74 66 adantlr 
 |-  ( ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) /\ n e. NN ) -> ( T ` n ) e. RR )
75 67 adantlr 
 |-  ( ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( G ` n ) ` y ) ) <_ ( T ` n ) )
76 68 adantr 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> seq 1 ( + , T ) e. dom ~~> )
77 simpr 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) )
78 5 70 71 72 73 74 75 76 77 mtestbdd 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> E. r e. RR A. y e. U ( abs ` ( ( z e. U |-> O ) ` y ) ) <_ r )
79 nfcv 
 |-  F/_ z abs
80 nffvmpt1 
 |-  F/_ z ( ( z e. U |-> O ) ` y )
81 79 80 nffv 
 |-  F/_ z ( abs ` ( ( z e. U |-> O ) ` y ) )
82 nfcv 
 |-  F/_ z <_
83 nfcv 
 |-  F/_ z r
84 81 82 83 nfbr 
 |-  F/ z ( abs ` ( ( z e. U |-> O ) ` y ) ) <_ r
85 nfv 
 |-  F/ y ( abs ` ( ( z e. U |-> O ) ` z ) ) <_ r
86 2fveq3 
 |-  ( y = z -> ( abs ` ( ( z e. U |-> O ) ` y ) ) = ( abs ` ( ( z e. U |-> O ) ` z ) ) )
87 86 breq1d 
 |-  ( y = z -> ( ( abs ` ( ( z e. U |-> O ) ` y ) ) <_ r <-> ( abs ` ( ( z e. U |-> O ) ` z ) ) <_ r ) )
88 84 85 87 cbvralw 
 |-  ( A. y e. U ( abs ` ( ( z e. U |-> O ) ` y ) ) <_ r <-> A. z e. U ( abs ` ( ( z e. U |-> O ) ` z ) ) <_ r )
89 ulmcl 
 |-  ( seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) -> ( z e. U |-> O ) : U --> CC )
90 89 adantl 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> ( z e. U |-> O ) : U --> CC )
91 eqid 
 |-  ( z e. U |-> O ) = ( z e. U |-> O )
92 91 fmpt 
 |-  ( A. z e. U O e. CC <-> ( z e. U |-> O ) : U --> CC )
93 90 92 sylibr 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> A. z e. U O e. CC )
94 91 fvmpt2 
 |-  ( ( z e. U /\ O e. CC ) -> ( ( z e. U |-> O ) ` z ) = O )
95 94 fveq2d 
 |-  ( ( z e. U /\ O e. CC ) -> ( abs ` ( ( z e. U |-> O ) ` z ) ) = ( abs ` O ) )
96 95 breq1d 
 |-  ( ( z e. U /\ O e. CC ) -> ( ( abs ` ( ( z e. U |-> O ) ` z ) ) <_ r <-> ( abs ` O ) <_ r ) )
97 96 ralimiaa 
 |-  ( A. z e. U O e. CC -> A. z e. U ( ( abs ` ( ( z e. U |-> O ) ` z ) ) <_ r <-> ( abs ` O ) <_ r ) )
98 ralbi 
 |-  ( A. z e. U ( ( abs ` ( ( z e. U |-> O ) ` z ) ) <_ r <-> ( abs ` O ) <_ r ) -> ( A. z e. U ( abs ` ( ( z e. U |-> O ) ` z ) ) <_ r <-> A. z e. U ( abs ` O ) <_ r ) )
99 93 97 98 3syl 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> ( A. z e. U ( abs ` ( ( z e. U |-> O ) ` z ) ) <_ r <-> A. z e. U ( abs ` O ) <_ r ) )
100 88 99 syl5bb 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> ( A. y e. U ( abs ` ( ( z e. U |-> O ) ` y ) ) <_ r <-> A. z e. U ( abs ` O ) <_ r ) )
101 100 rexbidv 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> ( E. r e. RR A. y e. U ( abs ` ( ( z e. U |-> O ) ` y ) ) <_ r <-> E. r e. RR A. z e. U ( abs ` O ) <_ r ) )
102 78 101 mpbid 
 |-  ( ( ph /\ seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) ) -> E. r e. RR A. z e. U ( abs ` O ) <_ r )
103 102 ex 
 |-  ( ph -> ( seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) -> E. r e. RR A. z e. U ( abs ` O ) <_ r ) )
104 69 103 jca 
 |-  ( ph -> ( seq 1 ( oF + , G ) e. dom ( ~~>u ` U ) /\ ( seq 1 ( oF + , G ) ( ~~>u ` U ) ( z e. U |-> O ) -> E. r e. RR A. z e. U ( abs ` O ) <_ r ) ) )