Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . 3
โข (๐ โ (1...(โโ๐ด)) โ Fin) |
2 | | fzfid 13885 |
. . . 4
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ (1...๐) โ Fin) |
3 | | elfznn 13477 |
. . . . . 6
โข (๐ โ
(1...(โโ๐ด))
โ ๐ โ
โ) |
4 | 3 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ๐ โ โ) |
5 | | dvdsssfz1 16207 |
. . . . 5
โข (๐ โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (1...๐)) |
6 | 4, 5 | syl 17 |
. . . 4
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (1...๐)) |
7 | 2, 6 | ssfid 9218 |
. . 3
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ Fin) |
8 | | nnre 12167 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
9 | 8 | ad2antrl 727 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ) |
10 | 4 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ) |
11 | 10 | nnred 12175 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โ โ) |
12 | | dvdsflsumcom.2 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ด โ โ) |
14 | | nnz 12527 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โค) |
15 | | dvdsle 16199 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ ๐ โ ๐ โค ๐)) |
16 | 14, 4, 15 | syl2anr 598 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง ๐ โ โ) โ (๐ โฅ ๐ โ ๐ โค ๐)) |
17 | 16 | impr 456 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โค ๐) |
18 | | fznnfl 13774 |
. . . . . . . . . . . . . 14
โข (๐ด โ โ โ (๐ โ
(1...(โโ๐ด))
โ (๐ โ โ
โง ๐ โค ๐ด))) |
19 | 12, 18 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ (1...(โโ๐ด)) โ (๐ โ โ โง ๐ โค ๐ด))) |
20 | 19 | simplbda 501 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ๐ โค ๐ด) |
21 | 20 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โค ๐ด) |
22 | 9, 11, 13, 17, 21 | letrd 11319 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง (๐ โ โ โง ๐ โฅ ๐)) โ ๐ โค ๐ด) |
23 | 22 | ex 414 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ((๐ โ โ โง ๐ โฅ ๐) โ ๐ โค ๐ด)) |
24 | 23 | pm4.71rd 564 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ((๐ โ โ โง ๐ โฅ ๐) โ (๐ โค ๐ด โง (๐ โ โ โง ๐ โฅ ๐)))) |
25 | | ancom 462 |
. . . . . . . . 9
โข ((๐ โค ๐ด โง (๐ โ โ โง ๐ โฅ ๐)) โ ((๐ โ โ โง ๐ โฅ ๐) โง ๐ โค ๐ด)) |
26 | | an32 645 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โฅ ๐) โง ๐ โค ๐ด) โ ((๐ โ โ โง ๐ โค ๐ด) โง ๐ โฅ ๐)) |
27 | 25, 26 | bitri 275 |
. . . . . . . 8
โข ((๐ โค ๐ด โง (๐ โ โ โง ๐ โฅ ๐)) โ ((๐ โ โ โง ๐ โค ๐ด) โง ๐ โฅ ๐)) |
28 | 24, 27 | bitrdi 287 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ((๐ โ โ โง ๐ โฅ ๐) โ ((๐ โ โ โง ๐ โค ๐ด) โง ๐ โฅ ๐))) |
29 | | fznnfl 13774 |
. . . . . . . . . 10
โข (๐ด โ โ โ (๐ โ
(1...(โโ๐ด))
โ (๐ โ โ
โง ๐ โค ๐ด))) |
30 | 12, 29 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ โ (1...(โโ๐ด)) โ (๐ โ โ โง ๐ โค ๐ด))) |
31 | 30 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ (๐ โ (1...(โโ๐ด)) โ (๐ โ โ โง ๐ โค ๐ด))) |
32 | 31 | anbi1d 631 |
. . . . . . 7
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ((๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐) โ ((๐ โ โ โง ๐ โค ๐ด) โง ๐ โฅ ๐))) |
33 | 28, 32 | bitr4d 282 |
. . . . . 6
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ((๐ โ โ โง ๐ โฅ ๐) โ (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐))) |
34 | 33 | pm5.32da 580 |
. . . . 5
โข (๐ โ ((๐ โ (1...(โโ๐ด)) โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ โ (1...(โโ๐ด)) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)))) |
35 | | an12 644 |
. . . . 5
โข ((๐ โ
(1...(โโ๐ด))
โง (๐ โ
(1...(โโ๐ด))
โง ๐ โฅ ๐)) โ (๐ โ (1...(โโ๐ด)) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐))) |
36 | 34, 35 | bitrdi 287 |
. . . 4
โข (๐ โ ((๐ โ (1...(โโ๐ด)) โง (๐ โ โ โง ๐ โฅ ๐)) โ (๐ โ (1...(โโ๐ด)) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)))) |
37 | | breq1 5113 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฅ โฅ ๐ โ ๐ โฅ ๐)) |
38 | 37 | elrab 3650 |
. . . . 5
โข (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} โ (๐ โ โ โง ๐ โฅ ๐)) |
39 | 38 | anbi2i 624 |
. . . 4
โข ((๐ โ
(1...(โโ๐ด))
โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ โ (1...(โโ๐ด)) โง (๐ โ โ โง ๐ โฅ ๐))) |
40 | | breq2 5114 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐)) |
41 | 40 | elrab 3650 |
. . . . 5
โข (๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ} โ (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐)) |
42 | 41 | anbi2i 624 |
. . . 4
โข ((๐ โ
(1...(โโ๐ด))
โง ๐ โ {๐ฅ โ
(1...(โโ๐ด))
โฃ ๐ โฅ ๐ฅ}) โ (๐ โ (1...(โโ๐ด)) โง (๐ โ (1...(โโ๐ด)) โง ๐ โฅ ๐))) |
43 | 36, 39, 42 | 3bitr4g 314 |
. . 3
โข (๐ โ ((๐ โ (1...(โโ๐ด)) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}) โ (๐ โ (1...(โโ๐ด)) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}))) |
44 | | dvdsflsumcom.3 |
. . 3
โข ((๐ โง (๐ โ (1...(โโ๐ด)) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) โ ๐ต โ โ) |
45 | 1, 1, 7, 43, 44 | fsumcom2 15666 |
. 2
โข (๐ โ ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ต = ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}๐ต) |
46 | | dvdsflsumcom.1 |
. . . 4
โข (๐ = (๐ ยท ๐) โ ๐ต = ๐ถ) |
47 | | fzfid 13885 |
. . . 4
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ (1...(โโ(๐ด / ๐))) โ Fin) |
48 | 12 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ๐ด โ โ) |
49 | 30 | simprbda 500 |
. . . . 5
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ๐ โ โ) |
50 | | eqid 2737 |
. . . . 5
โข (๐ฆ โ
(1...(โโ(๐ด /
๐))) โฆ (๐ ยท ๐ฆ)) = (๐ฆ โ (1...(โโ(๐ด / ๐))) โฆ (๐ ยท ๐ฆ)) |
51 | 48, 49, 50 | dvdsflf1o 26552 |
. . . 4
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ (๐ฆ โ (1...(โโ(๐ด / ๐))) โฆ (๐ ยท ๐ฆ)):(1...(โโ(๐ด / ๐)))โ1-1-ontoโ{๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) |
52 | | oveq2 7370 |
. . . . . 6
โข (๐ฆ = ๐ โ (๐ ยท ๐ฆ) = (๐ ยท ๐)) |
53 | | ovex 7395 |
. . . . . 6
โข (๐ ยท ๐) โ V |
54 | 52, 50, 53 | fvmpt 6953 |
. . . . 5
โข (๐ โ
(1...(โโ(๐ด /
๐))) โ ((๐ฆ โ
(1...(โโ(๐ด /
๐))) โฆ (๐ ยท ๐ฆ))โ๐) = (๐ ยท ๐)) |
55 | 54 | adantl 483 |
. . . 4
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง ๐ โ (1...(โโ(๐ด / ๐)))) โ ((๐ฆ โ (1...(โโ(๐ด / ๐))) โฆ (๐ ยท ๐ฆ))โ๐) = (๐ ยท ๐)) |
56 | 43 | biimpar 479 |
. . . . . 6
โข ((๐ โง (๐ โ (1...(โโ๐ด)) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ})) โ (๐ โ (1...(โโ๐ด)) โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐})) |
57 | 56, 44 | syldan 592 |
. . . . 5
โข ((๐ โง (๐ โ (1...(โโ๐ด)) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ})) โ ๐ต โ โ) |
58 | 57 | anassrs 469 |
. . . 4
โข (((๐ โง ๐ โ (1...(โโ๐ด))) โง ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}) โ ๐ต โ โ) |
59 | 46, 47, 51, 55, 58 | fsumf1o 15615 |
. . 3
โข ((๐ โง ๐ โ (1...(โโ๐ด))) โ ฮฃ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}๐ต = ฮฃ๐ โ (1...(โโ(๐ด / ๐)))๐ถ) |
60 | 59 | sumeq2dv 15595 |
. 2
โข (๐ โ ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ {๐ฅ โ (1...(โโ๐ด)) โฃ ๐ โฅ ๐ฅ}๐ต = ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ (1...(โโ(๐ด / ๐)))๐ถ) |
61 | 45, 60 | eqtrd 2777 |
1
โข (๐ โ ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐}๐ต = ฮฃ๐ โ (1...(โโ๐ด))ฮฃ๐ โ (1...(โโ(๐ด / ๐)))๐ถ) |