Metamath Proof Explorer


Theorem dchrvmaeq0

Description: The set W is the collection of all non-principal Dirichlet characters such that the sum sum_ n e. NN , X ( n ) / n is equal to zero. (Contributed by Mario Carneiro, 5-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˙
dchrvmasumif.f F=aXLaa
dchrvmasumif.c φC0+∞
dchrvmasumif.s φseq1+FS
dchrvmasumif.1 φy1+∞seq1+FySCy
dchrvmaeq0.w W=yD1˙|myLmm=0
Assertion dchrvmaeq0 φXWS=0

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 dchrvmasumif.f F=aXLaa
10 dchrvmasumif.c φC0+∞
11 dchrvmasumif.s φseq1+FS
12 dchrvmasumif.1 φy1+∞seq1+FySCy
13 dchrvmaeq0.w W=yD1˙|myLmm=0
14 eldifsn XD1˙XDX1˙
15 7 8 14 sylanbrc φXD1˙
16 fveq1 y=XyLm=XLm
17 16 oveq1d y=XyLmm=XLmm
18 17 sumeq2sdv y=XmyLmm=mXLmm
19 18 eqeq1d y=XmyLmm=0mXLmm=0
20 19 13 elrab2 XWXD1˙mXLmm=0
21 20 baib XD1˙XWmXLmm=0
22 15 21 syl φXWmXLmm=0
23 nnuz =1
24 1zzd φ1
25 2fveq3 a=mXLa=XLm
26 id a=ma=m
27 25 26 oveq12d a=mXLaa=XLmm
28 ovex XLmmV
29 27 9 28 fvmpt mFm=XLmm
30 29 adantl φmFm=XLmm
31 7 adantr φmXD
32 nnz mm
33 32 adantl φmm
34 4 1 5 2 31 33 dchrzrhcl φmXLm
35 nncn mm
36 35 adantl φmm
37 nnne0 mm0
38 37 adantl φmm0
39 34 36 38 divcld φmXLmm
40 23 24 30 39 11 isumclim φmXLmm=S
41 40 eqeq1d φmXLmm=0S=0
42 22 41 bitrd φXWS=0