Metamath Proof Explorer


Theorem dchrisum0lem2a

Description: Lemma for dchrisum0 . (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rpvmasum.z Z=/N
rpvmasum.l L=ℤRHomZ
rpvmasum.a φN
rpvmasum2.g G=DChrN
rpvmasum2.d D=BaseG
rpvmasum2.1 1˙=0G
rpvmasum2.w W=yD1˙|myLmm=0
dchrisum0.b φXW
dchrisum0lem1.f F=aXLaa
dchrisum0.c φC0+∞
dchrisum0.s φseq1+FS
dchrisum0.1 φy1+∞seq1+FySCy
dchrisum0lem2.h H=y+d=1y1d2y
dchrisum0lem2.u φHU
Assertion dchrisum0lem2a φx+m=1xXLmmHx2m𝑂1

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z=/N
2 rpvmasum.l L=ℤRHomZ
3 rpvmasum.a φN
4 rpvmasum2.g G=DChrN
5 rpvmasum2.d D=BaseG
6 rpvmasum2.1 1˙=0G
7 rpvmasum2.w W=yD1˙|myLmm=0
8 dchrisum0.b φXW
9 dchrisum0lem1.f F=aXLaa
10 dchrisum0.c φC0+∞
11 dchrisum0.s φseq1+FS
12 dchrisum0.1 φy1+∞seq1+FySCy
13 dchrisum0lem2.h H=y+d=1y1d2y
14 dchrisum0lem2.u φHU
15 fzfid φx+1xFin
16 simpl φx+φ
17 elfznn m1xm
18 7 ssrab3 WD1˙
19 18 8 sselid φXD1˙
20 19 eldifad φXD
21 20 adantr φmXD
22 nnz mm
23 22 adantl φmm
24 4 1 5 2 21 23 dchrzrhcl φmXLm
25 nnrp mm+
26 25 adantl φmm+
27 26 rpsqrtcld φmm+
28 27 rpcnd φmm
29 27 rpne0d φmm0
30 24 28 29 divcld φmXLmm
31 16 17 30 syl2an φx+m1xXLmm
32 15 31 fsumcl φx+m=1xXLmm
33 rlimcl HUU
34 14 33 syl φU
35 34 adantr φx+U
36 0xr 0*
37 0lt1 0<1
38 df-ioo .=x*,y*z*|x<zz<y
39 df-ico .=x*,y*z*|xzz<y
40 xrltletr 0*1*w*0<11w0<w
41 38 39 40 ixxss1 0*0<11+∞0+∞
42 36 37 41 mp2an 1+∞0+∞
43 ioorp 0+∞=+
44 42 43 sseqtri 1+∞+
45 resmpt 1+∞+x+m=1xXLmm1+∞=x1+∞m=1xXLmm
46 44 45 ax-mp x+m=1xXLmm1+∞=x1+∞m=1xXLmm
47 44 sseli x1+∞x+
48 17 adantl φx+m1xm
49 2fveq3 a=mXLa=XLm
50 fveq2 a=ma=m
51 49 50 oveq12d a=mXLaa=XLmm
52 ovex XLaaV
53 51 9 52 fvmpt3i mFm=XLmm
54 48 53 syl φx+m1xFm=XLmm
55 47 54 sylanl2 φx1+∞m1xFm=XLmm
56 1re 1
57 elicopnf 1x1+∞x1x
58 56 57 ax-mp x1+∞x1x
59 flge1nn x1xx
60 58 59 sylbi x1+∞x
61 60 adantl φx1+∞x
62 nnuz =1
63 61 62 eleqtrdi φx1+∞x1
64 47 31 sylanl2 φx1+∞m1xXLmm
65 55 63 64 fsumser φx1+∞m=1xXLmm=seq1+Fx
66 65 mpteq2dva φx1+∞m=1xXLmm=x1+∞seq1+Fx
67 46 66 eqtrid φx+m=1xXLmm1+∞=x1+∞seq1+Fx
68 fveq2 m=xseq1+Fm=seq1+Fx
69 rpssre +
70 69 a1i φ+
71 44 70 sstrid φ1+∞
72 1zzd φ1
73 51 cbvmptv aXLaa=mXLmm
74 9 73 eqtri F=mXLmm
75 30 74 fmptd φF:
76 75 ffvelrnda φmFm
77 62 72 76 serf φseq1+F:
78 77 feqmptd φseq1+F=mseq1+Fm
79 78 11 eqbrtrrd φmseq1+FmS
80 77 ffvelrnda φmseq1+Fm
81 58 simprbi x1+∞1x
82 81 adantl φx1+∞1x
83 62 68 71 72 79 80 82 climrlim2 φx1+∞seq1+FxS
84 rlimo1 x1+∞seq1+FxSx1+∞seq1+Fx𝑂1
85 83 84 syl φx1+∞seq1+Fx𝑂1
86 67 85 eqeltrd φx+m=1xXLmm1+∞𝑂1
87 32 fmpttd φx+m=1xXLmm:+
88 1red φ1
89 87 70 88 o1resb φx+m=1xXLmm𝑂1x+m=1xXLmm1+∞𝑂1
90 86 89 mpbird φx+m=1xXLmm𝑂1
91 o1const +Ux+U𝑂1
92 69 34 91 sylancr φx+U𝑂1
93 32 35 90 92 o1mul2 φx+m=1xXLmmU𝑂1
94 simpr φx+x+
95 2z 2
96 rpexpcl x+2x2+
97 94 95 96 sylancl φx+x2+
98 17 nnrpd m1xm+
99 rpdivcl x2+m+x2m+
100 97 98 99 syl2an φx+m1xx2m+
101 13 divsqrsumf H:+
102 101 ffvelrni x2m+Hx2m
103 100 102 syl φx+m1xHx2m
104 103 recnd φx+m1xHx2m
105 31 104 mulcld φx+m1xXLmmHx2m
106 15 105 fsumcl φx+m=1xXLmmHx2m
107 32 35 mulcld φx+m=1xXLmmU
108 14 ad2antrr φx+m1xHU
109 108 33 syl φx+m1xU
110 31 109 mulcld φx+m1xXLmmU
111 15 105 110 fsumsub φx+m=1xXLmmHx2mXLmmU=m=1xXLmmHx2mm=1xXLmmU
112 31 104 109 subdid φx+m1xXLmmHx2mU=XLmmHx2mXLmmU
113 112 sumeq2dv φx+m=1xXLmmHx2mU=m=1xXLmmHx2mXLmmU
114 15 35 31 fsummulc1 φx+m=1xXLmmU=m=1xXLmmU
115 114 oveq2d φx+m=1xXLmmHx2mm=1xXLmmU=m=1xXLmmHx2mm=1xXLmmU
116 111 113 115 3eqtr4d φx+m=1xXLmmHx2mU=m=1xXLmmHx2mm=1xXLmmU
117 116 mpteq2dva φx+m=1xXLmmHx2mU=x+m=1xXLmmHx2mm=1xXLmmU
118 104 109 subcld φx+m1xHx2mU
119 31 118 mulcld φx+m1xXLmmHx2mU
120 15 119 fsumcl φx+m=1xXLmmHx2mU
121 120 abscld φx+m=1xXLmmHx2mU
122 119 abscld φx+m1xXLmmHx2mU
123 15 122 fsumrecl φx+m=1xXLmmHx2mU
124 1red φx+1
125 15 119 fsumabs φx+m=1xXLmmHx2mUm=1xXLmmHx2mU
126 rprege0 x+x0x
127 126 adantl φx+x0x
128 127 simpld φx+x
129 reflcl xx
130 128 129 syl φx+x
131 130 94 rerpdivcld φx+xx
132 simplr φx+m1xx+
133 132 rprecred φx+m1x1x
134 31 abscld φx+m1xXLmm
135 98 rpsqrtcld m1xm+
136 135 adantl φx+m1xm+
137 136 rprecred φx+m1x1m
138 118 abscld φx+m1xHx2mU
139 136 132 rpdivcld φx+m1xmx+
140 69 139 sselid φx+m1xmx
141 31 absge0d φx+m1x0XLmm
142 118 absge0d φx+m1x0Hx2mU
143 16 17 24 syl2an φx+m1xXLm
144 136 rpcnd φx+m1xm
145 136 rpne0d φx+m1xm0
146 143 144 145 absdivd φx+m1xXLmm=XLmm
147 136 rprege0d φx+m1xm0m
148 absid m0mm=m
149 147 148 syl φx+m1xm=m
150 149 oveq2d φx+m1xXLmm=XLmm
151 146 150 eqtrd φx+m1xXLmm=XLmm
152 143 abscld φx+m1xXLm
153 1red φx+m1x1
154 eqid BaseZ=BaseZ
155 20 ad2antrr φx+m1xXD
156 3 nnnn0d φN0
157 1 154 2 znzrhfo N0L:ontoBaseZ
158 fof L:ontoBaseZL:BaseZ
159 156 157 158 3syl φL:BaseZ
160 159 adantr φx+L:BaseZ
161 elfzelz m1xm
162 ffvelrn L:BaseZmLmBaseZ
163 160 161 162 syl2an φx+m1xLmBaseZ
164 4 5 1 154 155 163 dchrabs2 φx+m1xXLm1
165 152 153 136 164 lediv1dd φx+m1xXLmm1m
166 151 165 eqbrtrd φx+m1xXLmm1m
167 13 108 divsqrtsum2 φx+m1xx2m+Hx2mU1x2m
168 100 167 mpdan φx+m1xHx2mU1x2m
169 97 rprege0d φx+x20x2
170 sqrtdiv x20x2m+x2m=x2m
171 169 98 170 syl2an φx+m1xx2m=x2m
172 126 ad2antlr φx+m1xx0x
173 sqrtsq x0xx2=x
174 172 173 syl φx+m1xx2=x
175 174 oveq1d φx+m1xx2m=xm
176 171 175 eqtrd φx+m1xx2m=xm
177 176 oveq2d φx+m1x1x2m=1xm
178 rpcnne0 x+xx0
179 178 ad2antlr φx+m1xxx0
180 136 rpcnne0d φx+m1xmm0
181 recdiv xx0mm01xm=mx
182 179 180 181 syl2anc φx+m1x1xm=mx
183 177 182 eqtrd φx+m1x1x2m=mx
184 168 183 breqtrd φx+m1xHx2mUmx
185 134 137 138 140 141 142 166 184 lemul12ad φx+m1xXLmmHx2mU1mmx
186 31 118 absmuld φx+m1xXLmmHx2mU=XLmmHx2mU
187 1cnd φx+m1x1
188 dmdcan mm0xx01mx1m=1x
189 180 179 187 188 syl3anc φx+m1xmx1m=1x
190 139 rpcnd φx+m1xmx
191 reccl mm01m
192 180 191 syl φx+m1x1m
193 190 192 mulcomd φx+m1xmx1m=1mmx
194 189 193 eqtr3d φx+m1x1x=1mmx
195 185 186 194 3brtr4d φx+m1xXLmmHx2mU1x
196 15 122 133 195 fsumle φx+m=1xXLmmHx2mUm=1x1x
197 flge0nn0 x0xx0
198 hashfz1 x01x=x
199 127 197 198 3syl φx+1x=x
200 199 oveq1d φx+1x1x=x1x
201 94 rpreccld φx+1x+
202 201 rpcnd φx+1x
203 fsumconst 1xFin1xm=1x1x=1x1x
204 15 202 203 syl2anc φx+m=1x1x=1x1x
205 130 recnd φx+x
206 178 adantl φx+xx0
207 206 simpld φx+x
208 206 simprd φx+x0
209 205 207 208 divrecd φx+xx=x1x
210 200 204 209 3eqtr4d φx+m=1x1x=xx
211 196 210 breqtrd φx+m=1xXLmmHx2mUxx
212 flle xxx
213 128 212 syl φx+xx
214 128 recnd φx+x
215 214 mulid1d φx+x1=x
216 213 215 breqtrrd φx+xx1
217 rpregt0 x+x0<x
218 217 adantl φx+x0<x
219 ledivmul x1x0<xxx1xx1
220 130 124 218 219 syl3anc φx+xx1xx1
221 216 220 mpbird φx+xx1
222 123 131 124 211 221 letrd φx+m=1xXLmmHx2mU1
223 121 123 124 125 222 letrd φx+m=1xXLmmHx2mU1
224 223 adantrr φx+1xm=1xXLmmHx2mU1
225 70 120 88 88 224 elo1d φx+m=1xXLmmHx2mU𝑂1
226 117 225 eqeltrrd φx+m=1xXLmmHx2mm=1xXLmmU𝑂1
227 106 107 226 o1dif φx+m=1xXLmmHx2m𝑂1x+m=1xXLmmU𝑂1
228 93 227 mpbird φx+m=1xXLmmHx2m𝑂1