Metamath Proof Explorer

Theorem dvdsflsumcom

Description: A sum commutation from sum_ n <_ A , sum_ d || n , B ( n , d ) to sum_ d <_ A , sum_ m <_ A / d , B ( n , d m ) . (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses dvdsflsumcom.1 
|- ( n = ( d x. m ) -> B = C )
dvdsflsumcom.2 
|- ( ph -> A e. RR )
dvdsflsumcom.3 
|- ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> B e. CC )
Assertion dvdsflsumcom 
|- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. { x e. NN | x || n } B = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) C )

Proof

Step Hyp Ref Expression
1 dvdsflsumcom.1 
 |-  ( n = ( d x. m ) -> B = C )
2 dvdsflsumcom.2 
 |-  ( ph -> A e. RR )
3 dvdsflsumcom.3 
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> B e. CC )
4 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` A ) ) e. Fin )
5 fzfid 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... n ) e. Fin )
6 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
7 6 adantl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
8 dvdsssfz1 
 |-  ( n e. NN -> { x e. NN | x || n } C_ ( 1 ... n ) )
9 7 8 syl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> { x e. NN | x || n } C_ ( 1 ... n ) )
10 5 9 ssfid 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> { x e. NN | x || n } e. Fin )
11 nnre 
 |-  ( d e. NN -> d e. RR )
12 11 ad2antrl 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( d e. NN /\ d || n ) ) -> d e. RR )
13 7 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( d e. NN /\ d || n ) ) -> n e. NN )
14 13 nnred 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( d e. NN /\ d || n ) ) -> n e. RR )
15 2 ad2antrr 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( d e. NN /\ d || n ) ) -> A e. RR )
16 nnz 
 |-  ( d e. NN -> d e. ZZ )
17 dvdsle 
 |-  ( ( d e. ZZ /\ n e. NN ) -> ( d || n -> d <_ n ) )
18 16 7 17 syl2anr 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ d e. NN ) -> ( d || n -> d <_ n ) )
19 18 impr 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( d e. NN /\ d || n ) ) -> d <_ n )
20 fznnfl 
 |-  ( A e. RR -> ( n e. ( 1 ... ( |_ ` A ) ) <-> ( n e. NN /\ n <_ A ) ) )
21 2 20 syl 
 |-  ( ph -> ( n e. ( 1 ... ( |_ ` A ) ) <-> ( n e. NN /\ n <_ A ) ) )
22 21 simplbda 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n <_ A )
23 22 adantr 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( d e. NN /\ d || n ) ) -> n <_ A )
24 12 14 15 19 23 letrd 
 |-  ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( d e. NN /\ d || n ) ) -> d <_ A )
25 24 ex 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( d e. NN /\ d || n ) -> d <_ A ) )
26 25 pm4.71rd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( d e. NN /\ d || n ) <-> ( d <_ A /\ ( d e. NN /\ d || n ) ) ) )
27 ancom 
 |-  ( ( d <_ A /\ ( d e. NN /\ d || n ) ) <-> ( ( d e. NN /\ d || n ) /\ d <_ A ) )
28 an32 
 |-  ( ( ( d e. NN /\ d || n ) /\ d <_ A ) <-> ( ( d e. NN /\ d <_ A ) /\ d || n ) )
29 27 28 bitri 
 |-  ( ( d <_ A /\ ( d e. NN /\ d || n ) ) <-> ( ( d e. NN /\ d <_ A ) /\ d || n ) )
30 26 29 bitrdi 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( d e. NN /\ d || n ) <-> ( ( d e. NN /\ d <_ A ) /\ d || n ) ) )
31 fznnfl 
 |-  ( A e. RR -> ( d e. ( 1 ... ( |_ ` A ) ) <-> ( d e. NN /\ d <_ A ) ) )
32 2 31 syl 
 |-  ( ph -> ( d e. ( 1 ... ( |_ ` A ) ) <-> ( d e. NN /\ d <_ A ) ) )
33 32 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( d e. ( 1 ... ( |_ ` A ) ) <-> ( d e. NN /\ d <_ A ) ) )
34 33 anbi1d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( d e. ( 1 ... ( |_ ` A ) ) /\ d || n ) <-> ( ( d e. NN /\ d <_ A ) /\ d || n ) ) )
35 30 34 bitr4d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( d e. NN /\ d || n ) <-> ( d e. ( 1 ... ( |_ ` A ) ) /\ d || n ) ) )
36 35 pm5.32da 
 |-  ( ph -> ( ( n e. ( 1 ... ( |_ ` A ) ) /\ ( d e. NN /\ d || n ) ) <-> ( n e. ( 1 ... ( |_ ` A ) ) /\ ( d e. ( 1 ... ( |_ ` A ) ) /\ d || n ) ) ) )
37 an12 
 |-  ( ( n e. ( 1 ... ( |_ ` A ) ) /\ ( d e. ( 1 ... ( |_ ` A ) ) /\ d || n ) ) <-> ( d e. ( 1 ... ( |_ ` A ) ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d || n ) ) )
38 36 37 bitrdi 
 |-  ( ph -> ( ( n e. ( 1 ... ( |_ ` A ) ) /\ ( d e. NN /\ d || n ) ) <-> ( d e. ( 1 ... ( |_ ` A ) ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d || n ) ) ) )
39 breq1 
 |-  ( x = d -> ( x || n <-> d || n ) )
40 39 elrab 
 |-  ( d e. { x e. NN | x || n } <-> ( d e. NN /\ d || n ) )
41 40 anbi2i 
 |-  ( ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) <-> ( n e. ( 1 ... ( |_ ` A ) ) /\ ( d e. NN /\ d || n ) ) )
42 breq2 
 |-  ( x = n -> ( d || x <-> d || n ) )
43 42 elrab 
 |-  ( n e. { x e. ( 1 ... ( |_ ` A ) ) | d || x } <-> ( n e. ( 1 ... ( |_ ` A ) ) /\ d || n ) )
44 43 anbi2i 
 |-  ( ( d e. ( 1 ... ( |_ ` A ) ) /\ n e. { x e. ( 1 ... ( |_ ` A ) ) | d || x } ) <-> ( d e. ( 1 ... ( |_ ` A ) ) /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d || n ) ) )
45 38 41 44 3bitr4g 
 |-  ( ph -> ( ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) <-> ( d e. ( 1 ... ( |_ ` A ) ) /\ n e. { x e. ( 1 ... ( |_ ` A ) ) | d || x } ) ) )
46 4 4 10 45 3 fsumcom2 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. { x e. NN | x || n } B = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ n e. { x e. ( 1 ... ( |_ ` A ) ) | d || x } B )
47 fzfid 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... ( |_ ` ( A / d ) ) ) e. Fin )
48 2 adantr 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> A e. RR )
49 32 simprbda 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> d e. NN )
50 eqid 
 |-  ( y e. ( 1 ... ( |_ ` ( A / d ) ) ) |-> ( d x. y ) ) = ( y e. ( 1 ... ( |_ ` ( A / d ) ) ) |-> ( d x. y ) )
51 48 49 50 dvdsflf1o 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> ( y e. ( 1 ... ( |_ ` ( A / d ) ) ) |-> ( d x. y ) ) : ( 1 ... ( |_ ` ( A / d ) ) ) -1-1-onto-> { x e. ( 1 ... ( |_ ` A ) ) | d || x } )
52 oveq2 
 |-  ( y = m -> ( d x. y ) = ( d x. m ) )
53 ovex 
 |-  ( d x. m ) e. _V
54 52 50 53 fvmpt 
 |-  ( m e. ( 1 ... ( |_ ` ( A / d ) ) ) -> ( ( y e. ( 1 ... ( |_ ` ( A / d ) ) ) |-> ( d x. y ) ) ` m ) = ( d x. m ) )
55 54 adantl 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ) -> ( ( y e. ( 1 ... ( |_ ` ( A / d ) ) ) |-> ( d x. y ) ) ` m ) = ( d x. m ) )
56 45 biimpar 
 |-  ( ( ph /\ ( d e. ( 1 ... ( |_ ` A ) ) /\ n e. { x e. ( 1 ... ( |_ ` A ) ) | d || x } ) ) -> ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) )
57 56 3 syldan 
 |-  ( ( ph /\ ( d e. ( 1 ... ( |_ ` A ) ) /\ n e. { x e. ( 1 ... ( |_ ` A ) ) | d || x } ) ) -> B e. CC )
58 57 anassrs 
 |-  ( ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) /\ n e. { x e. ( 1 ... ( |_ ` A ) ) | d || x } ) -> B e. CC )
59 1 47 51 55 58 fsumf1o 
 |-  ( ( ph /\ d e. ( 1 ... ( |_ ` A ) ) ) -> sum_ n e. { x e. ( 1 ... ( |_ ` A ) ) | d || x } B = sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) C )
60 59 sumeq2dv 
 |-  ( ph -> sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ n e. { x e. ( 1 ... ( |_ ` A ) ) | d || x } B = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) C )
61 46 60 eqtrd 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. { x e. NN | x || n } B = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) C )