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	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dchrmusum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrmusum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrmusum.1	⊢ 1 = ( 0_g ‘ 𝐺 )
	dchrmusum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrmusum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrmusum.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
	dchrmusum.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
	dchrmusum.t	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑇 )
	dchrmusum.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) )
Assertion	dchrisumn0	⊢ ( 𝜑 → 𝑇 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		dchrmusum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		dchrmusum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		dchrmusum.1	⊢ 1 = ( 0_g ‘ 𝐺 )
7		dchrmusum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrmusum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrmusum.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
10		dchrmusum.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
11		dchrmusum.t	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑇 )
12		dchrmusum.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) )
13	3	adantr	⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → 𝑁 ∈ ℕ )
14		eqid	⊢ { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 }
15	1 2 3 4 5 6 7 8 9 10 11 12 14	dchrvmaeq0	⊢ ( 𝜑 → ( 𝑋 ∈ { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ↔ 𝑇 = 0 ) )
16	15	biimpar	⊢ ( ( 𝜑 ∧ 𝑇 = 0 ) → 𝑋 ∈ { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } )
17	1 2 13 4 5 6 14 16	dchrisum0	⊢ ¬ ( 𝜑 ∧ 𝑇 = 0 )
18	17	imnani	⊢ ( 𝜑 → ¬ 𝑇 = 0 )
19	18	neqned	⊢ ( 𝜑 → 𝑇 ≠ 0 )

Metamath Proof Explorer

Theorem dchrisumn0

Proof