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 
|- ( ph -> M e. NN )
dvdsmulf1o.2 
|- ( ph -> N e. NN )
dvdsmulf1o.3 
|- ( ph -> ( M gcd N ) = 1 )
dvdsmulf1o.x 
|- X = { x e. NN | x || M }
dvdsmulf1o.y 
|- Y = { x e. NN | x || N }
dvdsmulf1o.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 dvdsmulf1o.1 
 |-  ( ph -> M e. NN )
2 dvdsmulf1o.2 
 |-  ( ph -> N e. NN )
3 dvdsmulf1o.3 
 |-  ( ph -> ( M gcd N ) = 1 )
4 dvdsmulf1o.x 
 |-  X = { x e. NN | x || M }
5 dvdsmulf1o.y 
 |-  Y = { x e. NN | x || N }
6 dvdsmulf1o.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 fveq2 
 |-  ( z = <. j , k >. -> ( x. ` z ) = ( x. ` <. j , k >. ) )
31 df-ov 
 |-  ( j x. k ) = ( x. ` <. j , k >. )
32 30 31 eqtr4di 
 |-  ( z = <. j , k >. -> ( x. ` z ) = ( j x. k ) )
33 32 csbeq1d 
 |-  ( z = <. j , k >. -> [_ ( x. ` z ) / i ]_ C = [_ ( j x. k ) / i ]_ C )
34 ovex 
 |-  ( j x. k ) e. _V
35 34 10 csbie 
 |-  [_ ( j x. k ) / i ]_ C = D
36 33 35 eqtrdi 
 |-  ( z = <. j , k >. -> [_ ( x. ` z ) / i ]_ C = D )
37 7 adantrr 
 |-  ( ( ph /\ ( j e. X /\ k e. Y ) ) -> A e. CC )
38 8 adantrl 
 |-  ( ( ph /\ ( j e. X /\ k e. Y ) ) -> B e. CC )
39 37 38 mulcld 
 |-  ( ( ph /\ ( j e. X /\ k e. Y ) ) -> ( A x. B ) e. CC )
40 9 39 eqeltrrd 
 |-  ( ( ph /\ ( j e. X /\ k e. Y ) ) -> D e. CC )
41 36 15 20 40 fsumxp 
 |-  ( ph -> sum_ j e. X sum_ k e. Y D = sum_ z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C )
42 nfcv 
 |-  F/_ w C
43 nfcsb1v 
 |-  F/_ i [_ w / i ]_ C
44 csbeq1a 
 |-  ( i = w -> C = [_ w / i ]_ C )
45 42 43 44 cbvsumi 
 |-  sum_ i e. Z C = sum_ w e. Z [_ w / i ]_ C
46 csbeq1 
 |-  ( w = ( x. ` z ) -> [_ w / i ]_ C = [_ ( x. ` z ) / i ]_ C )
47 xpfi 
 |-  ( ( X e. Fin /\ Y e. Fin ) -> ( X X. Y ) e. Fin )
48 15 20 47 syl2anc 
 |-  ( ph -> ( X X. Y ) e. Fin )
49 1 2 3 4 5 6 dvdsmulf1o 
 |-  ( ph -> ( x. |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z )
50 fvres 
 |-  ( z e. ( X X. Y ) -> ( ( x. |` ( X X. Y ) ) ` z ) = ( x. ` z ) )
51 50 adantl 
 |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( ( x. |` ( X X. Y ) ) ` z ) = ( x. ` z ) )
52 40 ralrimivva 
 |-  ( ph -> A. j e. X A. k e. Y D e. CC )
53 36 eleq1d 
 |-  ( z = <. j , k >. -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> D e. CC ) )
54 53 ralxp 
 |-  ( A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC <-> A. j e. X A. k e. Y D e. CC )
55 52 54 sylibr 
 |-  ( ph -> A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC )
56 ax-mulf 
 |-  x. : ( CC X. CC ) --> CC
57 ffn 
 |-  ( x. : ( CC X. CC ) --> CC -> x. Fn ( CC X. CC ) )
58 56 57 ax-mp 
 |-  x. Fn ( CC X. CC )
59 4 ssrab3 
 |-  X C_ NN
60 nnsscn 
 |-  NN C_ CC
61 59 60 sstri 
 |-  X C_ CC
62 5 ssrab3 
 |-  Y C_ NN
63 62 60 sstri 
 |-  Y C_ CC
64 xpss12 
 |-  ( ( X C_ CC /\ Y C_ CC ) -> ( X X. Y ) C_ ( CC X. CC ) )
65 61 63 64 mp2an 
 |-  ( X X. Y ) C_ ( CC X. CC )
66 46 eleq1d 
 |-  ( w = ( x. ` z ) -> ( [_ w / i ]_ C e. CC <-> [_ ( x. ` z ) / i ]_ C e. CC ) )
67 66 ralima 
 |-  ( ( x. Fn ( CC X. CC ) /\ ( X X. Y ) C_ ( CC X. CC ) ) -> ( A. w e. ( x. " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC ) )
68 58 65 67 mp2an 
 |-  ( A. w e. ( x. " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC )
69 df-ima 
 |-  ( x. " ( X X. Y ) ) = ran ( x. |` ( X X. Y ) )
70 f1ofo 
 |-  ( ( x. |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z -> ( x. |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z )
71 forn 
 |-  ( ( x. |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z -> ran ( x. |` ( X X. Y ) ) = Z )
72 49 70 71 3syl 
 |-  ( ph -> ran ( x. |` ( X X. Y ) ) = Z )
73 69 72 syl5eq 
 |-  ( ph -> ( x. " ( X X. Y ) ) = Z )
74 73 raleqdv 
 |-  ( ph -> ( A. w e. ( x. " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. w e. Z [_ w / i ]_ C e. CC ) )
75 68 74 bitr3id 
 |-  ( ph -> ( A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC <-> A. w e. Z [_ w / i ]_ C e. CC ) )
76 55 75 mpbid 
 |-  ( ph -> A. w e. Z [_ w / i ]_ C e. CC )
77 76 r19.21bi 
 |-  ( ( ph /\ w e. Z ) -> [_ w / i ]_ C e. CC )
78 46 48 49 51 77 fsumf1o 
 |-  ( ph -> sum_ w e. Z [_ w / i ]_ C = sum_ z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C )
79 45 78 syl5eq 
 |-  ( ph -> sum_ i e. Z C = sum_ z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C )
80 41 79 eqtr4d 
 |-  ( ph -> sum_ j e. X sum_ k e. Y D = sum_ i e. Z C )
81 22 29 80 3eqtrd 
 |-  ( ph -> ( sum_ j e. X A x. sum_ k e. Y B ) = sum_ i e. Z C )