Metamath Proof Explorer

Theorem lgamgulmlem4

Description: Lemma for lgamgulm . (Contributed by Mario Carneiro, 3-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 lgamgulmlem4 
|- ( ph -> seq 1 ( + , T ) e. dom ~~> )

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 2nn 
 |-  2 e. NN
6 5 a1i 
 |-  ( ph -> 2 e. NN )
7 6 1 nnmulcld 
 |-  ( ph -> ( 2 x. R ) e. NN )
8 7 nnzd 
 |-  ( ph -> ( 2 x. R ) e. ZZ )
9 eluzle 
 |-  ( n e. ( ZZ>= ` ( 2 x. R ) ) -> ( 2 x. R ) <_ n )
10 9 adantl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( 2 x. R ) ) ) -> ( 2 x. R ) <_ n )
11 10 iftrued 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( 2 x. R ) ) ) -> if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) = ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) )
12 eluznn 
 |-  ( ( ( 2 x. R ) e. NN /\ n e. ( ZZ>= ` ( 2 x. R ) ) ) -> n e. NN )
13 7 12 sylan 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( 2 x. R ) ) ) -> n e. NN )
14 breq2 
 |-  ( m = n -> ( ( 2 x. R ) <_ m <-> ( 2 x. R ) <_ n ) )
15 oveq1 
 |-  ( m = n -> ( m ^ 2 ) = ( n ^ 2 ) )
16 15 oveq2d 
 |-  ( m = n -> ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) = ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) )
17 16 oveq2d 
 |-  ( m = n -> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) = ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) )
18 oveq1 
 |-  ( m = n -> ( m + 1 ) = ( n + 1 ) )
19 id 
 |-  ( m = n -> m = n )
20 18 19 oveq12d 
 |-  ( m = n -> ( ( m + 1 ) / m ) = ( ( n + 1 ) / n ) )
21 20 fveq2d 
 |-  ( m = n -> ( log ` ( ( m + 1 ) / m ) ) = ( log ` ( ( n + 1 ) / n ) ) )
22 21 oveq2d 
 |-  ( m = n -> ( R x. ( log ` ( ( m + 1 ) / m ) ) ) = ( R x. ( log ` ( ( n + 1 ) / n ) ) ) )
23 oveq2 
 |-  ( m = n -> ( ( R + 1 ) x. m ) = ( ( R + 1 ) x. n ) )
24 23 fveq2d 
 |-  ( m = n -> ( log ` ( ( R + 1 ) x. m ) ) = ( log ` ( ( R + 1 ) x. n ) ) )
25 24 oveq1d 
 |-  ( m = n -> ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) = ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) )
26 22 25 oveq12d 
 |-  ( m = n -> ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) = ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) )
27 14 17 26 ifbieq12d 
 |-  ( m = n -> 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 ) ) ) = if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) )
28 ovex 
 |-  ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) e. _V
29 ovex 
 |-  ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) e. _V
30 28 29 ifex 
 |-  if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) e. _V
31 27 4 30 fvmpt 
 |-  ( n e. NN -> ( T ` n ) = if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) )
32 13 31 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( 2 x. R ) ) ) -> ( T ` n ) = if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) )
33 eqid 
 |-  ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) = ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) )
34 17 33 28 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ` n ) = ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) )
35 13 34 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( 2 x. R ) ) ) -> ( ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ` n ) = ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) )
36 11 32 35 3eqtr4d 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( 2 x. R ) ) ) -> ( T ` n ) = ( ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ` n ) )
37 8 36 seqfeq 
 |-  ( ph -> seq ( 2 x. R ) ( + , T ) = seq ( 2 x. R ) ( + , ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ) )
38 nnuz 
 |-  NN = ( ZZ>= ` 1 )
39 1zzd 
 |-  ( ph -> 1 e. ZZ )
40 1 nncnd 
 |-  ( ph -> R e. CC )
41 2cnd 
 |-  ( ph -> 2 e. CC )
42 1cnd 
 |-  ( ph -> 1 e. CC )
43 40 42 addcld 
 |-  ( ph -> ( R + 1 ) e. CC )
44 41 43 mulcld 
 |-  ( ph -> ( 2 x. ( R + 1 ) ) e. CC )
45 40 44 mulcld 
 |-  ( ph -> ( R x. ( 2 x. ( R + 1 ) ) ) e. CC )
46 1lt2 
 |-  1 < 2
47 2re 
 |-  2 e. RR
48 rere 
 |-  ( 2 e. RR -> ( Re ` 2 ) = 2 )
49 47 48 ax-mp 
 |-  ( Re ` 2 ) = 2
50 46 49 breqtrri 
 |-  1 < ( Re ` 2 )
51 50 a1i 
 |-  ( ph -> 1 < ( Re ` 2 ) )
52 oveq1 
 |-  ( m = n -> ( m ^c -u 2 ) = ( n ^c -u 2 ) )
53 eqid 
 |-  ( m e. NN |-> ( m ^c -u 2 ) ) = ( m e. NN |-> ( m ^c -u 2 ) )
54 ovex 
 |-  ( n ^c -u 2 ) e. _V
55 52 53 54 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( m ^c -u 2 ) ) ` n ) = ( n ^c -u 2 ) )
56 55 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( m ^c -u 2 ) ) ` n ) = ( n ^c -u 2 ) )
57 41 51 56 zetacvg 
 |-  ( ph -> seq 1 ( + , ( m e. NN |-> ( m ^c -u 2 ) ) ) e. dom ~~> )
58 climdm 
 |-  ( seq 1 ( + , ( m e. NN |-> ( m ^c -u 2 ) ) ) e. dom ~~> <-> seq 1 ( + , ( m e. NN |-> ( m ^c -u 2 ) ) ) ~~> ( ~~> ` seq 1 ( + , ( m e. NN |-> ( m ^c -u 2 ) ) ) ) )
59 57 58 sylib 
 |-  ( ph -> seq 1 ( + , ( m e. NN |-> ( m ^c -u 2 ) ) ) ~~> ( ~~> ` seq 1 ( + , ( m e. NN |-> ( m ^c -u 2 ) ) ) ) )
60 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
61 60 nncnd 
 |-  ( ( ph /\ n e. NN ) -> n e. CC )
62 2cnd 
 |-  ( ( ph /\ n e. NN ) -> 2 e. CC )
63 62 negcld 
 |-  ( ( ph /\ n e. NN ) -> -u 2 e. CC )
64 61 63 cxpcld 
 |-  ( ( ph /\ n e. NN ) -> ( n ^c -u 2 ) e. CC )
65 56 64 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( m ^c -u 2 ) ) ` n ) e. CC )
66 40 adantr 
 |-  ( ( ph /\ n e. NN ) -> R e. CC )
67 1cnd 
 |-  ( ( ph /\ n e. NN ) -> 1 e. CC )
68 66 67 addcld 
 |-  ( ( ph /\ n e. NN ) -> ( R + 1 ) e. CC )
69 62 68 mulcld 
 |-  ( ( ph /\ n e. NN ) -> ( 2 x. ( R + 1 ) ) e. CC )
70 66 69 mulcld 
 |-  ( ( ph /\ n e. NN ) -> ( R x. ( 2 x. ( R + 1 ) ) ) e. CC )
71 61 sqcld 
 |-  ( ( ph /\ n e. NN ) -> ( n ^ 2 ) e. CC )
72 60 nnne0d 
 |-  ( ( ph /\ n e. NN ) -> n =/= 0 )
73 2z 
 |-  2 e. ZZ
74 73 a1i 
 |-  ( ( ph /\ n e. NN ) -> 2 e. ZZ )
75 61 72 74 expne0d 
 |-  ( ( ph /\ n e. NN ) -> ( n ^ 2 ) =/= 0 )
76 70 71 75 divrecd 
 |-  ( ( ph /\ n e. NN ) -> ( ( R x. ( 2 x. ( R + 1 ) ) ) / ( n ^ 2 ) ) = ( ( R x. ( 2 x. ( R + 1 ) ) ) x. ( 1 / ( n ^ 2 ) ) ) )
77 66 69 71 75 divassd 
 |-  ( ( ph /\ n e. NN ) -> ( ( R x. ( 2 x. ( R + 1 ) ) ) / ( n ^ 2 ) ) = ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) )
78 61 72 62 cxpnegd 
 |-  ( ( ph /\ n e. NN ) -> ( n ^c -u 2 ) = ( 1 / ( n ^c 2 ) ) )
79 61 72 74 cxpexpzd 
 |-  ( ( ph /\ n e. NN ) -> ( n ^c 2 ) = ( n ^ 2 ) )
80 79 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / ( n ^c 2 ) ) = ( 1 / ( n ^ 2 ) ) )
81 78 80 eqtr2d 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / ( n ^ 2 ) ) = ( n ^c -u 2 ) )
82 81 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( R x. ( 2 x. ( R + 1 ) ) ) x. ( 1 / ( n ^ 2 ) ) ) = ( ( R x. ( 2 x. ( R + 1 ) ) ) x. ( n ^c -u 2 ) ) )
83 76 77 82 3eqtr3d 
 |-  ( ( ph /\ n e. NN ) -> ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) = ( ( R x. ( 2 x. ( R + 1 ) ) ) x. ( n ^c -u 2 ) ) )
84 34 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ` n ) = ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) )
85 56 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( R x. ( 2 x. ( R + 1 ) ) ) x. ( ( m e. NN |-> ( m ^c -u 2 ) ) ` n ) ) = ( ( R x. ( 2 x. ( R + 1 ) ) ) x. ( n ^c -u 2 ) ) )
86 83 84 85 3eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ` n ) = ( ( R x. ( 2 x. ( R + 1 ) ) ) x. ( ( m e. NN |-> ( m ^c -u 2 ) ) ` n ) ) )
87 38 39 45 59 65 86 isermulc2 
 |-  ( ph -> seq 1 ( + , ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ) ~~> ( ( R x. ( 2 x. ( R + 1 ) ) ) x. ( ~~> ` seq 1 ( + , ( m e. NN |-> ( m ^c -u 2 ) ) ) ) ) )
88 climrel 
 |-  Rel ~~>
89 88 releldmi 
 |-  ( seq 1 ( + , ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ) ~~> ( ( R x. ( 2 x. ( R + 1 ) ) ) x. ( ~~> ` seq 1 ( + , ( m e. NN |-> ( m ^c -u 2 ) ) ) ) ) -> seq 1 ( + , ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ) e. dom ~~> )
90 87 89 syl 
 |-  ( ph -> seq 1 ( + , ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ) e. dom ~~> )
91 69 71 75 divcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) e. CC )
92 66 91 mulcld 
 |-  ( ( ph /\ n e. NN ) -> ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) e. CC )
93 84 92 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ` n ) e. CC )
94 38 7 93 iserex 
 |-  ( ph -> ( seq 1 ( + , ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ) e. dom ~~> <-> seq ( 2 x. R ) ( + , ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ) e. dom ~~> ) )
95 90 94 mpbid 
 |-  ( ph -> seq ( 2 x. R ) ( + , ( m e. NN |-> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) ) ) e. dom ~~> )
96 37 95 eqeltrd 
 |-  ( ph -> seq ( 2 x. R ) ( + , T ) e. dom ~~> )
97 31 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( T ` n ) = if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) )
98 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> R e. NN )
99 98 nnred 
 |-  ( ( ph /\ n e. NN ) -> R e. RR )
100 47 a1i 
 |-  ( ( ph /\ n e. NN ) -> 2 e. RR )
101 1red 
 |-  ( ( ph /\ n e. NN ) -> 1 e. RR )
102 99 101 readdcld 
 |-  ( ( ph /\ n e. NN ) -> ( R + 1 ) e. RR )
103 100 102 remulcld 
 |-  ( ( ph /\ n e. NN ) -> ( 2 x. ( R + 1 ) ) e. RR )
104 60 nnsqcld 
 |-  ( ( ph /\ n e. NN ) -> ( n ^ 2 ) e. NN )
105 103 104 nndivred 
 |-  ( ( ph /\ n e. NN ) -> ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) e. RR )
106 99 105 remulcld 
 |-  ( ( ph /\ n e. NN ) -> ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) e. RR )
107 60 peano2nnd 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. NN )
108 107 nnrpd 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. RR+ )
109 60 nnrpd 
 |-  ( ( ph /\ n e. NN ) -> n e. RR+ )
110 108 109 rpdivcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( n + 1 ) / n ) e. RR+ )
111 110 relogcld 
 |-  ( ( ph /\ n e. NN ) -> ( log ` ( ( n + 1 ) / n ) ) e. RR )
112 99 111 remulcld 
 |-  ( ( ph /\ n e. NN ) -> ( R x. ( log ` ( ( n + 1 ) / n ) ) ) e. RR )
113 98 peano2nnd 
 |-  ( ( ph /\ n e. NN ) -> ( R + 1 ) e. NN )
114 113 nnrpd 
 |-  ( ( ph /\ n e. NN ) -> ( R + 1 ) e. RR+ )
115 114 109 rpmulcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( R + 1 ) x. n ) e. RR+ )
116 115 relogcld 
 |-  ( ( ph /\ n e. NN ) -> ( log ` ( ( R + 1 ) x. n ) ) e. RR )
117 pire 
 |-  _pi e. RR
118 117 a1i 
 |-  ( ( ph /\ n e. NN ) -> _pi e. RR )
119 116 118 readdcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) e. RR )
120 112 119 readdcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) e. RR )
121 106 120 ifcld 
 |-  ( ( ph /\ n e. NN ) -> if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) e. RR )
122 97 121 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( T ` n ) e. RR )
123 122 recnd 
 |-  ( ( ph /\ n e. NN ) -> ( T ` n ) e. CC )
124 38 7 123 iserex 
 |-  ( ph -> ( seq 1 ( + , T ) e. dom ~~> <-> seq ( 2 x. R ) ( + , T ) e. dom ~~> ) )
125 96 124 mpbird 
 |-  ( ph -> seq 1 ( + , T ) e. dom ~~> )