This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ℤ/Nℤ
rpvmasum.l ⊢ L = ℤRHom ⁡ Z
rpvmasum.a ⊢ φ → N ∈ ℕ
dchrmusum.g ⊢ G = DChr ⁡ N
dchrmusum.d ⊢ D = Base G
dchrmusum.1 ⊢ 1 ˙ = 0 G
dchrmusum.b ⊢ φ → X ∈ D
dchrmusum.n1 ⊢ φ → X ≠ 1 ˙
dchrmusum.f ⊢ F = a ∈ ℕ ⟼ X ⁡ L ⁡ a a
dchrmusum.c ⊢ φ → C ∈ 0 +∞
dchrmusum.t ⊢ φ → seq 1 + F ⇝ T
dchrmusum.2 ⊢ φ → ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − T ≤ C y
Assertion dchrisumn0 ⊢ φ → T ≠ 0

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ Z = ℤ/Nℤ
2 rpvmasum.l ⊢ L = ℤRHom ⁡ Z
3 rpvmasum.a ⊢ φ → N ∈ ℕ
4 dchrmusum.g ⊢ G = DChr ⁡ N
5 dchrmusum.d ⊢ D = Base G
6 dchrmusum.1 ⊢ 1 ˙ = 0 G
7 dchrmusum.b ⊢ φ → X ∈ D
8 dchrmusum.n1 ⊢ φ → X ≠ 1 ˙
9 dchrmusum.f ⊢ F = a ∈ ℕ ⟼ X ⁡ L ⁡ a a
10 dchrmusum.c ⊢ φ → C ∈ 0 +∞
11 dchrmusum.t ⊢ φ → seq 1 + F ⇝ T
12 dchrmusum.2 ⊢ φ → ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − T ≤ C y
13 3 adantr ⊢ φ ∧ T = 0 → N ∈ ℕ
14 eqid ⊢ y ∈ D ∖ 1 ˙ | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = y ∈ D ∖ 1 ˙ | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0
15 1 2 3 4 5 6 7 8 9 10 11 12 14 dchrvmaeq0 ⊢ φ → X ∈ y ∈ D ∖ 1 ˙ | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 ↔ T = 0
16 15 biimpar ⊢ φ ∧ T = 0 → X ∈ y ∈ D ∖ 1 ˙ | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0
17 1 2 13 4 5 6 14 16 dchrisum0 ⊢ ¬ φ ∧ T = 0
18 17 imnani ⊢ φ → ¬ T = 0
19 18 neqned ⊢ φ → T ≠ 0