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	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrvmasumif.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
	dchrvmasumif.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
	dchrvmasumif.s	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
	dchrvmasumif.1	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
	dchrvmaeq0.w	⊢ 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 }
Assertion	dchrvmaeq0	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑊 ↔ 𝑆 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
7		dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrvmasumif.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
10		dchrvmasumif.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
11		dchrvmasumif.s	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
12		dchrvmasumif.1	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
13		dchrvmaeq0.w	⊢ 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 }
14		eldifsn	⊢ ( 𝑋 ∈ ( 𝐷 ∖ { 1 } ) ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑋 ≠ 1 ) )
15	7 8 14	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 1 } ) )
16		fveq1	⊢ ( 𝑦 = 𝑋 → ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) )
17	16	oveq1d	⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
18	17	sumeq2sdv	⊢ ( 𝑦 = 𝑋 → Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = Σ 𝑚 ∈ ℕ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
19	18	eqeq1d	⊢ ( 𝑦 = 𝑋 → ( Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ↔ Σ 𝑚 ∈ ℕ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ) )
20	19 13	elrab2	⊢ ( 𝑋 ∈ 𝑊 ↔ ( 𝑋 ∈ ( 𝐷 ∖ { 1 } ) ∧ Σ 𝑚 ∈ ℕ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ) )
21	20	baib	⊢ ( 𝑋 ∈ ( 𝐷 ∖ { 1 } ) → ( 𝑋 ∈ 𝑊 ↔ Σ 𝑚 ∈ ℕ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ) )
22	15 21	syl	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑊 ↔ Σ 𝑚 ∈ ℕ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ) )
23		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
24		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
25		2fveq3	⊢ ( 𝑎 = 𝑚 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) )
26		id	⊢ ( 𝑎 = 𝑚 → 𝑎 = 𝑚 )
27	25 26	oveq12d	⊢ ( 𝑎 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
28		ovex	⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ V
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	⊢ ( 𝑚 ∈ ℕ → 𝑚 ≠ 0 )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ≠ 0 )
39	34 36 38	divcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
40	23 24 30 39 11	isumclim	⊢ ( 𝜑 → Σ 𝑚 ∈ ℕ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 𝑆 )
41	40	eqeq1d	⊢ ( 𝜑 → ( Σ 𝑚 ∈ ℕ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ↔ 𝑆 = 0 ) )
42	22 41	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑊 ↔ 𝑆 = 0 ) )