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 = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum.g	$⊢ G = DChr (N)$
	rpvmasum.d	$⊢ D = {Base}_{G}$
	rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrisum.b	$⊢ φ \to X \in D$
	dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
	dchrvmasumif.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
	dchrvmasumif.c	$⊢ φ \to C \in [0, +∞)$
	dchrvmasumif.s	$⊢ φ \to seq 1 (+ F) ⇝ S$
	dchrvmasumif.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{y}$
	dchrvmaeq0.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
Assertion	dchrvmaeq0	$⊢ φ \to (X \in W \leftrightarrow S = 0)$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum.g	$⊢ G = DChr (N)$
5		rpvmasum.d	$⊢ D = {Base}_{G}$
6		rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrisum.b	$⊢ φ \to X \in D$
8		dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
9		dchrvmasumif.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
10		dchrvmasumif.c	$⊢ φ \to C \in [0, +∞)$
11		dchrvmasumif.s	$⊢ φ \to seq 1 (+ F) ⇝ S$
12		dchrvmasumif.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{y}$
13		dchrvmaeq0.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
14		eldifsn	$⊢ X \in (D ∖ \{\underset{˙}{1}\}) \leftrightarrow (X \in D \land X \neq \underset{˙}{1})$
15	7 8 14	sylanbrc	$⊢ φ \to X \in (D ∖ \{\underset{˙}{1}\})$
16		fveq1	$⊢ y = X \to y (L (m)) = X (L (m))$
17	16	oveq1d	$⊢ y = X \to \frac{y (L (m))}{m} = \frac{X (L (m))}{m}$
18	17	sumeq2sdv	$⊢ y = X \to \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = \sum_{m \in ℕ} (\frac{X (L (m))}{m})$
19	18	eqeq1d	$⊢ y = X \to (\sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0 \leftrightarrow \sum_{m \in ℕ} (\frac{X (L (m))}{m}) = 0)$
20	19 13	elrab2	$⊢ X \in W \leftrightarrow (X \in (D ∖ \{\underset{˙}{1}\}) \land \sum_{m \in ℕ} (\frac{X (L (m))}{m}) = 0)$
21	20	baib	$⊢ X \in (D ∖ \{\underset{˙}{1}\}) \to (X \in W \leftrightarrow \sum_{m \in ℕ} (\frac{X (L (m))}{m}) = 0)$
22	15 21	syl	$⊢ φ \to (X \in W \leftrightarrow \sum_{m \in ℕ} (\frac{X (L (m))}{m}) = 0)$
23		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
24		1zzd	$⊢ φ \to 1 \in ℤ$
25		2fveq3	$⊢ a = m \to X (L (a)) = X (L (m))$
26		id	$⊢ a = m \to a = m$
27	25 26	oveq12d	$⊢ a = m \to \frac{X (L (a))}{a} = \frac{X (L (m))}{m}$
28		ovex	$⊢ \frac{X (L (m))}{m} \in V$
29	27 9 28	fvmpt	$⊢ m \in ℕ \to F (m) = \frac{X (L (m))}{m}$
30	29	adantl	$⊢ (φ \land m \in ℕ) \to F (m) = \frac{X (L (m))}{m}$
31	7	adantr	$⊢ (φ \land m \in ℕ) \to X \in D$
32		nnz	$⊢ m \in ℕ \to m \in ℤ$
33	32	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℤ$
34	4 1 5 2 31 33	dchrzrhcl	$⊢ (φ \land m \in ℕ) \to X (L (m)) \in ℂ$
35		nncn	$⊢ m \in ℕ \to m \in ℂ$
36	35	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℂ$
37		nnne0	$⊢ m \in ℕ \to m \neq 0$
38	37	adantl	$⊢ (φ \land m \in ℕ) \to m \neq 0$
39	34 36 38	divcld	$⊢ (φ \land m \in ℕ) \to \frac{X (L (m))}{m} \in ℂ$
40	23 24 30 39 11	isumclim	$⊢ φ \to \sum_{m \in ℕ} (\frac{X (L (m))}{m}) = S$
41	40	eqeq1d	$⊢ φ \to (\sum_{m \in ℕ} (\frac{X (L (m))}{m}) = 0 \leftrightarrow S = 0)$
42	22 41	bitrd	$⊢ φ \to (X \in W \leftrightarrow S = 0)$

Metamath Proof Explorer

Theorem dchrvmaeq0

Proof