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 )