Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . 3
โข (๐ = (๐โ๐) โ (ฮโ๐) = (ฮโ(๐โ๐))) |
2 | | fzfid 13937 |
. . . 4
โข (๐ด โ โ โ
(1...๐ด) โ
Fin) |
3 | | dvdsssfz1 16260 |
. . . 4
โข (๐ด โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด} โ (1...๐ด)) |
4 | 2, 3 | ssfid 9266 |
. . 3
โข (๐ด โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด} โ Fin) |
5 | | ssrab2 4077 |
. . . 4
โข {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด} โ โ |
6 | 5 | a1i 11 |
. . 3
โข (๐ด โ โ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด} โ โ) |
7 | | inss1 4228 |
. . . 4
โข
((1...๐ด) โฉ
โ) โ (1...๐ด) |
8 | | ssfi 9172 |
. . . 4
โข
(((1...๐ด) โ Fin
โง ((1...๐ด) โฉ
โ) โ (1...๐ด))
โ ((1...๐ด) โฉ
โ) โ Fin) |
9 | 2, 7, 8 | sylancl 586 |
. . 3
โข (๐ด โ โ โ
((1...๐ด) โฉ โ)
โ Fin) |
10 | | pccl 16781 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ด โ โ) โ (๐ pCnt ๐ด) โ
โ0) |
11 | 10 | ancoms 459 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ pCnt ๐ด) โ
โ0) |
12 | 11 | nn0zd 12583 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ pCnt ๐ด) โ โค) |
13 | | fznn 13568 |
. . . . . . . 8
โข ((๐ pCnt ๐ด) โ โค โ (๐ โ (1...(๐ pCnt ๐ด)) โ (๐ โ โ โง ๐ โค (๐ pCnt ๐ด)))) |
14 | 12, 13 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ โ (1...(๐ pCnt ๐ด)) โ (๐ โ โ โง ๐ โค (๐ pCnt ๐ด)))) |
15 | 14 | anbi2d 629 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ โ (1...๐ด) โง ๐ โ (1...(๐ pCnt ๐ด))) โ (๐ โ (1...๐ด) โง (๐ โ โ โง ๐ โค (๐ pCnt ๐ด))))) |
16 | | an12 643 |
. . . . . . 7
โข ((๐ โ (1...๐ด) โง (๐ โ โ โง ๐ โค (๐ pCnt ๐ด))) โ (๐ โ โ โง (๐ โ (1...๐ด) โง ๐ โค (๐ pCnt ๐ด)))) |
17 | | prmz 16611 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โค) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โค) |
19 | | iddvdsexp 16222 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โฅ (๐โ๐)) |
20 | 18, 19 | sylan 580 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ๐ โฅ (๐โ๐)) |
21 | 17 | ad2antlr 725 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โค) |
22 | | prmnn 16610 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โ) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
24 | | nnnn0 12478 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ0) |
25 | | nnexpcl 14039 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
26 | 23, 24, 25 | syl2an 596 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ (๐โ๐) โ โ) |
27 | 26 | nnzd 12584 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ (๐โ๐) โ โค) |
28 | | nnz 12578 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ ๐ด โ
โค) |
29 | 28 | ad2antrr 724 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ๐ด โ
โค) |
30 | | dvdstr 16236 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง (๐โ๐) โ โค โง ๐ด โ โค) โ ((๐ โฅ (๐โ๐) โง (๐โ๐) โฅ ๐ด) โ ๐ โฅ ๐ด)) |
31 | 21, 27, 29, 30 | syl3anc 1371 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ((๐ โฅ (๐โ๐) โง (๐โ๐) โฅ ๐ด) โ ๐ โฅ ๐ด)) |
32 | 20, 31 | mpand 693 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ((๐โ๐) โฅ ๐ด โ ๐ โฅ ๐ด)) |
33 | | simpll 765 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ๐ด โ
โ) |
34 | | dvdsle 16252 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ด โ โ) โ (๐ โฅ ๐ด โ ๐ โค ๐ด)) |
35 | 21, 33, 34 | syl2anc 584 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ (๐ โฅ ๐ด โ ๐ โค ๐ด)) |
36 | 32, 35 | syld 47 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ((๐โ๐) โฅ ๐ด โ ๐ โค ๐ด)) |
37 | 22 | ad2antlr 725 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โ) |
38 | | fznn 13568 |
. . . . . . . . . . . . 13
โข (๐ด โ โค โ (๐ โ (1...๐ด) โ (๐ โ โ โง ๐ โค ๐ด))) |
39 | 38 | baibd 540 |
. . . . . . . . . . . 12
โข ((๐ด โ โค โง ๐ โ โ) โ (๐ โ (1...๐ด) โ ๐ โค ๐ด)) |
40 | 29, 37, 39 | syl2anc 584 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ (๐ โ (1...๐ด) โ ๐ โค ๐ด)) |
41 | 36, 40 | sylibrd 258 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ((๐โ๐) โฅ ๐ด โ ๐ โ (1...๐ด))) |
42 | 41 | pm4.71rd 563 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ((๐โ๐) โฅ ๐ด โ (๐ โ (1...๐ด) โง (๐โ๐) โฅ ๐ด))) |
43 | | breq1 5151 |
. . . . . . . . . . 11
โข (๐ฅ = (๐โ๐) โ (๐ฅ โฅ ๐ด โ (๐โ๐) โฅ ๐ด)) |
44 | 43 | elrab3 3684 |
. . . . . . . . . 10
โข ((๐โ๐) โ โ โ ((๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด} โ (๐โ๐) โฅ ๐ด)) |
45 | 26, 44 | syl 17 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ((๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด} โ (๐โ๐) โฅ ๐ด)) |
46 | | simplr 767 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โ) |
47 | 24 | adantl 482 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ๐ โ
โ0) |
48 | | pcdvdsb 16801 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ด โ โค โง ๐ โ โ0)
โ (๐ โค (๐ pCnt ๐ด) โ (๐โ๐) โฅ ๐ด)) |
49 | 46, 29, 47, 48 | syl3anc 1371 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ (๐ โค (๐ pCnt ๐ด) โ (๐โ๐) โฅ ๐ด)) |
50 | 49 | anbi2d 629 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ((๐ โ (1...๐ด) โง ๐ โค (๐ pCnt ๐ด)) โ (๐ โ (1...๐ด) โง (๐โ๐) โฅ ๐ด))) |
51 | 42, 45, 50 | 3bitr4rd 311 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ โ โ) โ ((๐ โ (1...๐ด) โง ๐ โค (๐ pCnt ๐ด)) โ (๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด})) |
52 | 51 | pm5.32da 579 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ โ โ โง (๐ โ (1...๐ด) โง ๐ โค (๐ pCnt ๐ด))) โ (๐ โ โ โง (๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด}))) |
53 | 16, 52 | bitrid 282 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ โ (1...๐ด) โง (๐ โ โ โง ๐ โค (๐ pCnt ๐ด))) โ (๐ โ โ โง (๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด}))) |
54 | 15, 53 | bitrd 278 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ โ (1...๐ด) โง ๐ โ (1...(๐ pCnt ๐ด))) โ (๐ โ โ โง (๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด}))) |
55 | 54 | pm5.32da 579 |
. . . 4
โข (๐ด โ โ โ ((๐ โ โ โง (๐ โ (1...๐ด) โง ๐ โ (1...(๐ pCnt ๐ด)))) โ (๐ โ โ โง (๐ โ โ โง (๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด})))) |
56 | | elin 3964 |
. . . . . 6
โข (๐ โ ((1...๐ด) โฉ โ) โ (๐ โ (1...๐ด) โง ๐ โ โ)) |
57 | 56 | anbi1i 624 |
. . . . 5
โข ((๐ โ ((1...๐ด) โฉ โ) โง ๐ โ (1...(๐ pCnt ๐ด))) โ ((๐ โ (1...๐ด) โง ๐ โ โ) โง ๐ โ (1...(๐ pCnt ๐ด)))) |
58 | | anass 469 |
. . . . 5
โข (((๐ โ (1...๐ด) โง ๐ โ โ) โง ๐ โ (1...(๐ pCnt ๐ด))) โ (๐ โ (1...๐ด) โง (๐ โ โ โง ๐ โ (1...(๐ pCnt ๐ด))))) |
59 | | an12 643 |
. . . . 5
โข ((๐ โ (1...๐ด) โง (๐ โ โ โง ๐ โ (1...(๐ pCnt ๐ด)))) โ (๐ โ โ โง (๐ โ (1...๐ด) โง ๐ โ (1...(๐ pCnt ๐ด))))) |
60 | 57, 58, 59 | 3bitri 296 |
. . . 4
โข ((๐ โ ((1...๐ด) โฉ โ) โง ๐ โ (1...(๐ pCnt ๐ด))) โ (๐ โ โ โง (๐ โ (1...๐ด) โง ๐ โ (1...(๐ pCnt ๐ด))))) |
61 | | anass 469 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง (๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด}) โ (๐ โ โ โง (๐ โ โ โง (๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด}))) |
62 | 55, 60, 61 | 3bitr4g 313 |
. . 3
โข (๐ด โ โ โ ((๐ โ ((1...๐ด) โฉ โ) โง ๐ โ (1...(๐ pCnt ๐ด))) โ ((๐ โ โ โง ๐ โ โ) โง (๐โ๐) โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด}))) |
63 | 6 | sselda 3982 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด}) โ ๐ โ โ) |
64 | | vmacl 26619 |
. . . . 5
โข (๐ โ โ โ
(ฮโ๐) โ
โ) |
65 | 63, 64 | syl 17 |
. . . 4
โข ((๐ด โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด}) โ (ฮโ๐) โ โ) |
66 | 65 | recnd 11241 |
. . 3
โข ((๐ด โ โ โง ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด}) โ (ฮโ๐) โ โ) |
67 | | simprr 771 |
. . 3
โข ((๐ด โ โ โง (๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด} โง (ฮโ๐) = 0)) โ (ฮโ๐) = 0) |
68 | 1, 4, 6, 9, 62, 66, 67 | fsumvma 26713 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด} (ฮโ๐) = ฮฃ๐ โ ((1...๐ด) โฉ โ)ฮฃ๐ โ (1...(๐ pCnt ๐ด))(ฮโ(๐โ๐))) |
69 | | elinel2 4196 |
. . . . . . 7
โข (๐ โ ((1...๐ด) โฉ โ) โ ๐ โ โ) |
70 | 69 | ad2antlr 725 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โง ๐ โ (1...(๐ pCnt ๐ด))) โ ๐ โ โ) |
71 | | elfznn 13529 |
. . . . . . 7
โข (๐ โ (1...(๐ pCnt ๐ด)) โ ๐ โ โ) |
72 | 71 | adantl 482 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โง ๐ โ (1...(๐ pCnt ๐ด))) โ ๐ โ โ) |
73 | | vmappw 26617 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ
(ฮโ(๐โ๐)) = (logโ๐)) |
74 | 70, 72, 73 | syl2anc 584 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โง ๐ โ (1...(๐ pCnt ๐ด))) โ (ฮโ(๐โ๐)) = (logโ๐)) |
75 | 74 | sumeq2dv 15648 |
. . . 4
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ฮฃ๐ โ (1...(๐ pCnt ๐ด))(ฮโ(๐โ๐)) = ฮฃ๐ โ (1...(๐ pCnt ๐ด))(logโ๐)) |
76 | | fzfid 13937 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (1...(๐ pCnt ๐ด)) โ Fin) |
77 | 69, 22 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((1...๐ด) โฉ โ) โ ๐ โ โ) |
78 | 77 | adantl 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ๐ โ โ) |
79 | 78 | nnrpd 13013 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ๐ โ โ+) |
80 | 79 | relogcld 26130 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (logโ๐) โ
โ) |
81 | 80 | recnd 11241 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (logโ๐) โ
โ) |
82 | | fsumconst 15735 |
. . . . 5
โข
(((1...(๐ pCnt ๐ด)) โ Fin โง
(logโ๐) โ
โ) โ ฮฃ๐
โ (1...(๐ pCnt ๐ด))(logโ๐) = ((โฏโ(1...(๐ pCnt ๐ด))) ยท (logโ๐))) |
83 | 76, 81, 82 | syl2anc 584 |
. . . 4
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ฮฃ๐ โ (1...(๐ pCnt ๐ด))(logโ๐) = ((โฏโ(1...(๐ pCnt ๐ด))) ยท (logโ๐))) |
84 | 69, 11 | sylan2 593 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ (๐ pCnt ๐ด) โ
โ0) |
85 | | hashfz1 14305 |
. . . . . 6
โข ((๐ pCnt ๐ด) โ โ0 โ
(โฏโ(1...(๐ pCnt
๐ด))) = (๐ pCnt ๐ด)) |
86 | 84, 85 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ
(โฏโ(1...(๐ pCnt
๐ด))) = (๐ pCnt ๐ด)) |
87 | 86 | oveq1d 7423 |
. . . 4
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ
((โฏโ(1...(๐
pCnt ๐ด))) ยท
(logโ๐)) = ((๐ pCnt ๐ด) ยท (logโ๐))) |
88 | 75, 83, 87 | 3eqtrd 2776 |
. . 3
โข ((๐ด โ โ โง ๐ โ ((1...๐ด) โฉ โ)) โ ฮฃ๐ โ (1...(๐ pCnt ๐ด))(ฮโ(๐โ๐)) = ((๐ pCnt ๐ด) ยท (logโ๐))) |
89 | 88 | sumeq2dv 15648 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ ((1...๐ด) โฉ โ)ฮฃ๐ โ (1...(๐ pCnt ๐ด))(ฮโ(๐โ๐)) = ฮฃ๐ โ ((1...๐ด) โฉ โ)((๐ pCnt ๐ด) ยท (logโ๐))) |
90 | | pclogsum 26715 |
. 2
โข (๐ด โ โ โ
ฮฃ๐ โ ((1...๐ด) โฉ โ)((๐ pCnt ๐ด) ยท (logโ๐)) = (logโ๐ด)) |
91 | 68, 89, 90 | 3eqtrd 2776 |
1
โข (๐ด โ โ โ
ฮฃ๐ โ {๐ฅ โ โ โฃ ๐ฅ โฅ ๐ด} (ฮโ๐) = (logโ๐ด)) |