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=\mathrm{DChr}\left(N\right)$$
	sumdchr.d	$$⊢D={\mathrm{Base}}_G$$
	sumdchr.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	sumdchr.1	$$⊢\underset{\dot{}}{1}=1_Z$$
	sumdchr.b	$$⊢B={\mathrm{Base}}_Z$$
	sumdchr.n	$$⊢\phi \to N\in \mathbb{N}$$
	sumdchr.a	$$⊢\phi \to A\in B$$
Assertion	sumdchr	$$⊢\phi \to \sum _{x\in D}x\left(A\right)=if\left(A=\underset{\dot{}}{1},\mathrm{\varphi }\left(N\right),0\right)$$

Proof

Step	Hyp	Ref	Expression
1		sumdchr.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		sumdchr.d	$$⊢D={\mathrm{Base}}_G$$
3		sumdchr.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
4		sumdchr.1	$$⊢\underset{\dot{}}{1}=1_Z$$
5		sumdchr.b	$$⊢B={\mathrm{Base}}_Z$$
6		sumdchr.n	$$⊢\phi \to N\in \mathbb{N}$$
7		sumdchr.a	$$⊢\phi \to A\in B$$
8	1 2 3 4 5 6 7	sumdchr2	$$⊢\phi \to \sum _{x\in D}x\left(A\right)=if\left(A=\underset{\dot{}}{1},\left|D\right|,0\right)$$
9	1 2	dchrhash	$$⊢N\in \mathbb{N}\to \left|D\right|=\mathrm{\varphi }\left(N\right)$$
10	6 9	syl	$$⊢\phi \to \left|D\right|=\mathrm{\varphi }\left(N\right)$$
11	10	ifeq1d	$$⊢\phi \to if\left(A=\underset{\dot{}}{1},\left|D\right|,0\right)=if\left(A=\underset{\dot{}}{1},\mathrm{\varphi }\left(N\right),0\right)$$
12	8 11	eqtrd	$$⊢\phi \to \sum _{x\in D}x\left(A\right)=if\left(A=\underset{\dot{}}{1},\mathrm{\varphi }\left(N\right),0\right)$$