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 | |
|
rpvmasum.l | |
||
rpvmasum.a | |
||
rpvmasum.g | |
||
rpvmasum.d | |
||
rpvmasum.1 | |
||
dchrisum.b | |
||
dchrisum.n1 | |
||
dchrvmasumif.f | |
||
dchrvmasumif.c | |
||
dchrvmasumif.s | |
||
dchrvmasumif.1 | |
||
dchrvmaeq0.w | |
||
Assertion | dchrvmaeq0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpvmasum.z | |
|
2 | rpvmasum.l | |
|
3 | rpvmasum.a | |
|
4 | rpvmasum.g | |
|
5 | rpvmasum.d | |
|
6 | rpvmasum.1 | |
|
7 | dchrisum.b | |
|
8 | dchrisum.n1 | |
|
9 | dchrvmasumif.f | |
|
10 | dchrvmasumif.c | |
|
11 | dchrvmasumif.s | |
|
12 | dchrvmasumif.1 | |
|
13 | dchrvmaeq0.w | |
|
14 | eldifsn | |
|
15 | 7 8 14 | sylanbrc | |
16 | fveq1 | |
|
17 | 16 | oveq1d | |
18 | 17 | sumeq2sdv | |
19 | 18 | eqeq1d | |
20 | 19 13 | elrab2 | |
21 | 20 | baib | |
22 | 15 21 | syl | |
23 | nnuz | |
|
24 | 1zzd | |
|
25 | 2fveq3 | |
|
26 | id | |
|
27 | 25 26 | oveq12d | |
28 | ovex | |
|
29 | 27 9 28 | fvmpt | |
30 | 29 | adantl | |
31 | 7 | adantr | |
32 | nnz | |
|
33 | 32 | adantl | |
34 | 4 1 5 2 31 33 | dchrzrhcl | |
35 | nncn | |
|
36 | 35 | adantl | |
37 | nnne0 | |
|
38 | 37 | adantl | |
39 | 34 36 38 | divcld | |
40 | 23 24 30 39 11 | isumclim | |
41 | 40 | eqeq1d | |
42 | 22 41 | bitrd | |