Theorem dchrisum0fmul

Description: The function F , the divisor sum of a Dirichlet character, is a multiplicative function (but not completely multiplicative). Equation 9.4.27 of Shapiro, p. 382. (Contributed by Mario Carneiro, 5-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	rpvmasum.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
	rpvmasum.a	$$⊢\phi \to N\in \mathbb{N}$$
	rpvmasum2.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	rpvmasum2.d	$$⊢D={\mathrm{Base}}_G$$
	rpvmasum2.1	$$⊢\underset{\dot{}}{1}=0_G$$
	dchrisum0f.f	$$⊢F=\left(b\in \mathbb{N}⟼\sum _{v\in \left\{q\in \mathbb{N}|q\parallel b\right\}}X\left(L\left(v\right)\right)\right)$$
	dchrisum0f.x	$$⊢\phi \to X\in D$$
	dchrisum0fmul.a	$$⊢\phi \to A\in \mathbb{N}$$
	dchrisum0fmul.b	$$⊢\phi \to B\in \mathbb{N}$$
	dchrisum0fmul.m	$$⊢\phi \to A\gcd B=1$$
Assertion	dchrisum0fmul	$$⊢\phi \to F\left(AB\right)=F\left(A\right)F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
2		rpvmasum.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
3		rpvmasum.a	$$⊢\phi \to N\in \mathbb{N}$$
4		rpvmasum2.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
5		rpvmasum2.d	$$⊢D={\mathrm{Base}}_G$$
6		rpvmasum2.1	$$⊢\underset{\dot{}}{1}=0_G$$
7		dchrisum0f.f	$$⊢F=\left(b\in \mathbb{N}⟼\sum _{v\in \left\{q\in \mathbb{N}|q\parallel b\right\}}X\left(L\left(v\right)\right)\right)$$
8		dchrisum0f.x	$$⊢\phi \to X\in D$$
9		dchrisum0fmul.a	$$⊢\phi \to A\in \mathbb{N}$$
10		dchrisum0fmul.b	$$⊢\phi \to B\in \mathbb{N}$$
11		dchrisum0fmul.m	$$⊢\phi \to A\gcd B=1$$
12		eqid	$$⊢\left\{q\in \mathbb{N}|q\parallel A\right\}=\left\{q\in \mathbb{N}|q\parallel A\right\}$$
13		eqid	$$⊢\left\{q\in \mathbb{N}|q\parallel B\right\}=\left\{q\in \mathbb{N}|q\parallel B\right\}$$
14		eqid	$$⊢\left\{q\in \mathbb{N}|q\parallel AB\right\}=\left\{q\in \mathbb{N}|q\parallel AB\right\}$$
15	8	adantr	$$⊢\left(\phi \wedge j\in \left\{q\in \mathbb{N}|q\parallel A\right\}\right)\to X\in D$$
16		elrabi	$$⊢j\in \left\{q\in \mathbb{N}|q\parallel A\right\}\to j\in \mathbb{N}$$
17	16	nnzd	$$⊢j\in \left\{q\in \mathbb{N}|q\parallel A\right\}\to j\in \mathbb{Z}$$
18	17	adantl	$$⊢\left(\phi \wedge j\in \left\{q\in \mathbb{N}|q\parallel A\right\}\right)\to j\in \mathbb{Z}$$
19	4 1 5 2 15 18	dchrzrhcl	$$⊢\left(\phi \wedge j\in \left\{q\in \mathbb{N}|q\parallel A\right\}\right)\to X\left(L\left(j\right)\right)\in ℂ$$
20	8	adantr	$$⊢\left(\phi \wedge k\in \left\{q\in \mathbb{N}|q\parallel B\right\}\right)\to X\in D$$
21		elrabi	$$⊢k\in \left\{q\in \mathbb{N}|q\parallel B\right\}\to k\in \mathbb{N}$$
22	21	nnzd	$$⊢k\in \left\{q\in \mathbb{N}|q\parallel B\right\}\to k\in \mathbb{Z}$$
23	22	adantl	$$⊢\left(\phi \wedge k\in \left\{q\in \mathbb{N}|q\parallel B\right\}\right)\to k\in \mathbb{Z}$$
24	4 1 5 2 20 23	dchrzrhcl	$$⊢\left(\phi \wedge k\in \left\{q\in \mathbb{N}|q\parallel B\right\}\right)\to X\left(L\left(k\right)\right)\in ℂ$$
25	17 22	anim12i	$$⊢\left(j\in \left\{q\in \mathbb{N}|q\parallel A\right\}\wedge k\in \left\{q\in \mathbb{N}|q\parallel B\right\}\right)\to \left(j\in \mathbb{Z}\wedge k\in \mathbb{Z}\right)$$
26	8	adantr	$$⊢\left(\phi \wedge \left(j\in \mathbb{Z}\wedge k\in \mathbb{Z}\right)\right)\to X\in D$$
27		simprl	$$⊢\left(\phi \wedge \left(j\in \mathbb{Z}\wedge k\in \mathbb{Z}\right)\right)\to j\in \mathbb{Z}$$
28		simprr	$$⊢\left(\phi \wedge \left(j\in \mathbb{Z}\wedge k\in \mathbb{Z}\right)\right)\to k\in \mathbb{Z}$$
29	4 1 5 2 26 27 28	dchrzrhmul	$$⊢\left(\phi \wedge \left(j\in \mathbb{Z}\wedge k\in \mathbb{Z}\right)\right)\to X\left(L\left(jk\right)\right)=X\left(L\left(j\right)\right)X\left(L\left(k\right)\right)$$
30	29	eqcomd	$$⊢\left(\phi \wedge \left(j\in \mathbb{Z}\wedge k\in \mathbb{Z}\right)\right)\to X\left(L\left(j\right)\right)X\left(L\left(k\right)\right)=X\left(L\left(jk\right)\right)$$
31	25 30	sylan2	$$⊢\left(\phi \wedge \left(j\in \left\{q\in \mathbb{N}|q\parallel A\right\}\wedge k\in \left\{q\in \mathbb{N}|q\parallel B\right\}\right)\right)\to X\left(L\left(j\right)\right)X\left(L\left(k\right)\right)=X\left(L\left(jk\right)\right)$$
32		2fveq3	$$⊢i=jk\to X\left(L\left(i\right)\right)=X\left(L\left(jk\right)\right)$$
33	9 10 11 12 13 14 19 24 31 32	fsumdvdsmul	$$⊢\phi \to \sum _{j\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(j\right)\right)\sum _{k\in \left\{q\in \mathbb{N}|q\parallel B\right\}}X\left(L\left(k\right)\right)=\sum _{i\in \left\{q\in \mathbb{N}|q\parallel AB\right\}}X\left(L\left(i\right)\right)$$
34	1 2 3 4 5 6 7	dchrisum0fval	$$⊢A\in \mathbb{N}\to F\left(A\right)=\sum _{j\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(j\right)\right)$$
35	9 34	syl	$$⊢\phi \to F\left(A\right)=\sum _{j\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(j\right)\right)$$
36	1 2 3 4 5 6 7	dchrisum0fval	$$⊢B\in \mathbb{N}\to F\left(B\right)=\sum _{k\in \left\{q\in \mathbb{N}|q\parallel B\right\}}X\left(L\left(k\right)\right)$$
37	10 36	syl	$$⊢\phi \to F\left(B\right)=\sum _{k\in \left\{q\in \mathbb{N}|q\parallel B\right\}}X\left(L\left(k\right)\right)$$
38	35 37	oveq12d	$$⊢\phi \to F\left(A\right)F\left(B\right)=\sum _{j\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(j\right)\right)\sum _{k\in \left\{q\in \mathbb{N}|q\parallel B\right\}}X\left(L\left(k\right)\right)$$
39	9 10	nnmulcld	$$⊢\phi \to AB\in \mathbb{N}$$
40	1 2 3 4 5 6 7	dchrisum0fval	$$⊢AB\in \mathbb{N}\to F\left(AB\right)=\sum _{i\in \left\{q\in \mathbb{N}|q\parallel AB\right\}}X\left(L\left(i\right)\right)$$
41	39 40	syl	$$⊢\phi \to F\left(AB\right)=\sum _{i\in \left\{q\in \mathbb{N}|q\parallel AB\right\}}X\left(L\left(i\right)\right)$$
42	33 38 41	3eqtr4rd	$$⊢\phi \to F\left(AB\right)=F\left(A\right)F\left(B\right)$$