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 = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum.g 
|- G = ( DChr ` N )
rpvmasum.d 
|- D = ( Base ` G )
rpvmasum.1 
|- .1. = ( 0g ` G )
dchrisum.b 
|- ( ph -> X e. D )
dchrisum.n1 
|- ( ph -> X =/= .1. )
dchrvmasumif.f 
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
dchrvmasumif.c 
|- ( ph -> C e. ( 0 [,) +oo ) )
dchrvmasumif.s 
|- ( ph -> seq 1 ( + , F ) ~~> S )
dchrvmasumif.1 
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )
dchrvmaeq0.w 
|- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
Assertion dchrvmaeq0 
|- ( ph -> ( X e. W <-> S = 0 ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum.g 
 |-  G = ( DChr ` N )
5 rpvmasum.d 
 |-  D = ( Base ` G )
6 rpvmasum.1 
 |-  .1. = ( 0g ` G )
7 dchrisum.b 
 |-  ( ph -> X e. D )
8 dchrisum.n1 
 |-  ( ph -> X =/= .1. )
9 dchrvmasumif.f 
 |-  F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
10 dchrvmasumif.c 
 |-  ( ph -> C e. ( 0 [,) +oo ) )
11 dchrvmasumif.s 
 |-  ( ph -> seq 1 ( + , F ) ~~> S )
12 dchrvmasumif.1 
 |-  ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )
13 dchrvmaeq0.w 
 |-  W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
14 eldifsn 
 |-  ( X e. ( D \ { .1. } ) <-> ( X e. D /\ X =/= .1. ) )
15 7 8 14 sylanbrc 
 |-  ( ph -> X e. ( D \ { .1. } ) )
16 fveq1 
 |-  ( y = X -> ( y ` ( L ` m ) ) = ( X ` ( L ` m ) ) )
17 16 oveq1d 
 |-  ( y = X -> ( ( y ` ( L ` m ) ) / m ) = ( ( X ` ( L ` m ) ) / m ) )
18 17 sumeq2sdv 
 |-  ( y = X -> sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = sum_ m e. NN ( ( X ` ( L ` m ) ) / m ) )
19 18 eqeq1d 
 |-  ( y = X -> ( sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 <-> sum_ m e. NN ( ( X ` ( L ` m ) ) / m ) = 0 ) )
20 19 13 elrab2 
 |-  ( X e. W <-> ( X e. ( D \ { .1. } ) /\ sum_ m e. NN ( ( X ` ( L ` m ) ) / m ) = 0 ) )
21 20 baib 
 |-  ( X e. ( D \ { .1. } ) -> ( X e. W <-> sum_ m e. NN ( ( X ` ( L ` m ) ) / m ) = 0 ) )
22 15 21 syl 
 |-  ( ph -> ( X e. W <-> sum_ m e. NN ( ( X ` ( L ` m ) ) / m ) = 0 ) )
23 nnuz 
 |-  NN = ( ZZ>= ` 1 )
24 1zzd 
 |-  ( ph -> 1 e. ZZ )
25 2fveq3 
 |-  ( a = m -> ( X ` ( L ` a ) ) = ( X ` ( L ` m ) ) )
26 id 
 |-  ( a = m -> a = m )
27 25 26 oveq12d 
 |-  ( a = m -> ( ( X ` ( L ` a ) ) / a ) = ( ( X ` ( L ` m ) ) / m ) )
28 ovex 
 |-  ( ( X ` ( L ` m ) ) / m ) e. _V
29 27 9 28 fvmpt 
 |-  ( m e. NN -> ( F ` m ) = ( ( X ` ( L ` m ) ) / m ) )
30 29 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) = ( ( X ` ( L ` m ) ) / m ) )
31 7 adantr 
 |-  ( ( ph /\ m e. NN ) -> X e. D )
32 nnz 
 |-  ( m e. NN -> m e. ZZ )
33 32 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. ZZ )
34 4 1 5 2 31 33 dchrzrhcl 
 |-  ( ( ph /\ m e. NN ) -> ( X ` ( L ` m ) ) e. CC )
35 nncn 
 |-  ( m e. NN -> m e. CC )
36 35 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. CC )
37 nnne0 
 |-  ( m e. NN -> m =/= 0 )
38 37 adantl 
 |-  ( ( ph /\ m e. NN ) -> m =/= 0 )
39 34 36 38 divcld 
 |-  ( ( ph /\ m e. NN ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
40 23 24 30 39 11 isumclim 
 |-  ( ph -> sum_ m e. NN ( ( X ` ( L ` m ) ) / m ) = S )
41 40 eqeq1d 
 |-  ( ph -> ( sum_ m e. NN ( ( X ` ( L ` m ) ) / m ) = 0 <-> S = 0 ) )
42 22 41 bitrd 
 |-  ( ph -> ( X e. W <-> S = 0 ) )