Metamath Proof Explorer


Theorem dchrvmasumlem2

Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses rpvmasum.z Z=/N
rpvmasum.l L=ℤRHomZ
rpvmasum.a φN
rpvmasum.g G=DChrN
rpvmasum.d D=BaseG
rpvmasum.1 1˙=0G
dchrisum.b φXD
dchrisum.n1 φX1˙
dchrvmasum.f φm+F
dchrvmasum.g m=xdF=K
dchrvmasum.c φC0+∞
dchrvmasum.t φT
dchrvmasum.1 φm3+∞FTClogmm
dchrvmasum.r φR
dchrvmasum.2 φm13FTR
Assertion dchrvmasumlem2 φx+d=1xKTd𝑂1

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z=/N
2 rpvmasum.l L=ℤRHomZ
3 rpvmasum.a φN
4 rpvmasum.g G=DChrN
5 rpvmasum.d D=BaseG
6 rpvmasum.1 1˙=0G
7 dchrisum.b φXD
8 dchrisum.n1 φX1˙
9 dchrvmasum.f φm+F
10 dchrvmasum.g m=xdF=K
11 dchrvmasum.c φC0+∞
12 dchrvmasum.t φT
13 dchrvmasum.1 φm3+∞FTClogmm
14 dchrvmasum.r φR
15 dchrvmasum.2 φm13FTR
16 1red φ1
17 elrege0 C0+∞C0C
18 11 17 sylib φC0C
19 18 simpld φC
20 19 adantr φx+C
21 fzfid φx+1xFin
22 simpr φx+x+
23 elfznn d1xd
24 23 nnrpd d1xd+
25 rpdivcl x+d+xd+
26 22 24 25 syl2an φx+d1xxd+
27 26 relogcld φx+d1xlogxd
28 22 adantr φx+d1xx+
29 27 28 rerpdivcld φx+d1xlogxdx
30 21 29 fsumrecl φx+d=1xlogxdx
31 20 30 remulcld φx+Cd=1xlogxdx
32 3nn 3
33 nnrp 33+
34 relogcl 3+log3
35 32 33 34 mp2b log3
36 1re 1
37 35 36 readdcli log3+1
38 remulcl Rlog3+1Rlog3+1
39 14 37 38 sylancl φRlog3+1
40 39 adantr φx+Rlog3+1
41 rpssre +
42 19 recnd φC
43 o1const +Cx+C𝑂1
44 41 42 43 sylancr φx+C𝑂1
45 logfacrlim2 x+d=1xlogxdx1
46 rlimo1 x+d=1xlogxdx1x+d=1xlogxdx𝑂1
47 45 46 mp1i φx+d=1xlogxdx𝑂1
48 20 30 44 47 o1mul2 φx+Cd=1xlogxdx𝑂1
49 39 recnd φRlog3+1
50 o1const +Rlog3+1x+Rlog3+1𝑂1
51 41 49 50 sylancr φx+Rlog3+1𝑂1
52 31 40 48 51 o1add2 φx+Cd=1xlogxdx+Rlog3+1𝑂1
53 31 40 readdcld φx+Cd=1xlogxdx+Rlog3+1
54 10 eleq1d m=xdFK
55 9 ralrimiva φm+F
56 55 ad2antrr φx+d1xm+F
57 54 56 26 rspcdva φx+d1xK
58 12 ad2antrr φx+d1xT
59 57 58 subcld φx+d1xKT
60 59 abscld φx+d1xKT
61 23 adantl φx+d1xd
62 60 61 nndivred φx+d1xKTd
63 21 62 fsumrecl φx+d=1xKTd
64 63 recnd φx+d=1xKTd
65 61 nnrpd φx+d1xd+
66 59 absge0d φx+d1x0KT
67 60 65 66 divge0d φx+d1x0KTd
68 21 62 67 fsumge0 φx+0d=1xKTd
69 63 68 absidd φx+d=1xKTd=d=1xKTd
70 69 63 eqeltrd φx+d=1xKTd
71 53 recnd φx+Cd=1xlogxdx+Rlog3+1
72 71 abscld φx+Cd=1xlogxdx+Rlog3+1
73 3re 3
74 73 a1i φx+3
75 1le3 13
76 74 75 jctir φx+313
77 14 adantr φx+R
78 36 rexri 1*
79 73 rexri 3*
80 1lt3 1<3
81 lbico1 1*3*1<3113
82 78 79 80 81 mp3an 113
83 0red φm130
84 elico2 13*m13m1mm<3
85 36 79 84 mp2an m13m1mm<3
86 85 simp1bi m13m
87 0red m130
88 1red m131
89 0lt1 0<1
90 89 a1i m130<1
91 85 simp2bi m131m
92 87 88 86 90 91 ltletrd m130<m
93 86 92 elrpd m13m+
94 12 adantr φm+T
95 9 94 subcld φm+FT
96 95 abscld φm+FT
97 93 96 sylan2 φm13FT
98 14 adantr φm13R
99 95 absge0d φm+0FT
100 93 99 sylan2 φm130FT
101 15 r19.21bi φm13FTR
102 83 97 98 100 101 letrd φm130R
103 102 ralrimiva φm130R
104 biidd m=10R0R
105 104 rspcv 113m130R0R
106 82 103 105 mpsyl φ0R
107 106 adantr φx+0R
108 77 107 jca φx+R0R
109 60 recnd φx+d1xKT
110 19 ad2antrr φx+d1xC
111 110 29 remulcld φx+d1xClogxdx
112 18 ad2antrr φx+d1xC0C
113 log1 log1=0
114 61 nncnd φx+d1xd
115 114 mulid2d φx+d1x1d=d
116 rpre x+x
117 116 adantl φx+x
118 fznnfl xd1xddx
119 117 118 syl φx+d1xddx
120 119 simplbda φx+d1xdx
121 115 120 eqbrtrd φx+d1x1dx
122 1red φx+d1x1
123 116 ad2antlr φx+d1xx
124 122 123 65 lemuldivd φx+d1x1dx1xd
125 121 124 mpbid φx+d1x1xd
126 1rp 1+
127 126 a1i φx+d1x1+
128 127 26 logled φx+d1x1xdlog1logxd
129 125 128 mpbid φx+d1xlog1logxd
130 113 129 eqbrtrrid φx+d1x0logxd
131 rpregt0 x+x0<x
132 131 ad2antlr φx+d1xx0<x
133 divge0 logxd0logxdx0<x0logxdx
134 27 130 132 133 syl21anc φx+d1x0logxdx
135 mulge0 C0Clogxdx0logxdx0Clogxdx
136 112 29 134 135 syl12anc φx+d1x0Clogxdx
137 absidm KTKT=KT
138 59 137 syl φx+d1xKT=KT
139 138 adantr φx+d1x3xdKT=KT
140 10 fvoveq1d m=xdFT=KT
141 fveq2 m=xdlogm=logxd
142 id m=xdm=xd
143 141 142 oveq12d m=xdlogmm=logxdxd
144 143 oveq2d m=xdClogmm=Clogxdxd
145 140 144 breq12d m=xdFTClogmmKTClogxdxd
146 13 ralrimiva φm3+∞FTClogmm
147 146 ad3antrrr φx+d1x3xdm3+∞FTClogmm
148 nndivre xdxd
149 117 23 148 syl2an φx+d1xxd
150 149 adantr φx+d1x3xdxd
151 simpr φx+d1x3xd3xd
152 elicopnf 3xd3+∞xd3xd
153 73 152 ax-mp xd3+∞xd3xd
154 150 151 153 sylanbrc φx+d1x3xdxd3+∞
155 145 147 154 rspcdva φx+d1x3xdKTClogxdxd
156 27 recnd φx+d1xlogxd
157 rpcnne0 x+xx0
158 157 ad2antlr φx+d1xxx0
159 65 rpcnne0d φx+d1xdd0
160 divdiv2 logxdxx0dd0logxdxd=logxddx
161 156 158 159 160 syl3anc φx+d1xlogxdxd=logxddx
162 div23 logxddxx0logxddx=logxdxd
163 156 114 158 162 syl3anc φx+d1xlogxddx=logxdxd
164 161 163 eqtrd φx+d1xlogxdxd=logxdxd
165 164 oveq2d φx+d1xClogxdxd=Clogxdxd
166 42 ad2antrr φx+d1xC
167 29 recnd φx+d1xlogxdx
168 166 167 114 mulassd φx+d1xClogxdxd=Clogxdxd
169 165 168 eqtr4d φx+d1xClogxdxd=Clogxdxd
170 169 adantr φx+d1x3xdClogxdxd=Clogxdxd
171 155 170 breqtrd φx+d1x3xdKTClogxdxd
172 139 171 eqbrtrd φx+d1x3xdKTClogxdxd
173 138 adantr φx+d1xxd<3KT=KT
174 140 breq1d m=xdFTRKTR
175 15 ad3antrrr φx+d1xxd<3m13FTR
176 149 adantr φx+d1xxd<3xd
177 125 adantr φx+d1xxd<31xd
178 simpr φx+d1xxd<3xd<3
179 elico2 13*xd13xd1xdxd<3
180 36 79 179 mp2an xd13xd1xdxd<3
181 176 177 178 180 syl3anbrc φx+d1xxd<3xd13
182 174 175 181 rspcdva φx+d1xxd<3KTR
183 173 182 eqbrtrd φx+d1xxd<3KTR
184 22 76 108 109 111 136 172 183 fsumharmonic φx+d=1xKTdd=1xClogxdx+Rlog3+1
185 42 adantr φx+C
186 21 185 167 fsummulc2 φx+Cd=1xlogxdx=d=1xClogxdx
187 186 oveq1d φx+Cd=1xlogxdx+Rlog3+1=d=1xClogxdx+Rlog3+1
188 184 187 breqtrrd φx+d=1xKTdCd=1xlogxdx+Rlog3+1
189 53 leabsd φx+Cd=1xlogxdx+Rlog3+1Cd=1xlogxdx+Rlog3+1
190 70 53 72 188 189 letrd φx+d=1xKTdCd=1xlogxdx+Rlog3+1
191 190 adantrr φx+1xd=1xKTdCd=1xlogxdx+Rlog3+1
192 16 52 53 64 191 o1le φx+d=1xKTd𝑂1