Metamath Proof Explorer


Theorem dchrisum0re

Description: Suppose X is a non-principal Dirichlet character with sum_ n e. NN , X ( n ) / n = 0 . Then X is a real character. Part of Lemma 9.4.4 of Shapiro, p. 382. (Contributed by Mario Carneiro, 5-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
Assertion dchrisum0re φX:BaseZ

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 eqid BaseZ=BaseZ
10 7 ssrab3 WD1˙
11 10 8 sselid φXD1˙
12 11 eldifad φXD
13 4 1 5 9 12 dchrf φX:BaseZ
14 13 ffnd φXFnBaseZ
15 13 ffvelrnda φxBaseZXx
16 fvco3 X:BaseZxBaseZ*Xx=Xx
17 13 16 sylan φxBaseZ*Xx=Xx
18 logno1 ¬x+logx𝑂1
19 1red φ*XX1
20 eqid UnitZ=UnitZ
21 3 nnnn0d φN0
22 1 zncrng N0ZCRing
23 21 22 syl φZCRing
24 crngring ZCRingZRing
25 23 24 syl φZRing
26 eqid 1Z=1Z
27 20 26 1unit ZRing1ZUnitZ
28 25 27 syl φ1ZUnitZ
29 eqid L-11Z=L-11Z
30 eqidd φfW1Z=1Z
31 1 2 3 4 5 6 7 20 28 29 30 rpvmasum2 φx+ϕNn1xL-11ZΛnnlogx1W𝑂1
32 31 adantr φ*XXx+ϕNn1xL-11ZΛnnlogx1W𝑂1
33 3 phicld φϕN
34 33 nnnn0d φϕN0
35 34 adantr φx+ϕN0
36 35 nn0red φx+ϕN
37 fzfid φx+1xFin
38 inss1 1xL-11Z1x
39 ssfi 1xFin1xL-11Z1x1xL-11ZFin
40 37 38 39 sylancl φx+1xL-11ZFin
41 elinel1 n1xL-11Zn1x
42 elfznn n1xn
43 42 adantl φx+n1xn
44 41 43 sylan2 φx+n1xL-11Zn
45 vmacl nΛn
46 nndivre ΛnnΛnn
47 45 46 mpancom nΛnn
48 44 47 syl φx+n1xL-11ZΛnn
49 40 48 fsumrecl φx+n1xL-11ZΛnn
50 36 49 remulcld φx+ϕNn1xL-11ZΛnn
51 relogcl x+logx
52 51 adantl φx+logx
53 1re 1
54 4 5 dchrfi NDFin
55 3 54 syl φDFin
56 difss D1˙D
57 10 56 sstri WD
58 ssfi DFinWDWFin
59 55 57 58 sylancl φWFin
60 hashcl WFinW0
61 59 60 syl φW0
62 61 nn0red φW
63 resubcl 1W1W
64 53 62 63 sylancr φ1W
65 64 adantr φx+1W
66 52 65 remulcld φx+logx1W
67 50 66 resubcld φx+ϕNn1xL-11ZΛnnlogx1W
68 67 recnd φx+ϕNn1xL-11ZΛnnlogx1W
69 68 adantlr φ*XXx+ϕNn1xL-11ZΛnnlogx1W
70 51 adantl φ*XXx+logx
71 70 recnd φ*XXx+logx
72 51 ad2antrl φ*XXx+1xlogx
73 66 ad2ant2r φ*XXx+1xlogx1W
74 72 73 readdcld φ*XXx+1xlogx+logx1W
75 0red φ*XXx+1x0
76 50 ad2ant2r φ*XXx+1xϕNn1xL-11ZΛnn
77 2re 2
78 77 a1i φ*XXx+1x2
79 62 ad2antrr φ*XXx+1xW
80 78 79 resubcld φ*XXx+1x2W
81 log1 log1=0
82 simprr φ*XXx+1x1x
83 1rp 1+
84 simprl φ*XXx+1xx+
85 logleb 1+x+1xlog1logx
86 83 84 85 sylancr φ*XXx+1x1xlog1logx
87 82 86 mpbid φ*XXx+1xlog1logx
88 81 87 eqbrtrrid φ*XXx+1x0logx
89 59 ad2antrr φ*XXx+1xWFin
90 eqid invgG=invgG
91 4 5 12 90 dchrinv φinvgGX=*X
92 4 dchrabl NGAbel
93 3 92 syl φGAbel
94 ablgrp GAbelGGrp
95 93 94 syl φGGrp
96 5 90 grpinvcl GGrpXDinvgGXD
97 95 12 96 syl2anc φinvgGXD
98 91 97 eqeltrrd φ*XD
99 eldifsni XD1˙X1˙
100 11 99 syl φX1˙
101 5 6 grpidcl GGrp1˙D
102 95 101 syl φ1˙D
103 5 90 95 12 102 grpinv11 φinvgGX=invgG1˙X=1˙
104 103 necon3bid φinvgGXinvgG1˙X1˙
105 100 104 mpbird φinvgGXinvgG1˙
106 6 90 grpinvid GGrpinvgG1˙=1˙
107 95 106 syl φinvgG1˙=1˙
108 105 91 107 3netr3d φ*X1˙
109 eldifsn *XD1˙*XD*X1˙
110 98 108 109 sylanbrc φ*XD1˙
111 nnuz =1
112 1zzd φ1
113 2fveq3 n=mXLn=XLm
114 id n=mn=m
115 113 114 oveq12d n=mXLnn=XLmm
116 115 fveq2d n=mXLnn=XLmm
117 eqid nXLnn=nXLnn
118 fvex XLmmV
119 116 117 118 fvmpt mnXLnnm=XLmm
120 119 adantl φmnXLnnm=XLmm
121 nnre mm
122 121 adantl φmm
123 122 cjred φmm=m
124 123 oveq2d φmXLmm=XLmm
125 13 adantr φmX:BaseZ
126 1 9 2 znzrhfo N0L:ontoBaseZ
127 21 126 syl φL:ontoBaseZ
128 fof L:ontoBaseZL:BaseZ
129 127 128 syl φL:BaseZ
130 nnz mm
131 ffvelrn L:BaseZmLmBaseZ
132 129 130 131 syl2an φmLmBaseZ
133 125 132 ffvelrnd φmXLm
134 nncn mm
135 134 adantl φmm
136 nnne0 mm0
137 136 adantl φmm0
138 133 135 137 cjdivd φmXLmm=XLmm
139 fvco3 X:BaseZLmBaseZ*XLm=XLm
140 125 132 139 syl2anc φm*XLm=XLm
141 140 oveq1d φm*XLmm=XLmm
142 124 138 141 3eqtr4d φmXLmm=*XLmm
143 120 142 eqtrd φmnXLnnm=*XLmm
144 133 cjcld φmXLm
145 144 135 137 divcld φmXLmm
146 141 145 eqeltrd φm*XLmm
147 eqid aXLaa=aXLaa
148 1 2 3 4 5 6 12 100 147 dchrmusumlema φtc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcy
149 simprrl φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyseq1+aXLaat
150 8 adantr φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyXW
151 3 adantr φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyN
152 12 adantr φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyXD
153 100 adantr φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyX1˙
154 simprl φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyc0+∞
155 simprrr φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyy1+∞seq1+aXLaaytcy
156 1 2 151 4 5 6 152 153 147 154 149 155 7 dchrvmaeq0 φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyXWt=0
157 150 156 mpbid φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyt=0
158 149 157 breqtrd φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyseq1+aXLaa0
159 158 rexlimdvaa φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyseq1+aXLaa0
160 159 exlimdv φtc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyseq1+aXLaa0
161 148 160 mpd φseq1+aXLaa0
162 seqex seq1+nXLnnV
163 162 a1i φseq1+nXLnnV
164 2fveq3 a=mXLa=XLm
165 id a=ma=m
166 164 165 oveq12d a=mXLaa=XLmm
167 ovex XLmmV
168 166 147 167 fvmpt maXLaam=XLmm
169 168 adantl φmaXLaam=XLmm
170 133 135 137 divcld φmXLmm
171 169 170 eqeltrd φmaXLaam
172 111 112 171 serf φseq1+aXLaa:
173 172 ffvelrnda φkseq1+aXLaak
174 fzfid φk1kFin
175 simpl φkφ
176 elfznn m1km
177 175 176 170 syl2an φkm1kXLmm
178 174 177 fsumcj φkm=1kXLmm=m=1kXLmm
179 175 176 169 syl2an φkm1kaXLaam=XLmm
180 simpr φkk
181 180 111 eleqtrdi φkk1
182 179 181 177 fsumser φkm=1kXLmm=seq1+aXLaak
183 182 fveq2d φkm=1kXLmm=seq1+aXLaak
184 175 176 120 syl2an φkm1knXLnnm=XLmm
185 170 cjcld φmXLmm
186 175 176 185 syl2an φkm1kXLmm
187 184 181 186 fsumser φkm=1kXLmm=seq1+nXLnnk
188 178 183 187 3eqtr3rd φkseq1+nXLnnk=seq1+aXLaak
189 111 161 163 112 173 188 climcj φseq1+nXLnn0
190 cj0 0=0
191 189 190 breqtrdi φseq1+nXLnn0
192 111 112 143 146 191 isumclim φm*XLmm=0
193 fveq1 y=*XyLm=*XLm
194 193 oveq1d y=*XyLmm=*XLmm
195 194 sumeq2sdv y=*XmyLmm=m*XLmm
196 195 eqeq1d y=*XmyLmm=0m*XLmm=0
197 196 7 elrab2 *XW*XD1˙m*XLmm=0
198 110 192 197 sylanbrc φ*XW
199 198 ad2antrr φ*XXx+1x*XW
200 8 ad2antrr φ*XXx+1xXW
201 simplr φ*XXx+1x*XX
202 89 199 200 201 nehash2 φ*XXx+1x2W
203 suble0 2W2W02W
204 77 79 203 sylancr φ*XXx+1x2W02W
205 202 204 mpbird φ*XXx+1x2W0
206 80 75 72 88 205 lemul2ad φ*XXx+1xlogx2Wlogx0
207 df-2 2=1+1
208 207 oveq1i 2W=1+1-W
209 1cnd φ*XXx+1x1
210 79 recnd φ*XXx+1xW
211 209 209 210 addsubassd φ*XXx+1x1+1-W=1+1-W
212 208 211 eqtrid φ*XXx+1x2W=1+1-W
213 212 oveq2d φ*XXx+1xlogx2W=logx1+1-W
214 71 adantrr φ*XXx+1xlogx
215 64 ad2antrr φ*XXx+1x1W
216 215 recnd φ*XXx+1x1W
217 214 209 216 adddid φ*XXx+1xlogx1+1-W=logx1+logx1W
218 214 mulid1d φ*XXx+1xlogx1=logx
219 218 oveq1d φ*XXx+1xlogx1+logx1W=logx+logx1W
220 213 217 219 3eqtrd φ*XXx+1xlogx2W=logx+logx1W
221 214 mul01d φ*XXx+1xlogx0=0
222 206 220 221 3brtr3d φ*XXx+1xlogx+logx1W0
223 33 nnred φϕN
224 223 ad2antrr φ*XXx+1xϕN
225 49 ad2ant2r φ*XXx+1xn1xL-11ZΛnn
226 34 ad2antrr φ*XXx+1xϕN0
227 226 nn0ge0d φ*XXx+1x0ϕN
228 44 45 syl φx+n1xL-11ZΛn
229 vmage0 n0Λn
230 44 229 syl φx+n1xL-11Z0Λn
231 44 nnred φx+n1xL-11Zn
232 44 nngt0d φx+n1xL-11Z0<n
233 divge0 Λn0Λnn0<n0Λnn
234 228 230 231 232 233 syl22anc φx+n1xL-11Z0Λnn
235 40 48 234 fsumge0 φx+0n1xL-11ZΛnn
236 235 ad2ant2r φ*XXx+1x0n1xL-11ZΛnn
237 224 225 227 236 mulge0d φ*XXx+1x0ϕNn1xL-11ZΛnn
238 74 75 76 222 237 letrd φ*XXx+1xlogx+logx1WϕNn1xL-11ZΛnn
239 leaddsub logxlogx1WϕNn1xL-11ZΛnnlogx+logx1WϕNn1xL-11ZΛnnlogxϕNn1xL-11ZΛnnlogx1W
240 72 73 76 239 syl3anc φ*XXx+1xlogx+logx1WϕNn1xL-11ZΛnnlogxϕNn1xL-11ZΛnnlogx1W
241 238 240 mpbid φ*XXx+1xlogxϕNn1xL-11ZΛnnlogx1W
242 72 88 absidd φ*XXx+1xlogx=logx
243 67 ad2ant2r φ*XXx+1xϕNn1xL-11ZΛnnlogx1W
244 75 72 243 88 241 letrd φ*XXx+1x0ϕNn1xL-11ZΛnnlogx1W
245 243 244 absidd φ*XXx+1xϕNn1xL-11ZΛnnlogx1W=ϕNn1xL-11ZΛnnlogx1W
246 241 242 245 3brtr4d φ*XXx+1xlogxϕNn1xL-11ZΛnnlogx1W
247 19 32 69 71 246 o1le φ*XXx+logx𝑂1
248 247 ex φ*XXx+logx𝑂1
249 248 necon1bd φ¬x+logx𝑂1*X=X
250 18 249 mpi φ*X=X
251 250 adantr φxBaseZ*X=X
252 251 fveq1d φxBaseZ*Xx=Xx
253 17 252 eqtr3d φxBaseZXx=Xx
254 15 253 cjrebd φxBaseZXx
255 254 ralrimiva φxBaseZXx
256 ffnfv X:BaseZXFnBaseZxBaseZXx
257 14 255 256 sylanbrc φX:BaseZ