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 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=\mathbb{Z}/N\mathbb{Z}$$
	rpvmasum.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
	rpvmasum.a	$$⊢\phi \to N\in \mathbb{N}$$
	dchrmusum.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrmusum.d	$$⊢D={\mathrm{Base}}_G$$
	dchrmusum.1	$$⊢\underset{\dot{}}{1}=0_G$$
	dchrmusum.b	$$⊢\phi \to X\in D$$
	dchrmusum.n1	$$⊢\phi \to X\ne \underset{\dot{}}{1}$$
	dchrmusum.f	$$⊢F=\left(a\in \mathbb{N}⟼\frac{X\left(L\left(a\right)\right)}{a}\right)$$
	dchrmusum.c	$$⊢\phi \to C\in \left[0,\mathrm{+\infty }\right)$$
	dchrmusum.t	$$⊢\phi \to seq1\left(+,F\right)⇝T$$
	dchrmusum.2	$$⊢\phi \to \forall y\in \left[1,\mathrm{+\infty }\right)\left|seq1\left(+,F\right)\left(⌊y⌋\right)-T\right|\le \frac{C}{y}$$
Assertion	dchrisumn0	$$⊢\phi \to T\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
2		rpvmasum.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
3		rpvmasum.a	$$⊢\phi \to N\in \mathbb{N}$$
4		dchrmusum.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
5		dchrmusum.d	$$⊢D={\mathrm{Base}}_G$$
6		dchrmusum.1	$$⊢\underset{\dot{}}{1}=0_G$$
7		dchrmusum.b	$$⊢\phi \to X\in D$$
8		dchrmusum.n1	$$⊢\phi \to X\ne \underset{\dot{}}{1}$$
9		dchrmusum.f	$$⊢F=\left(a\in \mathbb{N}⟼\frac{X\left(L\left(a\right)\right)}{a}\right)$$
10		dchrmusum.c	$$⊢\phi \to C\in \left[0,\mathrm{+\infty }\right)$$
11		dchrmusum.t	$$⊢\phi \to seq1\left(+,F\right)⇝T$$
12		dchrmusum.2	$$⊢\phi \to \forall y\in \left[1,\mathrm{+\infty }\right)\left|seq1\left(+,F\right)\left(⌊y⌋\right)-T\right|\le \frac{C}{y}$$
13	3	adantr	$$⊢\left(\phi \wedge T=0\right)\to N\in \mathbb{N}$$
14		eqid	$$⊢\left\{y\in \left(D\setminus \left\{\underset{\dot{}}{1}\right\}\right)|\sum _{m\in \mathbb{N}}\left(\frac{y\left(L\left(m\right)\right)}{m}\right)=0\right\}=\left\{y\in \left(D\setminus \left\{\underset{\dot{}}{1}\right\}\right)|\sum _{m\in \mathbb{N}}\left(\frac{y\left(L\left(m\right)\right)}{m}\right)=0\right\}$$
15	1 2 3 4 5 6 7 8 9 10 11 12 14	dchrvmaeq0	$$⊢\phi \to \left(X\in \left\{y\in \left(D\setminus \left\{\underset{\dot{}}{1}\right\}\right)|\sum _{m\in \mathbb{N}}\left(\frac{y\left(L\left(m\right)\right)}{m}\right)=0\right\}\leftrightarrow T=0\right)$$
16	15	biimpar	$$⊢\left(\phi \wedge T=0\right)\to X\in \left\{y\in \left(D\setminus \left\{\underset{\dot{}}{1}\right\}\right)|\sum _{m\in \mathbb{N}}\left(\frac{y\left(L\left(m\right)\right)}{m}\right)=0\right\}$$
17	1 2 13 4 5 6 14 16	dchrisum0	$$⊢\neg \left(\phi \wedge T=0\right)$$
18	17	imnani	$$⊢\phi \to \neg T=0$$
19	18	neqned	$$⊢\phi \to T\ne 0$$