Metamath Proof Explorer

Theorem fsumdvdscom

Description: A double commutation of divisor sums based on fsumdvdsdiag . Note that A depends on both j and k . (Contributed by Mario Carneiro, 13-May-2016)

Ref Expression
Hypotheses fsumdvdscom.1 
|- ( ph -> N e. NN )
fsumdvdscom.2 
|- ( j = ( k x. m ) -> A = B )
fsumdvdscom.3 
|- ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || j } ) ) -> A e. CC )
Assertion fsumdvdscom 
|- ( ph -> sum_ j e. { x e. NN | x || N } sum_ k e. { x e. NN | x || j } A = sum_ k e. { x e. NN | x || N } sum_ m e. { x e. NN | x || ( N / k ) } B )

Proof

Step Hyp Ref Expression
1 fsumdvdscom.1 
 |-  ( ph -> N e. NN )
2 fsumdvdscom.2 
 |-  ( j = ( k x. m ) -> A = B )
3 fsumdvdscom.3 
 |-  ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || j } ) ) -> A e. CC )
4 nfcv 
 |-  F/_ u sum_ k e. { x e. NN | x || j } A
5 nfcv 
 |-  F/_ j { x e. NN | x || u }
6 nfcsb1v 
 |-  F/_ j [_ u / j ]_ A
7 5 6 nfsum 
 |-  F/_ j sum_ k e. { x e. NN | x || u } [_ u / j ]_ A
8 breq2 
 |-  ( j = u -> ( x || j <-> x || u ) )
9 8 rabbidv 
 |-  ( j = u -> { x e. NN | x || j } = { x e. NN | x || u } )
10 csbeq1a 
 |-  ( j = u -> A = [_ u / j ]_ A )
11 10 adantr 
 |-  ( ( j = u /\ k e. { x e. NN | x || j } ) -> A = [_ u / j ]_ A )
12 9 11 sumeq12dv 
 |-  ( j = u -> sum_ k e. { x e. NN | x || j } A = sum_ k e. { x e. NN | x || u } [_ u / j ]_ A )
13 4 7 12 cbvsumi 
 |-  sum_ j e. { x e. NN | x || N } sum_ k e. { x e. NN | x || j } A = sum_ u e. { x e. NN | x || N } sum_ k e. { x e. NN | x || u } [_ u / j ]_ A
14 breq2 
 |-  ( u = ( N / v ) -> ( x || u <-> x || ( N / v ) ) )
15 14 rabbidv 
 |-  ( u = ( N / v ) -> { x e. NN | x || u } = { x e. NN | x || ( N / v ) } )
16 csbeq1 
 |-  ( u = ( N / v ) -> [_ u / j ]_ A = [_ ( N / v ) / j ]_ A )
17 16 adantr 
 |-  ( ( u = ( N / v ) /\ k e. { x e. NN | x || u } ) -> [_ u / j ]_ A = [_ ( N / v ) / j ]_ A )
18 15 17 sumeq12dv 
 |-  ( u = ( N / v ) -> sum_ k e. { x e. NN | x || u } [_ u / j ]_ A = sum_ k e. { x e. NN | x || ( N / v ) } [_ ( N / v ) / j ]_ A )
19 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
20 dvdsssfz1 
 |-  ( N e. NN -> { x e. NN | x || N } C_ ( 1 ... N ) )
21 1 20 syl 
 |-  ( ph -> { x e. NN | x || N } C_ ( 1 ... N ) )
22 19 21 ssfid 
 |-  ( ph -> { x e. NN | x || N } e. Fin )
23 eqid 
 |-  { x e. NN | x || N } = { x e. NN | x || N }
24 eqid 
 |-  ( z e. { x e. NN | x || N } |-> ( N / z ) ) = ( z e. { x e. NN | x || N } |-> ( N / z ) )
25 23 24 dvdsflip 
 |-  ( N e. NN -> ( z e. { x e. NN | x || N } |-> ( N / z ) ) : { x e. NN | x || N } -1-1-onto-> { x e. NN | x || N } )
26 1 25 syl 
 |-  ( ph -> ( z e. { x e. NN | x || N } |-> ( N / z ) ) : { x e. NN | x || N } -1-1-onto-> { x e. NN | x || N } )
27 oveq2 
 |-  ( z = v -> ( N / z ) = ( N / v ) )
28 ovex 
 |-  ( N / z ) e. _V
29 27 24 28 fvmpt3i 
 |-  ( v e. { x e. NN | x || N } -> ( ( z e. { x e. NN | x || N } |-> ( N / z ) ) ` v ) = ( N / v ) )
30 29 adantl 
 |-  ( ( ph /\ v e. { x e. NN | x || N } ) -> ( ( z e. { x e. NN | x || N } |-> ( N / z ) ) ` v ) = ( N / v ) )
31 fzfid 
 |-  ( ( ph /\ u e. { x e. NN | x || N } ) -> ( 1 ... u ) e. Fin )
32 ssrab2 
 |-  { x e. NN | x || N } C_ NN
33 simpr 
 |-  ( ( ph /\ u e. { x e. NN | x || N } ) -> u e. { x e. NN | x || N } )
34 32 33 sseldi 
 |-  ( ( ph /\ u e. { x e. NN | x || N } ) -> u e. NN )
35 dvdsssfz1 
 |-  ( u e. NN -> { x e. NN | x || u } C_ ( 1 ... u ) )
36 34 35 syl 
 |-  ( ( ph /\ u e. { x e. NN | x || N } ) -> { x e. NN | x || u } C_ ( 1 ... u ) )
37 31 36 ssfid 
 |-  ( ( ph /\ u e. { x e. NN | x || N } ) -> { x e. NN | x || u } e. Fin )
38 3 ralrimivva 
 |-  ( ph -> A. j e. { x e. NN | x || N } A. k e. { x e. NN | x || j } A e. CC )
39 nfv 
 |-  F/ u A. k e. { x e. NN | x || j } A e. CC
40 6 nfel1 
 |-  F/ j [_ u / j ]_ A e. CC
41 5 40 nfralw 
 |-  F/ j A. k e. { x e. NN | x || u } [_ u / j ]_ A e. CC
42 10 eleq1d 
 |-  ( j = u -> ( A e. CC <-> [_ u / j ]_ A e. CC ) )
43 9 42 raleqbidv 
 |-  ( j = u -> ( A. k e. { x e. NN | x || j } A e. CC <-> A. k e. { x e. NN | x || u } [_ u / j ]_ A e. CC ) )
44 39 41 43 cbvralw 
 |-  ( A. j e. { x e. NN | x || N } A. k e. { x e. NN | x || j } A e. CC <-> A. u e. { x e. NN | x || N } A. k e. { x e. NN | x || u } [_ u / j ]_ A e. CC )
45 38 44 sylib 
 |-  ( ph -> A. u e. { x e. NN | x || N } A. k e. { x e. NN | x || u } [_ u / j ]_ A e. CC )
46 45 r19.21bi 
 |-  ( ( ph /\ u e. { x e. NN | x || N } ) -> A. k e. { x e. NN | x || u } [_ u / j ]_ A e. CC )
47 46 r19.21bi 
 |-  ( ( ( ph /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || u } ) -> [_ u / j ]_ A e. CC )
48 37 47 fsumcl 
 |-  ( ( ph /\ u e. { x e. NN | x || N } ) -> sum_ k e. { x e. NN | x || u } [_ u / j ]_ A e. CC )
49 18 22 26 30 48 fsumf1o 
 |-  ( ph -> sum_ u e. { x e. NN | x || N } sum_ k e. { x e. NN | x || u } [_ u / j ]_ A = sum_ v e. { x e. NN | x || N } sum_ k e. { x e. NN | x || ( N / v ) } [_ ( N / v ) / j ]_ A )
50 16 eleq1d 
 |-  ( u = ( N / v ) -> ( [_ u / j ]_ A e. CC <-> [_ ( N / v ) / j ]_ A e. CC ) )
51 15 50 raleqbidv 
 |-  ( u = ( N / v ) -> ( A. k e. { x e. NN | x || u } [_ u / j ]_ A e. CC <-> A. k e. { x e. NN | x || ( N / v ) } [_ ( N / v ) / j ]_ A e. CC ) )
52 45 adantr 
 |-  ( ( ph /\ v e. { x e. NN | x || N } ) -> A. u e. { x e. NN | x || N } A. k e. { x e. NN | x || u } [_ u / j ]_ A e. CC )
53 dvdsdivcl 
 |-  ( ( N e. NN /\ v e. { x e. NN | x || N } ) -> ( N / v ) e. { x e. NN | x || N } )
54 1 53 sylan 
 |-  ( ( ph /\ v e. { x e. NN | x || N } ) -> ( N / v ) e. { x e. NN | x || N } )
55 51 52 54 rspcdva 
 |-  ( ( ph /\ v e. { x e. NN | x || N } ) -> A. k e. { x e. NN | x || ( N / v ) } [_ ( N / v ) / j ]_ A e. CC )
56 55 r19.21bi 
 |-  ( ( ( ph /\ v e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / v ) } ) -> [_ ( N / v ) / j ]_ A e. CC )
57 56 anasss 
 |-  ( ( ph /\ ( v e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / v ) } ) ) -> [_ ( N / v ) / j ]_ A e. CC )
58 1 57 fsumdvdsdiag 
 |-  ( ph -> sum_ v e. { x e. NN | x || N } sum_ k e. { x e. NN | x || ( N / v ) } [_ ( N / v ) / j ]_ A = sum_ k e. { x e. NN | x || N } sum_ v e. { x e. NN | x || ( N / k ) } [_ ( N / v ) / j ]_ A )
59 oveq2 
 |-  ( v = ( ( N / k ) / m ) -> ( N / v ) = ( N / ( ( N / k ) / m ) ) )
60 59 csbeq1d 
 |-  ( v = ( ( N / k ) / m ) -> [_ ( N / v ) / j ]_ A = [_ ( N / ( ( N / k ) / m ) ) / j ]_ A )
61 fzfid 
 |-  ( ( ph /\ k e. { x e. NN | x || N } ) -> ( 1 ... ( N / k ) ) e. Fin )
62 dvdsdivcl 
 |-  ( ( N e. NN /\ k e. { x e. NN | x || N } ) -> ( N / k ) e. { x e. NN | x || N } )
63 32 62 sseldi 
 |-  ( ( N e. NN /\ k e. { x e. NN | x || N } ) -> ( N / k ) e. NN )
64 1 63 sylan 
 |-  ( ( ph /\ k e. { x e. NN | x || N } ) -> ( N / k ) e. NN )
65 dvdsssfz1 
 |-  ( ( N / k ) e. NN -> { x e. NN | x || ( N / k ) } C_ ( 1 ... ( N / k ) ) )
66 64 65 syl 
 |-  ( ( ph /\ k e. { x e. NN | x || N } ) -> { x e. NN | x || ( N / k ) } C_ ( 1 ... ( N / k ) ) )
67 61 66 ssfid 
 |-  ( ( ph /\ k e. { x e. NN | x || N } ) -> { x e. NN | x || ( N / k ) } e. Fin )
68 eqid 
 |-  { x e. NN | x || ( N / k ) } = { x e. NN | x || ( N / k ) }
69 eqid 
 |-  ( z e. { x e. NN | x || ( N / k ) } |-> ( ( N / k ) / z ) ) = ( z e. { x e. NN | x || ( N / k ) } |-> ( ( N / k ) / z ) )
70 68 69 dvdsflip 
 |-  ( ( N / k ) e. NN -> ( z e. { x e. NN | x || ( N / k ) } |-> ( ( N / k ) / z ) ) : { x e. NN | x || ( N / k ) } -1-1-onto-> { x e. NN | x || ( N / k ) } )
71 64 70 syl 
 |-  ( ( ph /\ k e. { x e. NN | x || N } ) -> ( z e. { x e. NN | x || ( N / k ) } |-> ( ( N / k ) / z ) ) : { x e. NN | x || ( N / k ) } -1-1-onto-> { x e. NN | x || ( N / k ) } )
72 oveq2 
 |-  ( z = m -> ( ( N / k ) / z ) = ( ( N / k ) / m ) )
73 ovex 
 |-  ( ( N / k ) / z ) e. _V
74 72 69 73 fvmpt3i 
 |-  ( m e. { x e. NN | x || ( N / k ) } -> ( ( z e. { x e. NN | x || ( N / k ) } |-> ( ( N / k ) / z ) ) ` m ) = ( ( N / k ) / m ) )
75 74 adantl 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( ( z e. { x e. NN | x || ( N / k ) } |-> ( ( N / k ) / z ) ) ` m ) = ( ( N / k ) / m ) )
76 1 fsumdvdsdiaglem 
 |-  ( ph -> ( ( k e. { x e. NN | x || N } /\ v e. { x e. NN | x || ( N / k ) } ) -> ( v e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / v ) } ) ) )
77 57 ex 
 |-  ( ph -> ( ( v e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / v ) } ) -> [_ ( N / v ) / j ]_ A e. CC ) )
78 76 77 syld 
 |-  ( ph -> ( ( k e. { x e. NN | x || N } /\ v e. { x e. NN | x || ( N / k ) } ) -> [_ ( N / v ) / j ]_ A e. CC ) )
79 78 impl 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ v e. { x e. NN | x || ( N / k ) } ) -> [_ ( N / v ) / j ]_ A e. CC )
80 60 67 71 75 79 fsumf1o 
 |-  ( ( ph /\ k e. { x e. NN | x || N } ) -> sum_ v e. { x e. NN | x || ( N / k ) } [_ ( N / v ) / j ]_ A = sum_ m e. { x e. NN | x || ( N / k ) } [_ ( N / ( ( N / k ) / m ) ) / j ]_ A )
81 ovexd 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( N / ( ( N / k ) / m ) ) e. _V )
82 nncn 
 |-  ( N e. NN -> N e. CC )
83 nnne0 
 |-  ( N e. NN -> N =/= 0 )
84 82 83 jca 
 |-  ( N e. NN -> ( N e. CC /\ N =/= 0 ) )
85 1 84 syl 
 |-  ( ph -> ( N e. CC /\ N =/= 0 ) )
86 85 ad2antrr 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( N e. CC /\ N =/= 0 ) )
87 86 simpld 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> N e. CC )
88 elrabi 
 |-  ( k e. { x e. NN | x || N } -> k e. NN )
89 88 adantl 
 |-  ( ( ph /\ k e. { x e. NN | x || N } ) -> k e. NN )
90 89 adantr 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> k e. NN )
91 nncn 
 |-  ( k e. NN -> k e. CC )
92 nnne0 
 |-  ( k e. NN -> k =/= 0 )
93 91 92 jca 
 |-  ( k e. NN -> ( k e. CC /\ k =/= 0 ) )
94 90 93 syl 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( k e. CC /\ k =/= 0 ) )
95 elrabi 
 |-  ( m e. { x e. NN | x || ( N / k ) } -> m e. NN )
96 95 adantl 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> m e. NN )
97 nncn 
 |-  ( m e. NN -> m e. CC )
98 nnne0 
 |-  ( m e. NN -> m =/= 0 )
99 97 98 jca 
 |-  ( m e. NN -> ( m e. CC /\ m =/= 0 ) )
100 96 99 syl 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( m e. CC /\ m =/= 0 ) )
101 divdiv1 
 |-  ( ( N e. CC /\ ( k e. CC /\ k =/= 0 ) /\ ( m e. CC /\ m =/= 0 ) ) -> ( ( N / k ) / m ) = ( N / ( k x. m ) ) )
102 87 94 100 101 syl3anc 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( ( N / k ) / m ) = ( N / ( k x. m ) ) )
103 102 oveq2d 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( N / ( ( N / k ) / m ) ) = ( N / ( N / ( k x. m ) ) ) )
104 nnmulcl 
 |-  ( ( k e. NN /\ m e. NN ) -> ( k x. m ) e. NN )
105 89 95 104 syl2an 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( k x. m ) e. NN )
106 nncn 
 |-  ( ( k x. m ) e. NN -> ( k x. m ) e. CC )
107 nnne0 
 |-  ( ( k x. m ) e. NN -> ( k x. m ) =/= 0 )
108 106 107 jca 
 |-  ( ( k x. m ) e. NN -> ( ( k x. m ) e. CC /\ ( k x. m ) =/= 0 ) )
109 105 108 syl 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( ( k x. m ) e. CC /\ ( k x. m ) =/= 0 ) )
110 ddcan 
 |-  ( ( ( N e. CC /\ N =/= 0 ) /\ ( ( k x. m ) e. CC /\ ( k x. m ) =/= 0 ) ) -> ( N / ( N / ( k x. m ) ) ) = ( k x. m ) )
111 86 109 110 syl2anc 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( N / ( N / ( k x. m ) ) ) = ( k x. m ) )
112 103 111 eqtrd 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( N / ( ( N / k ) / m ) ) = ( k x. m ) )
113 112 eqeq2d 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> ( j = ( N / ( ( N / k ) / m ) ) <-> j = ( k x. m ) ) )
114 113 biimpa 
 |-  ( ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) /\ j = ( N / ( ( N / k ) / m ) ) ) -> j = ( k x. m ) )
115 114 2 syl 
 |-  ( ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) /\ j = ( N / ( ( N / k ) / m ) ) ) -> A = B )
116 81 115 csbied 
 |-  ( ( ( ph /\ k e. { x e. NN | x || N } ) /\ m e. { x e. NN | x || ( N / k ) } ) -> [_ ( N / ( ( N / k ) / m ) ) / j ]_ A = B )
117 116 sumeq2dv 
 |-  ( ( ph /\ k e. { x e. NN | x || N } ) -> sum_ m e. { x e. NN | x || ( N / k ) } [_ ( N / ( ( N / k ) / m ) ) / j ]_ A = sum_ m e. { x e. NN | x || ( N / k ) } B )
118 80 117 eqtrd 
 |-  ( ( ph /\ k e. { x e. NN | x || N } ) -> sum_ v e. { x e. NN | x || ( N / k ) } [_ ( N / v ) / j ]_ A = sum_ m e. { x e. NN | x || ( N / k ) } B )
119 118 sumeq2dv 
 |-  ( ph -> sum_ k e. { x e. NN | x || N } sum_ v e. { x e. NN | x || ( N / k ) } [_ ( N / v ) / j ]_ A = sum_ k e. { x e. NN | x || N } sum_ m e. { x e. NN | x || ( N / k ) } B )
120 49 58 119 3eqtrd 
 |-  ( ph -> sum_ u e. { x e. NN | x || N } sum_ k e. { x e. NN | x || u } [_ u / j ]_ A = sum_ k e. { x e. NN | x || N } sum_ m e. { x e. NN | x || ( N / k ) } B )
121 13 120 syl5eq 
 |-  ( ph -> sum_ j e. { x e. NN | x || N } sum_ k e. { x e. NN | x || j } A = sum_ k e. { x e. NN | x || N } sum_ m e. { x e. NN | x || ( N / k ) } B )