Metamath Proof Explorer


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 = /N
rpvmasum.l L = ℤRHom Z
rpvmasum.a φ N
rpvmasum2.g G = DChr N
rpvmasum2.d D = Base G
rpvmasum2.1 1 ˙ = 0 G
dchrisum0f.f F = b v q | q b X L v
dchrisum0f.x φ X D
dchrisum0fmul.a φ A
dchrisum0fmul.b φ B
dchrisum0fmul.m φ A gcd B = 1
Assertion dchrisum0fmul φ F A B = F A F B

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z = /N
2 rpvmasum.l L = ℤRHom Z
3 rpvmasum.a φ N
4 rpvmasum2.g G = DChr N
5 rpvmasum2.d D = Base G
6 rpvmasum2.1 1 ˙ = 0 G
7 dchrisum0f.f F = b v q | q b X L v
8 dchrisum0f.x φ X D
9 dchrisum0fmul.a φ A
10 dchrisum0fmul.b φ B
11 dchrisum0fmul.m φ A gcd B = 1
12 eqid q | q A = q | q A
13 eqid q | q B = q | q B
14 eqid q | q A B = q | q A B
15 8 adantr φ j q | q A X D
16 elrabi j q | q A j
17 16 nnzd j q | q A j
18 17 adantl φ j q | q A j
19 4 1 5 2 15 18 dchrzrhcl φ j q | q A X L j
20 8 adantr φ k q | q B X D
21 elrabi k q | q B k
22 21 nnzd k q | q B k
23 22 adantl φ k q | q B k
24 4 1 5 2 20 23 dchrzrhcl φ k q | q B X L k
25 17 22 anim12i j q | q A k q | q B j k
26 8 adantr φ j k X D
27 simprl φ j k j
28 simprr φ j k k
29 4 1 5 2 26 27 28 dchrzrhmul φ j k X L j k = X L j X L k
30 29 eqcomd φ j k X L j X L k = X L j k
31 25 30 sylan2 φ j q | q A k q | q B X L j X L k = X L j k
32 2fveq3 i = j k X L i = X L j k
33 9 10 11 12 13 14 19 24 31 32 fsumdvdsmul φ j q | q A X L j k q | q B X L k = i q | q A B X L i
34 1 2 3 4 5 6 7 dchrisum0fval A F A = j q | q A X L j
35 9 34 syl φ F A = j q | q A X L j
36 1 2 3 4 5 6 7 dchrisum0fval B F B = k q | q B X L k
37 10 36 syl φ F B = k q | q B X L k
38 35 37 oveq12d φ F A F B = j q | q A X L j k q | q B X L k
39 9 10 nnmulcld φ A B
40 1 2 3 4 5 6 7 dchrisum0fval A B F A B = i q | q A B X L i
41 39 40 syl φ F A B = i q | q A B X L i
42 33 38 41 3eqtr4rd φ F A B = F A F B