Metamath Proof Explorer


Theorem fsumdvdsmul

Description: Product of two divisor sums. (This is also the main part of the proof that " sum_ k || N F ( k ) is a multiplicative function if F is".) (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Hypotheses dvdsmulf1o.1 โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
dvdsmulf1o.2 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
dvdsmulf1o.3 โŠข ( ๐œ‘ โ†’ ( ๐‘€ gcd ๐‘ ) = 1 )
dvdsmulf1o.x โŠข ๐‘‹ = { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐‘€ }
dvdsmulf1o.y โŠข ๐‘Œ = { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐‘ }
dvdsmulf1o.z โŠข ๐‘ = { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ( ๐‘€ ยท ๐‘ ) }
fsumdvdsmul.4 โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘‹ ) โ†’ ๐ด โˆˆ โ„‚ )
fsumdvdsmul.5 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘Œ ) โ†’ ๐ต โˆˆ โ„‚ )
fsumdvdsmul.6 โŠข ( ( ๐œ‘ โˆง ( ๐‘— โˆˆ ๐‘‹ โˆง ๐‘˜ โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ยท ๐ต ) = ๐ท )
fsumdvdsmul.7 โŠข ( ๐‘– = ( ๐‘— ยท ๐‘˜ ) โ†’ ๐ถ = ๐ท )
Assertion fsumdvdsmul ( ๐œ‘ โ†’ ( ฮฃ ๐‘— โˆˆ ๐‘‹ ๐ด ยท ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ต ) = ฮฃ ๐‘– โˆˆ ๐‘ ๐ถ )

Proof

Step Hyp Ref Expression
1 dvdsmulf1o.1 โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
2 dvdsmulf1o.2 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
3 dvdsmulf1o.3 โŠข ( ๐œ‘ โ†’ ( ๐‘€ gcd ๐‘ ) = 1 )
4 dvdsmulf1o.x โŠข ๐‘‹ = { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐‘€ }
5 dvdsmulf1o.y โŠข ๐‘Œ = { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐‘ }
6 dvdsmulf1o.z โŠข ๐‘ = { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ( ๐‘€ ยท ๐‘ ) }
7 fsumdvdsmul.4 โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘‹ ) โ†’ ๐ด โˆˆ โ„‚ )
8 fsumdvdsmul.5 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘Œ ) โ†’ ๐ต โˆˆ โ„‚ )
9 fsumdvdsmul.6 โŠข ( ( ๐œ‘ โˆง ( ๐‘— โˆˆ ๐‘‹ โˆง ๐‘˜ โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ยท ๐ต ) = ๐ท )
10 fsumdvdsmul.7 โŠข ( ๐‘– = ( ๐‘— ยท ๐‘˜ ) โ†’ ๐ถ = ๐ท )
11 fzfid โŠข ( ๐œ‘ โ†’ ( 1 ... ๐‘€ ) โˆˆ Fin )
12 dvdsssfz1 โŠข ( ๐‘€ โˆˆ โ„• โ†’ { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐‘€ } โŠ† ( 1 ... ๐‘€ ) )
13 1 12 syl โŠข ( ๐œ‘ โ†’ { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐‘€ } โŠ† ( 1 ... ๐‘€ ) )
14 4 13 eqsstrid โŠข ( ๐œ‘ โ†’ ๐‘‹ โŠ† ( 1 ... ๐‘€ ) )
15 11 14 ssfid โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ Fin )
16 fzfid โŠข ( ๐œ‘ โ†’ ( 1 ... ๐‘ ) โˆˆ Fin )
17 dvdsssfz1 โŠข ( ๐‘ โˆˆ โ„• โ†’ { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐‘ } โŠ† ( 1 ... ๐‘ ) )
18 2 17 syl โŠข ( ๐œ‘ โ†’ { ๐‘ฅ โˆˆ โ„• โˆฃ ๐‘ฅ โˆฅ ๐‘ } โŠ† ( 1 ... ๐‘ ) )
19 5 18 eqsstrid โŠข ( ๐œ‘ โ†’ ๐‘Œ โŠ† ( 1 ... ๐‘ ) )
20 16 19 ssfid โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ Fin )
21 20 8 fsumcl โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ต โˆˆ โ„‚ )
22 15 21 7 fsummulc1 โŠข ( ๐œ‘ โ†’ ( ฮฃ ๐‘— โˆˆ ๐‘‹ ๐ด ยท ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ต ) = ฮฃ ๐‘— โˆˆ ๐‘‹ ( ๐ด ยท ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ต ) )
23 20 adantr โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘‹ ) โ†’ ๐‘Œ โˆˆ Fin )
24 8 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘‹ ) โˆง ๐‘˜ โˆˆ ๐‘Œ ) โ†’ ๐ต โˆˆ โ„‚ )
25 23 7 24 fsummulc2 โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘‹ ) โ†’ ( ๐ด ยท ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ต ) = ฮฃ ๐‘˜ โˆˆ ๐‘Œ ( ๐ด ยท ๐ต ) )
26 9 anassrs โŠข ( ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘‹ ) โˆง ๐‘˜ โˆˆ ๐‘Œ ) โ†’ ( ๐ด ยท ๐ต ) = ๐ท )
27 26 sumeq2dv โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘‹ ) โ†’ ฮฃ ๐‘˜ โˆˆ ๐‘Œ ( ๐ด ยท ๐ต ) = ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ท )
28 25 27 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘— โˆˆ ๐‘‹ ) โ†’ ( ๐ด ยท ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ต ) = ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ท )
29 28 sumeq2dv โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘— โˆˆ ๐‘‹ ( ๐ด ยท ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ต ) = ฮฃ ๐‘— โˆˆ ๐‘‹ ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ท )
30 fveq2 โŠข ( ๐‘ง = โŸจ ๐‘— , ๐‘˜ โŸฉ โ†’ ( ยท โ€˜ ๐‘ง ) = ( ยท โ€˜ โŸจ ๐‘— , ๐‘˜ โŸฉ ) )
31 df-ov โŠข ( ๐‘— ยท ๐‘˜ ) = ( ยท โ€˜ โŸจ ๐‘— , ๐‘˜ โŸฉ )
32 30 31 eqtr4di โŠข ( ๐‘ง = โŸจ ๐‘— , ๐‘˜ โŸฉ โ†’ ( ยท โ€˜ ๐‘ง ) = ( ๐‘— ยท ๐‘˜ ) )
33 32 csbeq1d โŠข ( ๐‘ง = โŸจ ๐‘— , ๐‘˜ โŸฉ โ†’ โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ = โฆ‹ ( ๐‘— ยท ๐‘˜ ) / ๐‘– โฆŒ ๐ถ )
34 ovex โŠข ( ๐‘— ยท ๐‘˜ ) โˆˆ V
35 34 10 csbie โŠข โฆ‹ ( ๐‘— ยท ๐‘˜ ) / ๐‘– โฆŒ ๐ถ = ๐ท
36 33 35 eqtrdi โŠข ( ๐‘ง = โŸจ ๐‘— , ๐‘˜ โŸฉ โ†’ โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ = ๐ท )
37 7 adantrr โŠข ( ( ๐œ‘ โˆง ( ๐‘— โˆˆ ๐‘‹ โˆง ๐‘˜ โˆˆ ๐‘Œ ) ) โ†’ ๐ด โˆˆ โ„‚ )
38 8 adantrl โŠข ( ( ๐œ‘ โˆง ( ๐‘— โˆˆ ๐‘‹ โˆง ๐‘˜ โˆˆ ๐‘Œ ) ) โ†’ ๐ต โˆˆ โ„‚ )
39 37 38 mulcld โŠข ( ( ๐œ‘ โˆง ( ๐‘— โˆˆ ๐‘‹ โˆง ๐‘˜ โˆˆ ๐‘Œ ) ) โ†’ ( ๐ด ยท ๐ต ) โˆˆ โ„‚ )
40 9 39 eqeltrrd โŠข ( ( ๐œ‘ โˆง ( ๐‘— โˆˆ ๐‘‹ โˆง ๐‘˜ โˆˆ ๐‘Œ ) ) โ†’ ๐ท โˆˆ โ„‚ )
41 36 15 20 40 fsumxp โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘— โˆˆ ๐‘‹ ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ท = ฮฃ ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ )
42 nfcv โŠข โ„ฒ ๐‘ค ๐ถ
43 nfcsb1v โŠข โ„ฒ ๐‘– โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ
44 csbeq1a โŠข ( ๐‘– = ๐‘ค โ†’ ๐ถ = โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ )
45 42 43 44 cbvsumi โŠข ฮฃ ๐‘– โˆˆ ๐‘ ๐ถ = ฮฃ ๐‘ค โˆˆ ๐‘ โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ
46 csbeq1 โŠข ( ๐‘ค = ( ยท โ€˜ ๐‘ง ) โ†’ โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ = โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ )
47 xpfi โŠข ( ( ๐‘‹ โˆˆ Fin โˆง ๐‘Œ โˆˆ Fin ) โ†’ ( ๐‘‹ ร— ๐‘Œ ) โˆˆ Fin )
48 15 20 47 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ร— ๐‘Œ ) โˆˆ Fin )
49 1 2 3 4 5 6 dvdsmulf1o โŠข ( ๐œ‘ โ†’ ( ยท โ†พ ( ๐‘‹ ร— ๐‘Œ ) ) : ( ๐‘‹ ร— ๐‘Œ ) โ€“1-1-ontoโ†’ ๐‘ )
50 fvres โŠข ( ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) โ†’ ( ( ยท โ†พ ( ๐‘‹ ร— ๐‘Œ ) ) โ€˜ ๐‘ง ) = ( ยท โ€˜ ๐‘ง ) )
51 50 adantl โŠข ( ( ๐œ‘ โˆง ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) ) โ†’ ( ( ยท โ†พ ( ๐‘‹ ร— ๐‘Œ ) ) โ€˜ ๐‘ง ) = ( ยท โ€˜ ๐‘ง ) )
52 40 ralrimivva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘— โˆˆ ๐‘‹ โˆ€ ๐‘˜ โˆˆ ๐‘Œ ๐ท โˆˆ โ„‚ )
53 36 eleq1d โŠข ( ๐‘ง = โŸจ ๐‘— , ๐‘˜ โŸฉ โ†’ ( โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ โ†” ๐ท โˆˆ โ„‚ ) )
54 53 ralxp โŠข ( โˆ€ ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ โ†” โˆ€ ๐‘— โˆˆ ๐‘‹ โˆ€ ๐‘˜ โˆˆ ๐‘Œ ๐ท โˆˆ โ„‚ )
55 52 54 sylibr โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ )
56 ax-mulf โŠข ยท : ( โ„‚ ร— โ„‚ ) โŸถ โ„‚
57 ffn โŠข ( ยท : ( โ„‚ ร— โ„‚ ) โŸถ โ„‚ โ†’ ยท Fn ( โ„‚ ร— โ„‚ ) )
58 56 57 ax-mp โŠข ยท Fn ( โ„‚ ร— โ„‚ )
59 4 ssrab3 โŠข ๐‘‹ โŠ† โ„•
60 nnsscn โŠข โ„• โŠ† โ„‚
61 59 60 sstri โŠข ๐‘‹ โŠ† โ„‚
62 5 ssrab3 โŠข ๐‘Œ โŠ† โ„•
63 62 60 sstri โŠข ๐‘Œ โŠ† โ„‚
64 xpss12 โŠข ( ( ๐‘‹ โŠ† โ„‚ โˆง ๐‘Œ โŠ† โ„‚ ) โ†’ ( ๐‘‹ ร— ๐‘Œ ) โŠ† ( โ„‚ ร— โ„‚ ) )
65 61 63 64 mp2an โŠข ( ๐‘‹ ร— ๐‘Œ ) โŠ† ( โ„‚ ร— โ„‚ )
66 46 eleq1d โŠข ( ๐‘ค = ( ยท โ€˜ ๐‘ง ) โ†’ ( โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ โ†” โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ ) )
67 66 ralima โŠข ( ( ยท Fn ( โ„‚ ร— โ„‚ ) โˆง ( ๐‘‹ ร— ๐‘Œ ) โŠ† ( โ„‚ ร— โ„‚ ) ) โ†’ ( โˆ€ ๐‘ค โˆˆ ( ยท โ€œ ( ๐‘‹ ร— ๐‘Œ ) ) โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ โ†” โˆ€ ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ ) )
68 58 65 67 mp2an โŠข ( โˆ€ ๐‘ค โˆˆ ( ยท โ€œ ( ๐‘‹ ร— ๐‘Œ ) ) โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ โ†” โˆ€ ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ )
69 df-ima โŠข ( ยท โ€œ ( ๐‘‹ ร— ๐‘Œ ) ) = ran ( ยท โ†พ ( ๐‘‹ ร— ๐‘Œ ) )
70 f1ofo โŠข ( ( ยท โ†พ ( ๐‘‹ ร— ๐‘Œ ) ) : ( ๐‘‹ ร— ๐‘Œ ) โ€“1-1-ontoโ†’ ๐‘ โ†’ ( ยท โ†พ ( ๐‘‹ ร— ๐‘Œ ) ) : ( ๐‘‹ ร— ๐‘Œ ) โ€“ontoโ†’ ๐‘ )
71 forn โŠข ( ( ยท โ†พ ( ๐‘‹ ร— ๐‘Œ ) ) : ( ๐‘‹ ร— ๐‘Œ ) โ€“ontoโ†’ ๐‘ โ†’ ran ( ยท โ†พ ( ๐‘‹ ร— ๐‘Œ ) ) = ๐‘ )
72 49 70 71 3syl โŠข ( ๐œ‘ โ†’ ran ( ยท โ†พ ( ๐‘‹ ร— ๐‘Œ ) ) = ๐‘ )
73 69 72 eqtrid โŠข ( ๐œ‘ โ†’ ( ยท โ€œ ( ๐‘‹ ร— ๐‘Œ ) ) = ๐‘ )
74 73 raleqdv โŠข ( ๐œ‘ โ†’ ( โˆ€ ๐‘ค โˆˆ ( ยท โ€œ ( ๐‘‹ ร— ๐‘Œ ) ) โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ โ†” โˆ€ ๐‘ค โˆˆ ๐‘ โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ ) )
75 68 74 bitr3id โŠข ( ๐œ‘ โ†’ ( โˆ€ ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ โ†” โˆ€ ๐‘ค โˆˆ ๐‘ โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ ) )
76 55 75 mpbid โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ค โˆˆ ๐‘ โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ )
77 76 r19.21bi โŠข ( ( ๐œ‘ โˆง ๐‘ค โˆˆ ๐‘ ) โ†’ โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ โˆˆ โ„‚ )
78 46 48 49 51 77 fsumf1o โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘ค โˆˆ ๐‘ โฆ‹ ๐‘ค / ๐‘– โฆŒ ๐ถ = ฮฃ ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ )
79 45 78 eqtrid โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘– โˆˆ ๐‘ ๐ถ = ฮฃ ๐‘ง โˆˆ ( ๐‘‹ ร— ๐‘Œ ) โฆ‹ ( ยท โ€˜ ๐‘ง ) / ๐‘– โฆŒ ๐ถ )
80 41 79 eqtr4d โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘— โˆˆ ๐‘‹ ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ท = ฮฃ ๐‘– โˆˆ ๐‘ ๐ถ )
81 22 29 80 3eqtrd โŠข ( ๐œ‘ โ†’ ( ฮฃ ๐‘— โˆˆ ๐‘‹ ๐ด ยท ฮฃ ๐‘˜ โˆˆ ๐‘Œ ๐ต ) = ฮฃ ๐‘– โˆˆ ๐‘ ๐ถ )