Theorem dchrisumn0

Description: The sum sum_ n e. NN , X ( n ) / n is nonzero for all non-principal Dirichlet characters (i.e. the assumption X e. W is contradictory). This is the key result that allows us to eliminate the conditionals from dchrmusum2 and dchrvmasumif . Lemma 9.4.4 of Shapiro, p. 382. (Contributed by Mario Carneiro, 12-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	|- Z = ( Z/nZ ` N )
	rpvmasum.l	|- L = ( ZRHom ` Z )
	rpvmasum.a	|- ( ph -> N e. NN )
	dchrmusum.g	|- G = ( DChr ` N )
	dchrmusum.d	|- D = ( Base ` G )
	dchrmusum.1	|- .1. = ( 0g ` G )
	dchrmusum.b	|- ( ph -> X e. D )
	dchrmusum.n1	|- ( ph -> X =/= .1. )
	dchrmusum.f	|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
	dchrmusum.c	|- ( ph -> C e. ( 0 [,) +oo ) )
	dchrmusum.t	|- ( ph -> seq 1 ( + , F ) ~~> T )
	dchrmusum.2	|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )
Assertion	dchrisumn0	|- ( ph -> T =/= 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		dchrmusum.g	|- G = ( DChr ` N )
5		dchrmusum.d	|- D = ( Base ` G )
6		dchrmusum.1	|- .1. = ( 0g ` G )
7		dchrmusum.b	|- ( ph -> X e. D )
8		dchrmusum.n1	|- ( ph -> X =/= .1. )
9		dchrmusum.f	|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
10		dchrmusum.c	|- ( ph -> C e. ( 0 [,) +oo ) )
11		dchrmusum.t	|- ( ph -> seq 1 ( + , F ) ~~> T )
12		dchrmusum.2	|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )
13	3	adantr	|- ( ( ph /\ T = 0 ) -> N e. NN )
14		eqid	|- { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
15	1 2 3 4 5 6 7 8 9 10 11 12 14	dchrvmaeq0	|- ( ph -> ( X e. { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } <-> T = 0 ) )
16	15	biimpar	|- ( ( ph /\ T = 0 ) -> X e. { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } )
17	1 2 13 4 5 6 14 16	dchrisum0	|- -. ( ph /\ T = 0 )
18	17	imnani	|- ( ph -> -. T = 0 )
19	18	neqned	|- ( ph -> T =/= 0 )