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	$⊢ φ \to N \in ℕ$
	rpvmasum2.g	$⊢ G = DChr (N)$
	rpvmasum2.d	$⊢ D = {Base}_{G}$
	rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrisum0f.f	$⊢ F = (b \in ℕ ⟼ \sum_{v \in \{q \in ℕ \| q ∥ b\}} X (L (v)))$
	dchrisum0f.x	$⊢ φ \to X \in D$
	dchrisum0fmul.a	$⊢ φ \to A \in ℕ$
	dchrisum0fmul.b	$⊢ φ \to B \in ℕ$
	dchrisum0fmul.m	$⊢ φ \to A \gcd B = 1$
Assertion	dchrisum0fmul	$⊢ φ \to 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	$⊢ φ \to N \in ℕ$
4		rpvmasum2.g	$⊢ G = DChr (N)$
5		rpvmasum2.d	$⊢ D = {Base}_{G}$
6		rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrisum0f.f	$⊢ F = (b \in ℕ ⟼ \sum_{v \in \{q \in ℕ \| q ∥ b\}} X (L (v)))$
8		dchrisum0f.x	$⊢ φ \to X \in D$
9		dchrisum0fmul.a	$⊢ φ \to A \in ℕ$
10		dchrisum0fmul.b	$⊢ φ \to B \in ℕ$
11		dchrisum0fmul.m	$⊢ φ \to A \gcd B = 1$
12		eqid	$⊢ \{q \in ℕ \| q ∥ A\} = \{q \in ℕ \| q ∥ A\}$
13		eqid	$⊢ \{q \in ℕ \| q ∥ B\} = \{q \in ℕ \| q ∥ B\}$
14		eqid	$⊢ \{q \in ℕ \| q ∥ A B\} = \{q \in ℕ \| q ∥ A B\}$
15	8	adantr	$⊢ (φ \land j \in \{q \in ℕ \| q ∥ A\}) \to X \in D$
16		elrabi	$⊢ j \in \{q \in ℕ \| q ∥ A\} \to j \in ℕ$
17	16	nnzd	$⊢ j \in \{q \in ℕ \| q ∥ A\} \to j \in ℤ$
18	17	adantl	$⊢ (φ \land j \in \{q \in ℕ \| q ∥ A\}) \to j \in ℤ$
19	4 1 5 2 15 18	dchrzrhcl	$⊢ (φ \land j \in \{q \in ℕ \| q ∥ A\}) \to X (L (j)) \in ℂ$
20	8	adantr	$⊢ (φ \land k \in \{q \in ℕ \| q ∥ B\}) \to X \in D$
21		elrabi	$⊢ k \in \{q \in ℕ \| q ∥ B\} \to k \in ℕ$
22	21	nnzd	$⊢ k \in \{q \in ℕ \| q ∥ B\} \to k \in ℤ$
23	22	adantl	$⊢ (φ \land k \in \{q \in ℕ \| q ∥ B\}) \to k \in ℤ$
24	4 1 5 2 20 23	dchrzrhcl	$⊢ (φ \land k \in \{q \in ℕ \| q ∥ B\}) \to X (L (k)) \in ℂ$
25	17 22	anim12i	$⊢ (j \in \{q \in ℕ \| q ∥ A\} \land k \in \{q \in ℕ \| q ∥ B\}) \to (j \in ℤ \land k \in ℤ)$
26	8	adantr	$⊢ (φ \land (j \in ℤ \land k \in ℤ)) \to X \in D$
27		simprl	$⊢ (φ \land (j \in ℤ \land k \in ℤ)) \to j \in ℤ$
28		simprr	$⊢ (φ \land (j \in ℤ \land k \in ℤ)) \to k \in ℤ$
29	4 1 5 2 26 27 28	dchrzrhmul	$⊢ (φ \land (j \in ℤ \land k \in ℤ)) \to X (L (j k)) = X (L (j)) X (L (k))$
30	29	eqcomd	$⊢ (φ \land (j \in ℤ \land k \in ℤ)) \to X (L (j)) X (L (k)) = X (L (j k))$
31	25 30	sylan2	$⊢ (φ \land (j \in \{q \in ℕ \| q ∥ A\} \land k \in \{q \in ℕ \| q ∥ B\})) \to X (L (j)) X (L (k)) = X (L (j k))$
32		2fveq3	$⊢ i = j k \to X (L (i)) = X (L (j k))$
33	9 10 11 12 13 14 19 24 31 32	fsumdvdsmul	$⊢ φ \to \sum_{j \in \{q \in ℕ \| q ∥ A\}} X (L (j)) \sum_{k \in \{q \in ℕ \| q ∥ B\}} X (L (k)) = \sum_{i \in \{q \in ℕ \| q ∥ A B\}} X (L (i))$
34	1 2 3 4 5 6 7	dchrisum0fval	$⊢ A \in ℕ \to F (A) = \sum_{j \in \{q \in ℕ \| q ∥ A\}} X (L (j))$
35	9 34	syl	$⊢ φ \to F (A) = \sum_{j \in \{q \in ℕ \| q ∥ A\}} X (L (j))$
36	1 2 3 4 5 6 7	dchrisum0fval	$⊢ B \in ℕ \to F (B) = \sum_{k \in \{q \in ℕ \| q ∥ B\}} X (L (k))$
37	10 36	syl	$⊢ φ \to F (B) = \sum_{k \in \{q \in ℕ \| q ∥ B\}} X (L (k))$
38	35 37	oveq12d	$⊢ φ \to F (A) F (B) = \sum_{j \in \{q \in ℕ \| q ∥ A\}} X (L (j)) \sum_{k \in \{q \in ℕ \| q ∥ B\}} X (L (k))$
39	9 10	nnmulcld	$⊢ φ \to A B \in ℕ$
40	1 2 3 4 5 6 7	dchrisum0fval	$⊢ A B \in ℕ \to F (A B) = \sum_{i \in \{q \in ℕ \| q ∥ A B\}} X (L (i))$
41	39 40	syl	$⊢ φ \to F (A B) = \sum_{i \in \{q \in ℕ \| q ∥ A B\}} X (L (i))$
42	33 38 41	3eqtr4rd	$⊢ φ \to F (A B) = F (A) F (B)$

Metamath Proof Explorer

Theorem dchrisum0fmul

Proof