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 ) |