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) Avoid ax-mulf . (Revised by GG, 18-Apr-2025)

Ref Expression
Hypotheses mpodvdsmulf1o.1 
|- ( ph -> M e. NN )
mpodvdsmulf1o.2 
|- ( ph -> N e. NN )
mpodvdsmulf1o.3 
|- ( ph -> ( M gcd N ) = 1 )
mpodvdsmulf1o.x 
|- X = { x e. NN | x || M }
mpodvdsmulf1o.y 
|- Y = { x e. NN | x || N }
mpodvdsmulf1o.z 
|- Z = { x e. NN | x || ( M x. N ) }
fsumdvdsmul.4 
|- ( ( ph /\ j e. X ) -> A e. CC )
fsumdvdsmul.5 
|- ( ( ph /\ k e. Y ) -> B e. CC )
fsumdvdsmul.6 
|- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> ( A x. B ) = D )
fsumdvdsmul.7 
|- ( i = ( j x. k ) -> C = D )
Assertion fsumdvdsmul 
|- ( ph -> ( sum_ j e. X A x. sum_ k e. Y B ) = sum_ i e. Z C )

Proof

Step Hyp Ref Expression
1 mpodvdsmulf1o.1 
 |-  ( ph -> M e. NN )
2 mpodvdsmulf1o.2 
 |-  ( ph -> N e. NN )
3 mpodvdsmulf1o.3 
 |-  ( ph -> ( M gcd N ) = 1 )
4 mpodvdsmulf1o.x 
 |-  X = { x e. NN | x || M }
5 mpodvdsmulf1o.y 
 |-  Y = { x e. NN | x || N }
6 mpodvdsmulf1o.z 
 |-  Z = { x e. NN | x || ( M x. N ) }
7 fsumdvdsmul.4 
 |-  ( ( ph /\ j e. X ) -> A e. CC )
8 fsumdvdsmul.5 
 |-  ( ( ph /\ k e. Y ) -> B e. CC )
9 fsumdvdsmul.6 
 |-  ( ( ph /\ ( j e. X /\ k e. Y ) ) -> ( A x. B ) = D )
10 fsumdvdsmul.7 
 |-  ( i = ( j x. k ) -> C = D )
11 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
12 dvdsssfz1 
 |-  ( M e. NN -> { x e. NN | x || M } C_ ( 1 ... M ) )
13 1 12 syl 
 |-  ( ph -> { x e. NN | x || M } C_ ( 1 ... M ) )
14 4 13 eqsstrid 
 |-  ( ph -> X C_ ( 1 ... M ) )
15 11 14 ssfid 
 |-  ( ph -> X e. Fin )
16 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
17 dvdsssfz1 
 |-  ( N e. NN -> { x e. NN | x || N } C_ ( 1 ... N ) )
18 2 17 syl 
 |-  ( ph -> { x e. NN | x || N } C_ ( 1 ... N ) )
19 5 18 eqsstrid 
 |-  ( ph -> Y C_ ( 1 ... N ) )
20 16 19 ssfid 
 |-  ( ph -> Y e. Fin )
21 20 8 fsumcl 
 |-  ( ph -> sum_ k e. Y B e. CC )
22 15 21 7 fsummulc1 
 |-  ( ph -> ( sum_ j e. X A x. sum_ k e. Y B ) = sum_ j e. X ( A x. sum_ k e. Y B ) )
23 20 adantr 
 |-  ( ( ph /\ j e. X ) -> Y e. Fin )
24 8 adantlr 
 |-  ( ( ( ph /\ j e. X ) /\ k e. Y ) -> B e. CC )
25 23 7 24 fsummulc2 
 |-  ( ( ph /\ j e. X ) -> ( A x. sum_ k e. Y B ) = sum_ k e. Y ( A x. B ) )
26 9 anassrs 
 |-  ( ( ( ph /\ j e. X ) /\ k e. Y ) -> ( A x. B ) = D )
27 26 sumeq2dv 
 |-  ( ( ph /\ j e. X ) -> sum_ k e. Y ( A x. B ) = sum_ k e. Y D )
28 25 27 eqtrd 
 |-  ( ( ph /\ j e. X ) -> ( A x. sum_ k e. Y B ) = sum_ k e. Y D )
29 28 sumeq2dv 
 |-  ( ph -> sum_ j e. X ( A x. sum_ k e. Y B ) = sum_ j e. X sum_ k e. Y D )
30 elxpi 
 |-  ( z e. ( X X. Y ) -> E. u E. v ( z = <. u , v >. /\ ( u e. X /\ v e. Y ) ) )
31 fveq2 
 |-  ( <. u , v >. = z -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) )
32 31 eqcoms 
 |-  ( z = <. u , v >. -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) )
33 fveq2 
 |-  ( <. u , v >. = z -> ( x. ` <. u , v >. ) = ( x. ` z ) )
34 33 eqcoms 
 |-  ( z = <. u , v >. -> ( x. ` <. u , v >. ) = ( x. ` z ) )
35 32 34 eqeq12d 
 |-  ( z = <. u , v >. -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u , v >. ) <-> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) )
36 35 biimpd 
 |-  ( z = <. u , v >. -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u , v >. ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) )
37 4 ssrab3 
 |-  X C_ NN
38 nnsscn 
 |-  NN C_ CC
39 37 38 sstri 
 |-  X C_ CC
40 39 sseli 
 |-  ( u e. X -> u e. CC )
41 5 ssrab3 
 |-  Y C_ NN
42 41 38 sstri 
 |-  Y C_ CC
43 42 sseli 
 |-  ( v e. Y -> v e. CC )
44 ovmpot 
 |-  ( ( u e. CC /\ v e. CC ) -> ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) = ( u x. v ) )
45 df-ov 
 |-  ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. )
46 df-ov 
 |-  ( u x. v ) = ( x. ` <. u , v >. )
47 44 45 46 3eqtr3g 
 |-  ( ( u e. CC /\ v e. CC ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u , v >. ) )
48 40 43 47 syl2an 
 |-  ( ( u e. X /\ v e. Y ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u , v >. ) )
49 36 48 impel 
 |-  ( ( z = <. u , v >. /\ ( u e. X /\ v e. Y ) ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) )
50 49 exlimivv 
 |-  ( E. u E. v ( z = <. u , v >. /\ ( u e. X /\ v e. Y ) ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) )
51 30 50 syl 
 |-  ( z e. ( X X. Y ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) )
52 51 eqcomd 
 |-  ( z e. ( X X. Y ) -> ( x. ` z ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) )
53 52 csbeq1d 
 |-  ( z e. ( X X. Y ) -> [_ ( x. ` z ) / i ]_ C = [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C )
54 53 sumeq2i 
 |-  sum_ z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C = sum_ z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C
55 fveq2 
 |-  ( z = <. j , k >. -> ( x. ` z ) = ( x. ` <. j , k >. ) )
56 df-ov 
 |-  ( j x. k ) = ( x. ` <. j , k >. )
57 55 56 eqtr4di 
 |-  ( z = <. j , k >. -> ( x. ` z ) = ( j x. k ) )
58 57 csbeq1d 
 |-  ( z = <. j , k >. -> [_ ( x. ` z ) / i ]_ C = [_ ( j x. k ) / i ]_ C )
59 ovex 
 |-  ( j x. k ) e. _V
60 59 10 csbie 
 |-  [_ ( j x. k ) / i ]_ C = D
61 58 60 eqtrdi 
 |-  ( z = <. j , k >. -> [_ ( x. ` z ) / i ]_ C = D )
62 7 adantrr 
 |-  ( ( ph /\ ( j e. X /\ k e. Y ) ) -> A e. CC )
63 8 adantrl 
 |-  ( ( ph /\ ( j e. X /\ k e. Y ) ) -> B e. CC )
64 62 63 mulcld 
 |-  ( ( ph /\ ( j e. X /\ k e. Y ) ) -> ( A x. B ) e. CC )
65 9 64 eqeltrrd 
 |-  ( ( ph /\ ( j e. X /\ k e. Y ) ) -> D e. CC )
66 61 15 20 65 fsumxp 
 |-  ( ph -> sum_ j e. X sum_ k e. Y D = sum_ z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C )
67 nfcv 
 |-  F/_ w C
68 nfcsb1v 
 |-  F/_ i [_ w / i ]_ C
69 csbeq1a 
 |-  ( i = w -> C = [_ w / i ]_ C )
70 67 68 69 cbvsumi 
 |-  sum_ i e. Z C = sum_ w e. Z [_ w / i ]_ C
71 csbeq1 
 |-  ( w = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) -> [_ w / i ]_ C = [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C )
72 xpfi 
 |-  ( ( X e. Fin /\ Y e. Fin ) -> ( X X. Y ) e. Fin )
73 15 20 72 syl2anc 
 |-  ( ph -> ( X X. Y ) e. Fin )
74 1 2 3 4 5 6 mpodvdsmulf1o 
 |-  ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z )
75 fvres 
 |-  ( z e. ( X X. Y ) -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` z ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) )
76 75 adantl 
 |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` z ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) )
77 65 ralrimivva 
 |-  ( ph -> A. j e. X A. k e. Y D e. CC )
78 61 eleq1d 
 |-  ( z = <. j , k >. -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> D e. CC ) )
79 78 ralxp 
 |-  ( A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC <-> A. j e. X A. k e. Y D e. CC )
80 77 79 sylibr 
 |-  ( ph -> A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC )
81 fveq2 
 |-  ( z = w -> ( x. ` z ) = ( x. ` w ) )
82 81 csbeq1d 
 |-  ( z = w -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C )
83 82 eleq1d 
 |-  ( z = w -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( x. ` w ) / i ]_ C e. CC ) )
84 83 cbvralvw 
 |-  ( A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC <-> A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C e. CC )
85 id 
 |-  ( z e. ( X X. Y ) -> z e. ( X X. Y ) )
86 82 eqcoms 
 |-  ( w = z -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C )
87 86 adantl 
 |-  ( ( z e. ( X X. Y ) /\ w = z ) -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C )
88 87 eleq1d 
 |-  ( ( z e. ( X X. Y ) /\ w = z ) -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( x. ` w ) / i ]_ C e. CC ) )
89 53 eleq1d 
 |-  ( z e. ( X X. Y ) -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) )
90 89 adantr 
 |-  ( ( z e. ( X X. Y ) /\ w = z ) -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) )
91 88 90 bitr3d 
 |-  ( ( z e. ( X X. Y ) /\ w = z ) -> ( [_ ( x. ` w ) / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) )
92 85 91 rspcdv 
 |-  ( z e. ( X X. Y ) -> ( A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C e. CC -> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) )
93 92 com12 
 |-  ( A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C e. CC -> ( z e. ( X X. Y ) -> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) )
94 93 ralrimiv 
 |-  ( A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C e. CC -> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC )
95 84 94 sylbi 
 |-  ( A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC -> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC )
96 80 95 syl 
 |-  ( ph -> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC )
97 mpomulf 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC
98 ffn 
 |-  ( ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC -> ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC ) )
99 97 98 ax-mp 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC )
100 xpss12 
 |-  ( ( X C_ CC /\ Y C_ CC ) -> ( X X. Y ) C_ ( CC X. CC ) )
101 39 42 100 mp2an 
 |-  ( X X. Y ) C_ ( CC X. CC )
102 71 eleq1d 
 |-  ( w = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) -> ( [_ w / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) )
103 102 ralima 
 |-  ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC ) /\ ( X X. Y ) C_ ( CC X. CC ) ) -> ( A. w e. ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) )
104 99 101 103 mp2an 
 |-  ( A. w e. ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC )
105 df-ima 
 |-  ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) = ran ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) )
106 f1ofo 
 |-  ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z )
107 forn 
 |-  ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z -> ran ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) = Z )
108 74 106 107 3syl 
 |-  ( ph -> ran ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) = Z )
109 105 108 eqtrid 
 |-  ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) = Z )
110 109 raleqdv 
 |-  ( ph -> ( A. w e. ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. w e. Z [_ w / i ]_ C e. CC ) )
111 104 110 bitr3id 
 |-  ( ph -> ( A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC <-> A. w e. Z [_ w / i ]_ C e. CC ) )
112 96 111 mpbid 
 |-  ( ph -> A. w e. Z [_ w / i ]_ C e. CC )
113 112 r19.21bi 
 |-  ( ( ph /\ w e. Z ) -> [_ w / i ]_ C e. CC )
114 71 73 74 76 113 fsumf1o 
 |-  ( ph -> sum_ w e. Z [_ w / i ]_ C = sum_ z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C )
115 70 114 eqtrid 
 |-  ( ph -> sum_ i e. Z C = sum_ z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C )
116 54 66 115 3eqtr4a 
 |-  ( ph -> sum_ j e. X sum_ k e. Y D = sum_ i e. Z C )
117 22 29 116 3eqtrd 
 |-  ( ph -> ( sum_ j e. X A x. sum_ k e. Y B ) = sum_ i e. Z C )