Metamath Proof Explorer


Theorem dchrisum0lem2

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
dchrisum0lem2.k K=aXLaa
dchrisum0lem2.e φE0+∞
dchrisum0lem2.t φseq1+KT
dchrisum0lem2.3 φy1+∞seq1+KyTEy
Assertion dchrisum0lem2 φx+m=1xd=1x2mXLmmd𝑂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 dchrisum0lem2.k K=aXLaa
16 dchrisum0lem2.e φE0+∞
17 dchrisum0lem2.t φseq1+KT
18 dchrisum0lem2.3 φy1+∞seq1+KyTEy
19 2cnd φx+2
20 rpcn x+x
21 20 adantl φx+x
22 fzfid φx+1xFin
23 7 ssrab3 WD1˙
24 23 8 sselid φXD1˙
25 24 eldifad φXD
26 25 ad2antrr φx+m1xXD
27 elfzelz m1xm
28 27 adantl φx+m1xm
29 4 1 5 2 26 28 dchrzrhcl φx+m1xXLm
30 elfznn m1xm
31 30 nnrpd m1xm+
32 31 adantl φx+m1xm+
33 32 rpcnd φx+m1xm
34 32 rpne0d φx+m1xm0
35 29 33 34 divcld φx+m1xXLmm
36 22 35 fsumcl φx+m=1xXLmm
37 21 36 mulcld φx+xm=1xXLmm
38 rpssre +
39 2cn 2
40 o1const +2x+2𝑂1
41 38 39 40 mp2an x+2𝑂1
42 41 a1i φx+2𝑂1
43 38 a1i φ+
44 1red φ1
45 elrege0 E0+∞E0E
46 45 simplbi E0+∞E
47 16 46 syl φE
48 21 36 absmuld φx+xm=1xXLmm=xm=1xXLmm
49 rprege0 x+x0x
50 49 adantl φx+x0x
51 absid x0xx=x
52 50 51 syl φx+x=x
53 52 oveq1d φx+xm=1xXLmm=xm=1xXLmm
54 48 53 eqtrd φx+xm=1xXLmm=xm=1xXLmm
55 54 adantrr φx+1xxm=1xXLmm=xm=1xXLmm
56 36 adantrr φx+1xm=1xXLmm
57 56 subid1d φx+1xm=1xXLmm0=m=1xXLmm
58 30 adantl φx+m1xm
59 2fveq3 a=mXLa=XLm
60 id a=ma=m
61 59 60 oveq12d a=mXLaa=XLmm
62 ovex XLaaV
63 61 15 62 fvmpt3i mKm=XLmm
64 58 63 syl φx+m1xKm=XLmm
65 64 adantlrr φx+1xm1xKm=XLmm
66 rpregt0 x+x0<x
67 66 ad2antrl φx+1xx0<x
68 67 simpld φx+1xx
69 simprr φx+1x1x
70 flge1nn x1xx
71 68 69 70 syl2anc φx+1xx
72 nnuz =1
73 71 72 eleqtrdi φx+1xx1
74 35 adantlrr φx+1xm1xXLmm
75 65 73 74 fsumser φx+1xm=1xXLmm=seq1+Kx
76 eldifsni XD1˙X1˙
77 24 76 syl φX1˙
78 1 2 3 4 5 6 25 77 15 16 17 18 7 dchrvmaeq0 φXWT=0
79 8 78 mpbid φT=0
80 79 adantr φx+1xT=0
81 80 eqcomd φx+1x0=T
82 75 81 oveq12d φx+1xm=1xXLmm0=seq1+KxT
83 57 82 eqtr3d φx+1xm=1xXLmm=seq1+KxT
84 83 fveq2d φx+1xm=1xXLmm=seq1+KxT
85 2fveq3 y=xseq1+Ky=seq1+Kx
86 85 fvoveq1d y=xseq1+KyT=seq1+KxT
87 oveq2 y=xEy=Ex
88 86 87 breq12d y=xseq1+KyTEyseq1+KxTEx
89 18 adantr φx+1xy1+∞seq1+KyTEy
90 1re 1
91 elicopnf 1x1+∞x1x
92 90 91 ax-mp x1+∞x1x
93 68 69 92 sylanbrc φx+1xx1+∞
94 88 89 93 rspcdva φx+1xseq1+KxTEx
95 84 94 eqbrtrd φx+1xm=1xXLmmEx
96 56 abscld φx+1xm=1xXLmm
97 47 adantr φx+1xE
98 lemuldiv2 m=1xXLmmEx0<xxm=1xXLmmEm=1xXLmmEx
99 96 97 67 98 syl3anc φx+1xxm=1xXLmmEm=1xXLmmEx
100 95 99 mpbird φx+1xxm=1xXLmmE
101 55 100 eqbrtrd φx+1xxm=1xXLmmE
102 43 37 44 47 101 elo1d φx+xm=1xXLmm𝑂1
103 19 37 42 102 o1mul2 φx+2xm=1xXLmm𝑂1
104 fzfid φx+m1x1x2mFin
105 32 rpsqrtcld φx+m1xm+
106 105 rpcnd φx+m1xm
107 105 rpne0d φx+m1xm0
108 29 106 107 divcld φx+m1xXLmm
109 108 adantr φx+m1xd1x2mXLmm
110 elfznn d1x2md
111 110 adantl φx+m1xd1x2md
112 111 nnrpd φx+m1xd1x2md+
113 112 rpsqrtcld φx+m1xd1x2md+
114 113 rpcnd φx+m1xd1x2md
115 113 rpne0d φx+m1xd1x2md0
116 109 114 115 divcld φx+m1xd1x2mXLmmd
117 104 116 fsumcl φx+m1xd=1x2mXLmmd
118 22 117 fsumcl φx+m=1xd=1x2mXLmmd
119 mulcl 2xm=1xXLmm2xm=1xXLmm
120 39 37 119 sylancr φx+2xm=1xXLmm
121 2re 2
122 simpr φx+x+
123 2z 2
124 rpexpcl x+2x2+
125 122 123 124 sylancl φx+x2+
126 rpdivcl x2+m+x2m+
127 125 31 126 syl2an φx+m1xx2m+
128 127 rpsqrtcld φx+m1xx2m+
129 128 rpred φx+m1xx2m
130 remulcl 2x2m2x2m
131 121 129 130 sylancr φx+m1x2x2m
132 131 recnd φx+m1x2x2m
133 108 132 mulcld φx+m1xXLmm2x2m
134 22 117 133 fsumsub φx+m=1xd=1x2mXLmmdXLmm2x2m=m=1xd=1x2mXLmmdm=1xXLmm2x2m
135 113 rpcnne0d φx+m1xd1x2mdd0
136 reccl dd01d
137 135 136 syl φx+m1xd1x2m1d
138 104 137 fsumcl φx+m1xd=1x2m1d
139 108 138 132 subdid φx+m1xXLmmd=1x2m1d2x2m=XLmmd=1x2m1dXLmm2x2m
140 fveq2 y=x2my=x2m
141 140 oveq2d y=x2m1y=1x2m
142 141 sumeq1d y=x2md=1y1d=d=1x2m1d
143 fveq2 y=x2my=x2m
144 143 oveq2d y=x2m2y=2x2m
145 142 144 oveq12d y=x2md=1y1d2y=d=1x2m1d2x2m
146 ovex d=1y1d2yV
147 145 13 146 fvmpt3i x2m+Hx2m=d=1x2m1d2x2m
148 127 147 syl φx+m1xHx2m=d=1x2m1d2x2m
149 148 oveq2d φx+m1xXLmmHx2m=XLmmd=1x2m1d2x2m
150 109 114 115 divrecd φx+m1xd1x2mXLmmd=XLmm1d
151 150 sumeq2dv φx+m1xd=1x2mXLmmd=d=1x2mXLmm1d
152 104 108 137 fsummulc2 φx+m1xXLmmd=1x2m1d=d=1x2mXLmm1d
153 151 152 eqtr4d φx+m1xd=1x2mXLmmd=XLmmd=1x2m1d
154 153 oveq1d φx+m1xd=1x2mXLmmdXLmm2x2m=XLmmd=1x2m1dXLmm2x2m
155 139 149 154 3eqtr4d φx+m1xXLmmHx2m=d=1x2mXLmmdXLmm2x2m
156 155 sumeq2dv φx+m=1xXLmmHx2m=m=1xd=1x2mXLmmdXLmm2x2m
157 mulcl 2x2x
158 39 21 157 sylancr φx+2x
159 22 158 35 fsummulc2 φx+2xm=1xXLmm=m=1x2xXLmm
160 19 21 36 mulassd φx+2xm=1xXLmm=2xm=1xXLmm
161 158 adantr φx+m1x2x
162 161 108 106 107 div12d φx+m1x2xXLmmm=XLmm2xm
163 105 rpcnne0d φx+m1xmm0
164 divdiv1 XLmmm0mm0XLmmm=XLmmm
165 29 163 163 164 syl3anc φx+m1xXLmmm=XLmmm
166 32 rprege0d φx+m1xm0m
167 remsqsqrt m0mmm=m
168 166 167 syl φx+m1xmm=m
169 168 oveq2d φx+m1xXLmmm=XLmm
170 165 169 eqtr2d φx+m1xXLmm=XLmmm
171 170 oveq2d φx+m1x2xXLmm=2xXLmmm
172 125 adantr φx+m1xx2+
173 172 rprege0d φx+m1xx20x2
174 sqrtdiv x20x2m+x2m=x2m
175 173 32 174 syl2anc φx+m1xx2m=x2m
176 49 ad2antlr φx+m1xx0x
177 sqrtsq x0xx2=x
178 176 177 syl φx+m1xx2=x
179 178 oveq1d φx+m1xx2m=xm
180 175 179 eqtrd φx+m1xx2m=xm
181 180 oveq2d φx+m1x2x2m=2xm
182 2cnd φx+m1x2
183 21 adantr φx+m1xx
184 divass 2xmm02xm=2xm
185 182 183 163 184 syl3anc φx+m1x2xm=2xm
186 181 185 eqtr4d φx+m1x2x2m=2xm
187 186 oveq2d φx+m1xXLmm2x2m=XLmm2xm
188 162 171 187 3eqtr4d φx+m1x2xXLmm=XLmm2x2m
189 188 sumeq2dv φx+m=1x2xXLmm=m=1xXLmm2x2m
190 159 160 189 3eqtr3d φx+2xm=1xXLmm=m=1xXLmm2x2m
191 190 oveq2d φx+m=1xd=1x2mXLmmd2xm=1xXLmm=m=1xd=1x2mXLmmdm=1xXLmm2x2m
192 134 156 191 3eqtr4d φx+m=1xXLmmHx2m=m=1xd=1x2mXLmmd2xm=1xXLmm
193 192 mpteq2dva φx+m=1xXLmmHx2m=x+m=1xd=1x2mXLmmd2xm=1xXLmm
194 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dchrisum0lem2a φx+m=1xXLmmHx2m𝑂1
195 193 194 eqeltrrd φx+m=1xd=1x2mXLmmd2xm=1xXLmm𝑂1
196 118 120 195 o1dif φx+m=1xd=1x2mXLmmd𝑂1x+2xm=1xXLmm𝑂1
197 103 196 mpbird φx+m=1xd=1x2mXLmmd𝑂1