Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dchrisum0fmul | Structured version Visualization version GIF version |
Description: The function 𝐹, 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 |
---|---|
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) |
Ref | Expression |
---|---|
dchrisum0fmul | ⊢ (𝜑 → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) · (𝐹‘𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dchrisum0fmul.a | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
2 | dchrisum0fmul.b | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℕ) | |
3 | dchrisum0fmul.m | . . 3 ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) | |
4 | eqid 2737 | . . 3 ⊢ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} = {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} | |
5 | eqid 2737 | . . 3 ⊢ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵} = {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵} | |
6 | eqid 2737 | . . 3 ⊢ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝐴 · 𝐵)} = {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝐴 · 𝐵)} | |
7 | rpvmasum2.g | . . . 4 ⊢ 𝐺 = (DChr‘𝑁) | |
8 | rpvmasum.z | . . . 4 ⊢ 𝑍 = (ℤ/nℤ‘𝑁) | |
9 | rpvmasum2.d | . . . 4 ⊢ 𝐷 = (Base‘𝐺) | |
10 | rpvmasum.l | . . . 4 ⊢ 𝐿 = (ℤRHom‘𝑍) | |
11 | dchrisum0f.x | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐷) | |
12 | 11 | adantr 482 | . . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴}) → 𝑋 ∈ 𝐷) |
13 | elrabi 3634 | . . . . . 6 ⊢ (𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} → 𝑗 ∈ ℕ) | |
14 | 13 | nnzd 12535 | . . . . 5 ⊢ (𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} → 𝑗 ∈ ℤ) |
15 | 14 | adantl 483 | . . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴}) → 𝑗 ∈ ℤ) |
16 | 7, 8, 9, 10, 12, 15 | dchrzrhcl 26503 | . . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴}) → (𝑋‘(𝐿‘𝑗)) ∈ ℂ) |
17 | 11 | adantr 482 | . . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵}) → 𝑋 ∈ 𝐷) |
18 | elrabi 3634 | . . . . . 6 ⊢ (𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵} → 𝑘 ∈ ℕ) | |
19 | 18 | nnzd 12535 | . . . . 5 ⊢ (𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵} → 𝑘 ∈ ℤ) |
20 | 19 | adantl 483 | . . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵}) → 𝑘 ∈ ℤ) |
21 | 7, 8, 9, 10, 17, 20 | dchrzrhcl 26503 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵}) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
22 | 14, 19 | anim12i 614 | . . . 4 ⊢ ((𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} ∧ 𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵}) → (𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ)) |
23 | 11 | adantr 482 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ)) → 𝑋 ∈ 𝐷) |
24 | simprl 769 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ)) → 𝑗 ∈ ℤ) | |
25 | simprr 771 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ)) → 𝑘 ∈ ℤ) | |
26 | 7, 8, 9, 10, 23, 24, 25 | dchrzrhmul 26504 | . . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ)) → (𝑋‘(𝐿‘(𝑗 · 𝑘))) = ((𝑋‘(𝐿‘𝑗)) · (𝑋‘(𝐿‘𝑘)))) |
27 | 26 | eqcomd 2743 | . . . 4 ⊢ ((𝜑 ∧ (𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ)) → ((𝑋‘(𝐿‘𝑗)) · (𝑋‘(𝐿‘𝑘))) = (𝑋‘(𝐿‘(𝑗 · 𝑘)))) |
28 | 22, 27 | sylan2 594 | . . 3 ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} ∧ 𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵})) → ((𝑋‘(𝐿‘𝑗)) · (𝑋‘(𝐿‘𝑘))) = (𝑋‘(𝐿‘(𝑗 · 𝑘)))) |
29 | 2fveq3 6839 | . . 3 ⊢ (𝑖 = (𝑗 · 𝑘) → (𝑋‘(𝐿‘𝑖)) = (𝑋‘(𝐿‘(𝑗 · 𝑘)))) | |
30 | 1, 2, 3, 4, 5, 6, 16, 21, 28, 29 | fsumdvdsmul 26454 | . 2 ⊢ (𝜑 → (Σ𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} (𝑋‘(𝐿‘𝑗)) · Σ𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵} (𝑋‘(𝐿‘𝑘))) = Σ𝑖 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝐴 · 𝐵)} (𝑋‘(𝐿‘𝑖))) |
31 | rpvmasum.a | . . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ) | |
32 | rpvmasum2.1 | . . . . 5 ⊢ 1 = (0g‘𝐺) | |
33 | dchrisum0f.f | . . . . 5 ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) | |
34 | 8, 10, 31, 7, 9, 32, 33 | dchrisum0fval 26763 | . . . 4 ⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) = Σ𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} (𝑋‘(𝐿‘𝑗))) |
35 | 1, 34 | syl 17 | . . 3 ⊢ (𝜑 → (𝐹‘𝐴) = Σ𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} (𝑋‘(𝐿‘𝑗))) |
36 | 8, 10, 31, 7, 9, 32, 33 | dchrisum0fval 26763 | . . . 4 ⊢ (𝐵 ∈ ℕ → (𝐹‘𝐵) = Σ𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵} (𝑋‘(𝐿‘𝑘))) |
37 | 2, 36 | syl 17 | . . 3 ⊢ (𝜑 → (𝐹‘𝐵) = Σ𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵} (𝑋‘(𝐿‘𝑘))) |
38 | 35, 37 | oveq12d 7364 | . 2 ⊢ (𝜑 → ((𝐹‘𝐴) · (𝐹‘𝐵)) = (Σ𝑗 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} (𝑋‘(𝐿‘𝑗)) · Σ𝑘 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐵} (𝑋‘(𝐿‘𝑘)))) |
39 | 1, 2 | nnmulcld 12136 | . . 3 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
40 | 8, 10, 31, 7, 9, 32, 33 | dchrisum0fval 26763 | . . 3 ⊢ ((𝐴 · 𝐵) ∈ ℕ → (𝐹‘(𝐴 · 𝐵)) = Σ𝑖 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝐴 · 𝐵)} (𝑋‘(𝐿‘𝑖))) |
41 | 39, 40 | syl 17 | . 2 ⊢ (𝜑 → (𝐹‘(𝐴 · 𝐵)) = Σ𝑖 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ (𝐴 · 𝐵)} (𝑋‘(𝐿‘𝑖))) |
42 | 30, 38, 41 | 3eqtr4rd 2788 | 1 ⊢ (𝜑 → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) · (𝐹‘𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1541 ∈ wcel 2106 {crab 3405 class class class wbr 5100 ↦ cmpt 5183 ‘cfv 6488 (class class class)co 7346 1c1 10982 · cmul 10986 ℕcn 12083 ℤcz 12429 Σcsu 15501 ∥ cdvds 16067 gcd cgcd 16305 Basecbs 17014 0gc0g 17252 ℤRHomczrh 20811 ℤ/nℤczn 20814 DChrcdchr 26490 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5237 ax-sep 5251 ax-nul 5258 ax-pow 5315 ax-pr 5379 ax-un 7659 ax-inf2 9507 ax-cnex 11037 ax-resscn 11038 ax-1cn 11039 ax-icn 11040 ax-addcl 11041 ax-addrcl 11042 ax-mulcl 11043 ax-mulrcl 11044 ax-mulcom 11045 ax-addass 11046 ax-mulass 11047 ax-distr 11048 ax-i2m1 11049 ax-1ne0 11050 ax-1rid 11051 ax-rnegex 11052 ax-rrecex 11053 ax-cnre 11054 ax-pre-lttri 11055 ax-pre-lttrn 11056 ax-pre-ltadd 11057 ax-pre-mulgt0 11058 ax-pre-sup 11059 ax-addf 11060 ax-mulf 11061 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3351 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3735 df-csb 3851 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3924 df-nul 4278 df-if 4482 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4861 df-int 4903 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5184 df-tr 5218 df-id 5525 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5582 df-se 5583 df-we 5584 df-xp 5633 df-rel 5634 df-cnv 5635 df-co 5636 df-dm 5637 df-rn 5638 df-res 5639 df-ima 5640 df-pred 6246 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6440 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7302 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7790 df-1st 7908 df-2nd 7909 df-tpos 8121 df-frecs 8176 df-wrecs 8207 df-recs 8281 df-rdg 8320 df-1o 8376 df-er 8578 df-ec 8580 df-qs 8584 df-map 8697 df-en 8814 df-dom 8815 df-sdom 8816 df-fin 8817 df-sup 9308 df-inf 9309 df-oi 9376 df-card 9805 df-pnf 11121 df-mnf 11122 df-xr 11123 df-ltxr 11124 df-le 11125 df-sub 11317 df-neg 11318 df-div 11743 df-nn 12084 df-2 12146 df-3 12147 df-4 12148 df-5 12149 df-6 12150 df-7 12151 df-8 12152 df-9 12153 df-n0 12344 df-z 12430 df-dec 12548 df-uz 12693 df-rp 12841 df-fz 13350 df-fzo 13493 df-fl 13622 df-mod 13700 df-seq 13832 df-exp 13893 df-hash 14155 df-cj 14914 df-re 14915 df-im 14916 df-sqrt 15050 df-abs 15051 df-clim 15301 df-sum 15502 df-dvds 16068 df-gcd 16306 df-struct 16950 df-sets 16967 df-slot 16985 df-ndx 16997 df-base 17015 df-ress 17044 df-plusg 17077 df-mulr 17078 df-starv 17079 df-sca 17080 df-vsca 17081 df-ip 17082 df-tset 17083 df-ple 17084 df-ds 17086 df-unif 17087 df-0g 17254 df-imas 17321 df-qus 17322 df-mgm 18428 df-sgrp 18477 df-mnd 18488 df-mhm 18532 df-grp 18681 df-minusg 18682 df-sbg 18683 df-mulg 18802 df-subg 18853 df-nsg 18854 df-eqg 18855 df-ghm 18933 df-cmn 19488 df-abl 19489 df-mgp 19820 df-ur 19837 df-ring 19884 df-cring 19885 df-oppr 19961 df-dvdsr 19982 df-unit 19983 df-rnghom 20058 df-subrg 20131 df-lmod 20235 df-lss 20304 df-lsp 20344 df-sra 20544 df-rgmod 20545 df-lidl 20546 df-rsp 20547 df-2idl 20613 df-cnfld 20708 df-zring 20781 df-zrh 20815 df-zn 20818 df-dchr 26491 |
This theorem is referenced by: dchrisum0flblem2 26767 |
Copyright terms: Public domain | W3C validator |