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

Metamath Proof Explorer

Theorem sumdchr

Description: An orthogonality relation for Dirichlet characters: the sum of x ( A ) for fixed A and all x is 0 if A = 1 and phi ( n ) otherwise. Theorem 6.5.1 of Shapiro p. 230. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses sumdchr.g ⊢ G = DChr ⁡ N
sumdchr.d ⊢ D = Base G
sumdchr.z ⊢ Z = ℤ/Nℤ
sumdchr.1 ⊢ 1 ˙ = 1 Z
sumdchr.b ⊢ B = Base Z
sumdchr.n ⊢ φ → N ∈ ℕ
sumdchr.a ⊢ φ → A ∈ B
Assertion sumdchr ⊢ φ → ∑ x ∈ D x ⁡ A = if A = 1 ˙ ϕ ⁡ N 0

Proof

Step Hyp Ref Expression
1 sumdchr.g ⊢ G = DChr ⁡ N
2 sumdchr.d ⊢ D = Base G
3 sumdchr.z ⊢ Z = ℤ/Nℤ
4 sumdchr.1 ⊢ 1 ˙ = 1 Z
5 sumdchr.b ⊢ B = Base Z
6 sumdchr.n ⊢ φ → N ∈ ℕ
7 sumdchr.a ⊢ φ → A ∈ B
8 1 2 3 4 5 6 7 sumdchr2 ⊢ φ → ∑ x ∈ D x ⁡ A = if A = 1 ˙ D 0
9 1 2 dchrhash ⊢ N ∈ ℕ → D = ϕ ⁡ N
10 6 9 syl ⊢ φ → D = ϕ ⁡ N
11 10 ifeq1d ⊢ φ → if A = 1 ˙ D 0 = if A = 1 ˙ ϕ ⁡ N 0
12 8 11 eqtrd ⊢ φ → ∑ x ∈ D x ⁡ A = if A = 1 ˙ ϕ ⁡ N 0