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 = ℤRHom Z
rpvmasum.a φ N
rpvmasum2.g G = DChr N
rpvmasum2.d D = Base G
rpvmasum2.1 1 ˙ = 0 G
rpvmasum2.w W = y D 1 ˙ | m y L m m = 0
dchrisum0.b φ X W
Assertion dchrisum0re φ X : Base Z

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z = /N
2 rpvmasum.l L = ℤRHom Z
3 rpvmasum.a φ N
4 rpvmasum2.g G = DChr N
5 rpvmasum2.d D = Base G
6 rpvmasum2.1 1 ˙ = 0 G
7 rpvmasum2.w W = y D 1 ˙ | m y L m m = 0
8 dchrisum0.b φ X W
9 eqid Base Z = Base Z
10 7 ssrab3 W D 1 ˙
11 10 8 sselid φ X D 1 ˙
12 11 eldifad φ X D
13 4 1 5 9 12 dchrf φ X : Base Z
14 13 ffnd φ X Fn Base Z
15 13 ffvelrnda φ x Base Z X x
16 fvco3 X : Base Z x Base Z * X x = X x
17 13 16 sylan φ x Base Z * X x = X x
18 logno1 ¬ x + log x 𝑂1
19 1red φ * X X 1
20 eqid Unit Z = Unit Z
21 3 nnnn0d φ N 0
22 1 zncrng N 0 Z CRing
23 21 22 syl φ Z CRing
24 crngring Z CRing Z Ring
25 23 24 syl φ Z Ring
26 eqid 1 Z = 1 Z
27 20 26 1unit Z Ring 1 Z Unit Z
28 25 27 syl φ 1 Z Unit Z
29 eqid L -1 1 Z = L -1 1 Z
30 eqidd φ f W 1 Z = 1 Z
31 1 2 3 4 5 6 7 20 28 29 30 rpvmasum2 φ x + ϕ N n 1 x L -1 1 Z Λ n n log x 1 W 𝑂1
32 31 adantr φ * X X x + ϕ N n 1 x L -1 1 Z Λ n n log x 1 W 𝑂1
33 3 phicld φ ϕ N
34 33 nnnn0d φ ϕ N 0
35 34 adantr φ x + ϕ N 0
36 35 nn0red φ x + ϕ N
37 fzfid φ x + 1 x Fin
38 inss1 1 x L -1 1 Z 1 x
39 ssfi 1 x Fin 1 x L -1 1 Z 1 x 1 x L -1 1 Z Fin
40 37 38 39 sylancl φ x + 1 x L -1 1 Z Fin
41 elinel1 n 1 x L -1 1 Z n 1 x
42 elfznn n 1 x n
43 42 adantl φ x + n 1 x n
44 41 43 sylan2 φ x + n 1 x L -1 1 Z n
45 vmacl n Λ n
46 nndivre Λ n n Λ n n
47 45 46 mpancom n Λ n n
48 44 47 syl φ x + n 1 x L -1 1 Z Λ n n
49 40 48 fsumrecl φ x + n 1 x L -1 1 Z Λ n n
50 36 49 remulcld φ x + ϕ N n 1 x L -1 1 Z Λ n n
51 relogcl x + log x
52 51 adantl φ x + log x
53 1re 1
54 4 5 dchrfi N D Fin
55 3 54 syl φ D Fin
56 difss D 1 ˙ D
57 10 56 sstri W D
58 ssfi D Fin W D W Fin
59 55 57 58 sylancl φ W Fin
60 hashcl W Fin W 0
61 59 60 syl φ W 0
62 61 nn0red φ W
63 resubcl 1 W 1 W
64 53 62 63 sylancr φ 1 W
65 64 adantr φ x + 1 W
66 52 65 remulcld φ x + log x 1 W
67 50 66 resubcld φ x + ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
68 67 recnd φ x + ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
69 68 adantlr φ * X X x + ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
70 51 adantl φ * X X x + log x
71 70 recnd φ * X X x + log x
72 51 ad2antrl φ * X X x + 1 x log x
73 66 ad2ant2r φ * X X x + 1 x log x 1 W
74 72 73 readdcld φ * X X x + 1 x log x + log x 1 W
75 0red φ * X X x + 1 x 0
76 50 ad2ant2r φ * X X x + 1 x ϕ N n 1 x L -1 1 Z Λ n n
77 2re 2
78 77 a1i φ * X X x + 1 x 2
79 62 ad2antrr φ * X X x + 1 x W
80 78 79 resubcld φ * X X x + 1 x 2 W
81 log1 log 1 = 0
82 simprr φ * X X x + 1 x 1 x
83 1rp 1 +
84 simprl φ * X X x + 1 x x +
85 logleb 1 + x + 1 x log 1 log x
86 83 84 85 sylancr φ * X X x + 1 x 1 x log 1 log x
87 82 86 mpbid φ * X X x + 1 x log 1 log x
88 81 87 eqbrtrrid φ * X X x + 1 x 0 log x
89 59 ad2antrr φ * X X x + 1 x W Fin
90 eqid inv g G = inv g G
91 4 5 12 90 dchrinv φ inv g G X = * X
92 4 dchrabl N G Abel
93 3 92 syl φ G Abel
94 ablgrp G Abel G Grp
95 93 94 syl φ G Grp
96 5 90 grpinvcl G Grp X D inv g G X D
97 95 12 96 syl2anc φ inv g G X D
98 91 97 eqeltrrd φ * X D
99 eldifsni X D 1 ˙ X 1 ˙
100 11 99 syl φ X 1 ˙
101 5 6 grpidcl G Grp 1 ˙ D
102 95 101 syl φ 1 ˙ D
103 5 90 95 12 102 grpinv11 φ inv g G X = inv g G 1 ˙ X = 1 ˙
104 103 necon3bid φ inv g G X inv g G 1 ˙ X 1 ˙
105 100 104 mpbird φ inv g G X inv g G 1 ˙
106 6 90 grpinvid G Grp inv g G 1 ˙ = 1 ˙
107 95 106 syl φ inv g G 1 ˙ = 1 ˙
108 105 91 107 3netr3d φ * X 1 ˙
109 eldifsn * X D 1 ˙ * X D * X 1 ˙
110 98 108 109 sylanbrc φ * X D 1 ˙
111 nnuz = 1
112 1zzd φ 1
113 2fveq3 n = m X L n = X L m
114 id n = m n = m
115 113 114 oveq12d n = m X L n n = X L m m
116 115 fveq2d n = m X L n n = X L m m
117 eqid n X L n n = n X L n n
118 fvex X L m m V
119 116 117 118 fvmpt m n X L n n m = X L m m
120 119 adantl φ m n X L n n m = X L m m
121 nnre m m
122 121 adantl φ m m
123 122 cjred φ m m = m
124 123 oveq2d φ m X L m m = X L m m
125 13 adantr φ m X : Base Z
126 1 9 2 znzrhfo N 0 L : onto Base Z
127 21 126 syl φ L : onto Base Z
128 fof L : onto Base Z L : Base Z
129 127 128 syl φ L : Base Z
130 nnz m m
131 ffvelrn L : Base Z m L m Base Z
132 129 130 131 syl2an φ m L m Base Z
133 125 132 ffvelrnd φ m X L m
134 nncn m m
135 134 adantl φ m m
136 nnne0 m m 0
137 136 adantl φ m m 0
138 133 135 137 cjdivd φ m X L m m = X L m m
139 fvco3 X : Base Z L m Base Z * X L m = X L m
140 125 132 139 syl2anc φ m * X L m = X L m
141 140 oveq1d φ m * X L m m = X L m m
142 124 138 141 3eqtr4d φ m X L m m = * X L m m
143 120 142 eqtrd φ m n X L n n m = * X L m m
144 133 cjcld φ m X L m
145 144 135 137 divcld φ m X L m m
146 141 145 eqeltrd φ m * X L m m
147 eqid a X L a a = a X L a a
148 1 2 3 4 5 6 12 100 147 dchrmusumlema φ t c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y
149 simprrl φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y seq 1 + a X L a a t
150 8 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y X W
151 3 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y N
152 12 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y X D
153 100 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y X 1 ˙
154 simprl φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y c 0 +∞
155 simprrr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y y 1 +∞ seq 1 + a X L a a y t c y
156 1 2 151 4 5 6 152 153 147 154 149 155 7 dchrvmaeq0 φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y X W t = 0
157 150 156 mpbid φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y t = 0
158 149 157 breqtrd φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y seq 1 + a X L a a 0
159 158 rexlimdvaa φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y seq 1 + a X L a a 0
160 159 exlimdv φ t c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y seq 1 + a X L a a 0
161 148 160 mpd φ seq 1 + a X L a a 0
162 seqex seq 1 + n X L n n V
163 162 a1i φ seq 1 + n X L n n V
164 2fveq3 a = m X L a = X L m
165 id a = m a = m
166 164 165 oveq12d a = m X L a a = X L m m
167 ovex X L m m V
168 166 147 167 fvmpt m a X L a a m = X L m m
169 168 adantl φ m a X L a a m = X L m m
170 133 135 137 divcld φ m X L m m
171 169 170 eqeltrd φ m a X L a a m
172 111 112 171 serf φ seq 1 + a X L a a :
173 172 ffvelrnda φ k seq 1 + a X L a a k
174 fzfid φ k 1 k Fin
175 simpl φ k φ
176 elfznn m 1 k m
177 175 176 170 syl2an φ k m 1 k X L m m
178 174 177 fsumcj φ k m = 1 k X L m m = m = 1 k X L m m
179 175 176 169 syl2an φ k m 1 k a X L a a m = X L m m
180 simpr φ k k
181 180 111 eleqtrdi φ k k 1
182 179 181 177 fsumser φ k m = 1 k X L m m = seq 1 + a X L a a k
183 182 fveq2d φ k m = 1 k X L m m = seq 1 + a X L a a k
184 175 176 120 syl2an φ k m 1 k n X L n n m = X L m m
185 170 cjcld φ m X L m m
186 175 176 185 syl2an φ k m 1 k X L m m
187 184 181 186 fsumser φ k m = 1 k X L m m = seq 1 + n X L n n k
188 178 183 187 3eqtr3rd φ k seq 1 + n X L n n k = seq 1 + a X L a a k
189 111 161 163 112 173 188 climcj φ seq 1 + n X L n n 0
190 cj0 0 = 0
191 189 190 breqtrdi φ seq 1 + n X L n n 0
192 111 112 143 146 191 isumclim φ m * X L m m = 0
193 fveq1 y = * X y L m = * X L m
194 193 oveq1d y = * X y L m m = * X L m m
195 194 sumeq2sdv y = * X m y L m m = m * X L m m
196 195 eqeq1d y = * X m y L m m = 0 m * X L m m = 0
197 196 7 elrab2 * X W * X D 1 ˙ m * X L m m = 0
198 110 192 197 sylanbrc φ * X W
199 198 ad2antrr φ * X X x + 1 x * X W
200 8 ad2antrr φ * X X x + 1 x X W
201 simplr φ * X X x + 1 x * X X
202 89 199 200 201 nehash2 φ * X X x + 1 x 2 W
203 suble0 2 W 2 W 0 2 W
204 77 79 203 sylancr φ * X X x + 1 x 2 W 0 2 W
205 202 204 mpbird φ * X X x + 1 x 2 W 0
206 80 75 72 88 205 lemul2ad φ * X X x + 1 x log x 2 W log x 0
207 df-2 2 = 1 + 1
208 207 oveq1i 2 W = 1 + 1 - W
209 1cnd φ * X X x + 1 x 1
210 79 recnd φ * X X x + 1 x W
211 209 209 210 addsubassd φ * X X x + 1 x 1 + 1 - W = 1 + 1 - W
212 208 211 syl5eq φ * X X x + 1 x 2 W = 1 + 1 - W
213 212 oveq2d φ * X X x + 1 x log x 2 W = log x 1 + 1 - W
214 71 adantrr φ * X X x + 1 x log x
215 64 ad2antrr φ * X X x + 1 x 1 W
216 215 recnd φ * X X x + 1 x 1 W
217 214 209 216 adddid φ * X X x + 1 x log x 1 + 1 - W = log x 1 + log x 1 W
218 214 mulid1d φ * X X x + 1 x log x 1 = log x
219 218 oveq1d φ * X X x + 1 x log x 1 + log x 1 W = log x + log x 1 W
220 213 217 219 3eqtrd φ * X X x + 1 x log x 2 W = log x + log x 1 W
221 214 mul01d φ * X X x + 1 x log x 0 = 0
222 206 220 221 3brtr3d φ * X X x + 1 x log x + log x 1 W 0
223 33 nnred φ ϕ N
224 223 ad2antrr φ * X X x + 1 x ϕ N
225 49 ad2ant2r φ * X X x + 1 x n 1 x L -1 1 Z Λ n n
226 34 ad2antrr φ * X X x + 1 x ϕ N 0
227 226 nn0ge0d φ * X X x + 1 x 0 ϕ N
228 44 45 syl φ x + n 1 x L -1 1 Z Λ n
229 vmage0 n 0 Λ n
230 44 229 syl φ x + n 1 x L -1 1 Z 0 Λ n
231 44 nnred φ x + n 1 x L -1 1 Z n
232 44 nngt0d φ x + n 1 x L -1 1 Z 0 < n
233 divge0 Λ n 0 Λ n n 0 < n 0 Λ n n
234 228 230 231 232 233 syl22anc φ x + n 1 x L -1 1 Z 0 Λ n n
235 40 48 234 fsumge0 φ x + 0 n 1 x L -1 1 Z Λ n n
236 235 ad2ant2r φ * X X x + 1 x 0 n 1 x L -1 1 Z Λ n n
237 224 225 227 236 mulge0d φ * X X x + 1 x 0 ϕ N n 1 x L -1 1 Z Λ n n
238 74 75 76 222 237 letrd φ * X X x + 1 x log x + log x 1 W ϕ N n 1 x L -1 1 Z Λ n n
239 leaddsub log x log x 1 W ϕ N n 1 x L -1 1 Z Λ n n log x + log x 1 W ϕ N n 1 x L -1 1 Z Λ n n log x ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
240 72 73 76 239 syl3anc φ * X X x + 1 x log x + log x 1 W ϕ N n 1 x L -1 1 Z Λ n n log x ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
241 238 240 mpbid φ * X X x + 1 x log x ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
242 72 88 absidd φ * X X x + 1 x log x = log x
243 67 ad2ant2r φ * X X x + 1 x ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
244 75 72 243 88 241 letrd φ * X X x + 1 x 0 ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
245 243 244 absidd φ * X X x + 1 x ϕ N n 1 x L -1 1 Z Λ n n log x 1 W = ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
246 241 242 245 3brtr4d φ * X X x + 1 x log x ϕ N n 1 x L -1 1 Z Λ n n log x 1 W
247 19 32 69 71 246 o1le φ * X X x + log x 𝑂1
248 247 ex φ * X X x + log x 𝑂1
249 248 necon1bd φ ¬ x + log x 𝑂1 * X = X
250 18 249 mpi φ * X = X
251 250 adantr φ x Base Z * X = X
252 251 fveq1d φ x Base Z * X x = X x
253 17 252 eqtr3d φ x Base Z X x = X x
254 15 253 cjrebd φ x Base Z X x
255 254 ralrimiva φ x Base Z X x
256 ffnfv X : Base Z X Fn Base Z x Base Z X x
257 14 255 256 sylanbrc φ X : Base Z