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	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum2.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum2.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum2.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrisum0f.f	⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
	dchrisum0f.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum0fmul.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	dchrisum0fmul.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	dchrisum0fmul.m	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
Assertion	dchrisum0fmul	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) · ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum2.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum2.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum2.1	⊢ 1 = ( 0g ‘ 𝐺 )
7		dchrisum0f.f	⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
8		dchrisum0f.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9		dchrisum0fmul.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
10		dchrisum0fmul.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
11		dchrisum0fmul.m	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
12		eqid	⊢ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } = { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 }
13		eqid	⊢ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } = { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 }
14		eqid	⊢ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝐴 · 𝐵 ) } = { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝐴 · 𝐵 ) }
15	8	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ) → 𝑋 ∈ 𝐷 )
16		elrabi	⊢ ( 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } → 𝑗 ∈ ℕ )
17	16	nnzd	⊢ ( 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } → 𝑗 ∈ ℤ )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ) → 𝑗 ∈ ℤ )
19	4 1 5 2 15 18	dchrzrhcl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑗 ) ) ∈ ℂ )
20	8	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } ) → 𝑋 ∈ 𝐷 )
21		elrabi	⊢ ( 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } → 𝑘 ∈ ℕ )
22	21	nnzd	⊢ ( 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } → 𝑘 ∈ ℤ )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } ) → 𝑘 ∈ ℤ )
24	4 1 5 2 20 23	dchrzrhcl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ∈ ℂ )
25	17 22	anim12i	⊢ ( ( 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } ) → ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ ) )
26	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → 𝑋 ∈ 𝐷 )
27		simprl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → 𝑗 ∈ ℤ )
28		simprr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → 𝑘 ∈ ℤ )
29	4 1 5 2 26 27 28	dchrzrhmul	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑗 · 𝑘 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑗 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) )
30	29	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑗 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑗 · 𝑘 ) ) ) )
31	25 30	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ∧ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑗 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑗 · 𝑘 ) ) ) )
32		2fveq3	⊢ ( 𝑖 = ( 𝑗 · 𝑘 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑗 · 𝑘 ) ) ) )
33	9 10 11 12 13 14 19 24 31 32	fsumdvdsmul	⊢ ( 𝜑 → ( Σ 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑗 ) ) · Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) = Σ 𝑖 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝐴 · 𝐵 ) } ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) )
34	1 2 3 4 5 6 7	dchrisum0fval	⊢ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝐴 ) = Σ 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑗 ) ) )
35	9 34	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = Σ 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑗 ) ) )
36	1 2 3 4 5 6 7	dchrisum0fval	⊢ ( 𝐵 ∈ ℕ → ( 𝐹 ‘ 𝐵 ) = Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) )
37	10 36	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) )
38	35 37	oveq12d	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) · ( 𝐹 ‘ 𝐵 ) ) = ( Σ 𝑗 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑗 ) ) · Σ 𝑘 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑘 ) ) ) )
39	9 10	nnmulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℕ )
40	1 2 3 4 5 6 7	dchrisum0fval	⊢ ( ( 𝐴 · 𝐵 ) ∈ ℕ → ( 𝐹 ‘ ( 𝐴 · 𝐵 ) ) = Σ 𝑖 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝐴 · 𝐵 ) } ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) )
41	39 40	syl	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 · 𝐵 ) ) = Σ 𝑖 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ ( 𝐴 · 𝐵 ) } ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) )
42	33 38 41	3eqtr4rd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) · ( 𝐹 ‘ 𝐵 ) ) )