Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6852 |
. . . 4
β’ (π = (π Β· π) β (πβ(πΏβπ)) = (πβ(πΏβ(π Β· π)))) |
2 | | oveq2 7370 |
. . . . 5
β’ (π = (π Β· π) β ((ΞΌβπ) / π) = ((ΞΌβπ) / (π Β· π))) |
3 | | fvoveq1 7385 |
. . . . 5
β’ (π = (π Β· π) β (logβ(π / π)) = (logβ((π Β· π) / π))) |
4 | 2, 3 | oveq12d 7380 |
. . . 4
β’ (π = (π Β· π) β (((ΞΌβπ) / π) Β· (logβ(π / π))) = (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π)))) |
5 | 1, 4 | oveq12d 7380 |
. . 3
β’ (π = (π Β· π) β ((πβ(πΏβπ)) Β· (((ΞΌβπ) / π) Β· (logβ(π / π)))) = ((πβ(πΏβ(π Β· π))) Β· (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π))))) |
6 | | dchrvmasum.a |
. . . 4
β’ (π β π΄ β
β+) |
7 | 6 | rpred 12964 |
. . 3
β’ (π β π΄ β β) |
8 | | rpvmasum.g |
. . . . . 6
β’ πΊ = (DChrβπ) |
9 | | rpvmasum.z |
. . . . . 6
β’ π =
(β€/nβ€βπ) |
10 | | rpvmasum.d |
. . . . . 6
β’ π· = (BaseβπΊ) |
11 | | rpvmasum.l |
. . . . . 6
β’ πΏ = (β€RHomβπ) |
12 | | dchrisum.b |
. . . . . . 7
β’ (π β π β π·) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β π β π·) |
14 | | elfzelz 13448 |
. . . . . . 7
β’ (π β
(1...(ββπ΄))
β π β
β€) |
15 | 14 | adantl 483 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β π β β€) |
16 | 8, 9, 10, 11, 13, 15 | dchrzrhcl 26609 |
. . . . 5
β’ ((π β§ π β (1...(ββπ΄))) β (πβ(πΏβπ)) β β) |
17 | 16 | adantrr 716 |
. . . 4
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (πβ(πΏβπ)) β β) |
18 | | elrabi 3644 |
. . . . . . . . . 10
β’ (π β {π₯ β β β£ π₯ β₯ π} β π β β) |
19 | 18 | ad2antll 728 |
. . . . . . . . 9
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β π β β) |
20 | | mucl 26506 |
. . . . . . . . 9
β’ (π β β β
(ΞΌβπ) β
β€) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (ΞΌβπ) β β€) |
22 | 21 | zred 12614 |
. . . . . . 7
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (ΞΌβπ) β β) |
23 | | elfznn 13477 |
. . . . . . . 8
β’ (π β
(1...(ββπ΄))
β π β
β) |
24 | 23 | ad2antrl 727 |
. . . . . . 7
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β π β β) |
25 | 22, 24 | nndivred 12214 |
. . . . . 6
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β ((ΞΌβπ) / π) β β) |
26 | 25 | recnd 11190 |
. . . . 5
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β ((ΞΌβπ) / π) β β) |
27 | 24 | nnrpd 12962 |
. . . . . . . 8
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β π β β+) |
28 | 19 | nnrpd 12962 |
. . . . . . . 8
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β π β β+) |
29 | 27, 28 | rpdivcld 12981 |
. . . . . . 7
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (π / π) β
β+) |
30 | 29 | relogcld 25994 |
. . . . . 6
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (logβ(π / π)) β β) |
31 | 30 | recnd 11190 |
. . . . 5
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (logβ(π / π)) β β) |
32 | 26, 31 | mulcld 11182 |
. . . 4
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (((ΞΌβπ) / π) Β· (logβ(π / π))) β β) |
33 | 17, 32 | mulcld 11182 |
. . 3
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β ((πβ(πΏβπ)) Β· (((ΞΌβπ) / π) Β· (logβ(π / π)))) β β) |
34 | 5, 7, 33 | dvdsflsumcom 26553 |
. 2
β’ (π β Ξ£π β (1...(ββπ΄))Ξ£π β {π₯ β β β£ π₯ β₯ π} ((πβ(πΏβπ)) Β· (((ΞΌβπ) / π) Β· (logβ(π / π)))) = Ξ£π β (1...(ββπ΄))Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβ(π Β· π))) Β· (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π))))) |
35 | | vmaf 26484 |
. . . . . . . . . . . . 13
β’
Ξ:ββΆβ |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β
Ξ:ββΆβ) |
37 | | ax-resscn 11115 |
. . . . . . . . . . . 12
β’ β
β β |
38 | | fss 6690 |
. . . . . . . . . . . 12
β’
((Ξ:ββΆβ β§ β β β) β
Ξ:ββΆβ) |
39 | 36, 37, 38 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β
Ξ:ββΆβ) |
40 | | vmasum 26580 |
. . . . . . . . . . . . . 14
β’ (π β β β
Ξ£π β {π₯ β β β£ π₯ β₯ π} (Ξβπ) = (logβπ)) |
41 | 40 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β Ξ£π β {π₯ β β β£ π₯ β₯ π} (Ξβπ) = (logβπ)) |
42 | 41 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (logβπ) = Ξ£π β {π₯ β β β£ π₯ β₯ π} (Ξβπ)) |
43 | 42 | mpteq2dva 5210 |
. . . . . . . . . . 11
β’ (π β (π β β β¦ (logβπ)) = (π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} (Ξβπ))) |
44 | 39, 43 | muinv 26558 |
. . . . . . . . . 10
β’ (π β Ξ = (π β β β¦
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π))))) |
45 | 44 | fveq1d 6849 |
. . . . . . . . 9
β’ (π β (Ξβπ) = ((π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π))))βπ)) |
46 | | sumex 15579 |
. . . . . . . . . 10
β’
Ξ£π β
{π₯ β β β£
π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π))) β V |
47 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π β β β¦
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π)))) = (π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π)))) |
48 | 47 | fvmpt2 6964 |
. . . . . . . . . 10
β’ ((π β β β§
Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π))) β V) β ((π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π))))βπ) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π)))) |
49 | 23, 46, 48 | sylancl 587 |
. . . . . . . . 9
β’ (π β
(1...(ββπ΄))
β ((π β β
β¦ Ξ£π β
{π₯ β β β£
π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π))))βπ) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π)))) |
50 | 45, 49 | sylan9eq 2797 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β (Ξβπ) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π)))) |
51 | | breq1 5113 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
52 | 51 | elrab 3650 |
. . . . . . . . . . . . . 14
β’ (π β {π₯ β β β£ π₯ β₯ π} β (π β β β§ π β₯ π)) |
53 | 52 | simprbi 498 |
. . . . . . . . . . . . 13
β’ (π β {π₯ β β β£ π₯ β₯ π} β π β₯ π) |
54 | 53 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β₯ π) |
55 | 23 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
56 | | nndivdvds 16152 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β (π β₯ π β (π / π) β β)) |
57 | 55, 18, 56 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π β₯ π β (π / π) β β)) |
58 | 54, 57 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β β) |
59 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = (π / π) β (logβπ) = (logβ(π / π))) |
60 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β β β¦
(logβπ)) = (π β β β¦
(logβπ)) |
61 | | fvex 6860 |
. . . . . . . . . . . 12
β’
(logβ(π /
π)) β
V |
62 | 59, 60, 61 | fvmpt 6953 |
. . . . . . . . . . 11
β’ ((π / π) β β β ((π β β β¦ (logβπ))β(π / π)) = (logβ(π / π))) |
63 | 58, 62 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((π β β β¦ (logβπ))β(π / π)) = (logβ(π / π))) |
64 | 63 | oveq2d 7378 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π))) = ((ΞΌβπ) Β· (logβ(π / π)))) |
65 | 64 | sumeq2dv 15595 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· ((π β β β¦ (logβπ))β(π / π))) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (logβ(π / π)))) |
66 | 50, 65 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β (Ξβπ) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (logβ(π / π)))) |
67 | 66 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β ((Ξβπ) / π) = (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (logβ(π / π))) / π)) |
68 | | fzfid 13885 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β (1...π) β Fin) |
69 | | dvdsssfz1 16207 |
. . . . . . . . 9
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
70 | 55, 69 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
71 | 68, 70 | ssfid 9218 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β {π₯ β β β£ π₯ β₯ π} β Fin) |
72 | 55 | nncnd 12176 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
73 | 21 | zcnd 12615 |
. . . . . . . . 9
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (ΞΌβπ) β β) |
74 | 73 | anassrs 469 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β (ΞΌβπ) β β) |
75 | 31 | anassrs 469 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β (logβ(π / π)) β β) |
76 | 74, 75 | mulcld 11182 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((ΞΌβπ) Β· (logβ(π / π))) β β) |
77 | 55 | nnne0d 12210 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β π β 0) |
78 | 71, 72, 76, 77 | fsumdivc 15678 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β (Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (logβ(π / π))) / π) = Ξ£π β {π₯ β β β£ π₯ β₯ π} (((ΞΌβπ) Β· (logβ(π / π))) / π)) |
79 | 18 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β) |
80 | 79, 20 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β (ΞΌβπ) β β€) |
81 | 80 | zcnd 12615 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β (ΞΌβπ) β β) |
82 | 72 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β) |
83 | 77 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β 0) |
84 | 81, 75, 82, 83 | div23d 11975 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β (((ΞΌβπ) Β· (logβ(π / π))) / π) = (((ΞΌβπ) / π) Β· (logβ(π / π)))) |
85 | 84 | sumeq2dv 15595 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β Ξ£π β {π₯ β β β£ π₯ β₯ π} (((ΞΌβπ) Β· (logβ(π / π))) / π) = Ξ£π β {π₯ β β β£ π₯ β₯ π} (((ΞΌβπ) / π) Β· (logβ(π / π)))) |
86 | 67, 78, 85 | 3eqtrd 2781 |
. . . . 5
β’ ((π β§ π β (1...(ββπ΄))) β ((Ξβπ) / π) = Ξ£π β {π₯ β β β£ π₯ β₯ π} (((ΞΌβπ) / π) Β· (logβ(π / π)))) |
87 | 86 | oveq2d 7378 |
. . . 4
β’ ((π β§ π β (1...(ββπ΄))) β ((πβ(πΏβπ)) Β· ((Ξβπ) / π)) = ((πβ(πΏβπ)) Β· Ξ£π β {π₯ β β β£ π₯ β₯ π} (((ΞΌβπ) / π) Β· (logβ(π / π))))) |
88 | 32 | anassrs 469 |
. . . . 5
β’ (((π β§ π β (1...(ββπ΄))) β§ π β {π₯ β β β£ π₯ β₯ π}) β (((ΞΌβπ) / π) Β· (logβ(π / π))) β β) |
89 | 71, 16, 88 | fsummulc2 15676 |
. . . 4
β’ ((π β§ π β (1...(ββπ΄))) β ((πβ(πΏβπ)) Β· Ξ£π β {π₯ β β β£ π₯ β₯ π} (((ΞΌβπ) / π) Β· (logβ(π / π)))) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((πβ(πΏβπ)) Β· (((ΞΌβπ) / π) Β· (logβ(π / π))))) |
90 | 87, 89 | eqtrd 2777 |
. . 3
β’ ((π β§ π β (1...(ββπ΄))) β ((πβ(πΏβπ)) Β· ((Ξβπ) / π)) = Ξ£π β {π₯ β β β£ π₯ β₯ π} ((πβ(πΏβπ)) Β· (((ΞΌβπ) / π) Β· (logβ(π / π))))) |
91 | 90 | sumeq2dv 15595 |
. 2
β’ (π β Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) = Ξ£π β (1...(ββπ΄))Ξ£π β {π₯ β β β£ π₯ β₯ π} ((πβ(πΏβπ)) Β· (((ΞΌβπ) / π) Β· (logβ(π / π))))) |
92 | | fzfid 13885 |
. . . . 5
β’ ((π β§ π β (1...(ββπ΄))) β (1...(ββ(π΄ / π))) β Fin) |
93 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β π β π·) |
94 | | elfzelz 13448 |
. . . . . . . 8
β’ (π β
(1...(ββπ΄))
β π β
β€) |
95 | 94 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β π β β€) |
96 | 8, 9, 10, 11, 93, 95 | dchrzrhcl 26609 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β (πβ(πΏβπ)) β β) |
97 | | fznnfl 13774 |
. . . . . . . . . . . 12
β’ (π΄ β β β (π β
(1...(ββπ΄))
β (π β β
β§ π β€ π΄))) |
98 | 7, 97 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π β (1...(ββπ΄)) β (π β β β§ π β€ π΄))) |
99 | 98 | simprbda 500 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
100 | 99, 20 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β (ΞΌβπ) β β€) |
101 | 100 | zred 12614 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β (ΞΌβπ) β β) |
102 | 101, 99 | nndivred 12214 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β ((ΞΌβπ) / π) β β) |
103 | 102 | recnd 11190 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β ((ΞΌβπ) / π) β β) |
104 | 96, 103 | mulcld 11182 |
. . . . 5
β’ ((π β§ π β (1...(ββπ΄))) β ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) β β) |
105 | 12 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β π·) |
106 | | elfzelz 13448 |
. . . . . . . 8
β’ (π β
(1...(ββ(π΄ /
π))) β π β
β€) |
107 | 106 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β€) |
108 | 8, 9, 10, 11, 105, 107 | dchrzrhcl 26609 |
. . . . . 6
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (πβ(πΏβπ)) β β) |
109 | | elfznn 13477 |
. . . . . . . . . . 11
β’ (π β
(1...(ββ(π΄ /
π))) β π β
β) |
110 | 109 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β) |
111 | 110 | nnrpd 12962 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β+) |
112 | 111 | relogcld 25994 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβπ) β β) |
113 | 112, 110 | nndivred 12214 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβπ) / π) β β) |
114 | 113 | recnd 11190 |
. . . . . 6
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβπ) / π) β β) |
115 | 108, 114 | mulcld 11182 |
. . . . 5
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) Β· ((logβπ) / π)) β β) |
116 | 92, 104, 115 | fsummulc2 15676 |
. . . 4
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) = Ξ£π β (1...(ββ(π΄ / π)))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) Β· ((logβπ) / π)))) |
117 | 96 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (πβ(πΏβπ)) β β) |
118 | 103 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((ΞΌβπ) / π) β β) |
119 | 117, 118,
108, 114 | mul4d 11374 |
. . . . . 6
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) Β· ((logβπ) / π))) = (((πβ(πΏβπ)) Β· (πβ(πΏβπ))) Β· (((ΞΌβπ) / π) Β· ((logβπ) / π)))) |
120 | 94 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β€) |
121 | 8, 9, 10, 11, 105, 120, 107 | dchrzrhmul 26610 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (πβ(πΏβ(π Β· π))) = ((πβ(πΏβπ)) Β· (πβ(πΏβπ)))) |
122 | 101 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (ΞΌβπ) β β) |
123 | 122 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (ΞΌβπ) β β) |
124 | 112 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβπ) β β) |
125 | 99 | nnrpd 12962 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...(ββπ΄))) β π β β+) |
126 | 125 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β+) |
127 | 126, 111 | rpmulcld 12980 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (π Β· π) β
β+) |
128 | 127 | rpcnne0d 12973 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((π Β· π) β β β§ (π Β· π) β 0)) |
129 | | div23 11839 |
. . . . . . . . 9
β’
(((ΞΌβπ)
β β β§ (logβπ) β β β§ ((π Β· π) β β β§ (π Β· π) β 0)) β (((ΞΌβπ) Β· (logβπ)) / (π Β· π)) = (((ΞΌβπ) / (π Β· π)) Β· (logβπ))) |
130 | 123, 124,
128, 129 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((ΞΌβπ) Β· (logβπ)) / (π Β· π)) = (((ΞΌβπ) / (π Β· π)) Β· (logβπ))) |
131 | 126 | rpcnne0d 12973 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (π β β β§ π β 0)) |
132 | 111 | rpcnne0d 12973 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (π β β β§ π β 0)) |
133 | | divmuldiv 11862 |
. . . . . . . . 9
β’
((((ΞΌβπ)
β β β§ (logβπ) β β) β§ ((π β β β§ π β 0) β§ (π β β β§ π β 0))) β (((ΞΌβπ) / π) Β· ((logβπ) / π)) = (((ΞΌβπ) Β· (logβπ)) / (π Β· π))) |
134 | 123, 124,
131, 132, 133 | syl22anc 838 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((ΞΌβπ) / π) Β· ((logβπ) / π)) = (((ΞΌβπ) Β· (logβπ)) / (π Β· π))) |
135 | 110 | nncnd 12176 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β) |
136 | 126 | rpcnd 12966 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β) |
137 | 126 | rpne0d 12969 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β 0) |
138 | 135, 136,
137 | divcan3d 11943 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((π Β· π) / π) = π) |
139 | 138 | fveq2d 6851 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβ((π Β· π) / π)) = (logβπ)) |
140 | 139 | oveq2d 7378 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π))) = (((ΞΌβπ) / (π Β· π)) Β· (logβπ))) |
141 | 130, 134,
140 | 3eqtr4rd 2788 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π))) = (((ΞΌβπ) / π) Β· ((logβπ) / π))) |
142 | 121, 141 | oveq12d 7380 |
. . . . . 6
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβ(π Β· π))) Β· (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π)))) = (((πβ(πΏβπ)) Β· (πβ(πΏβπ))) Β· (((ΞΌβπ) / π) Β· ((logβπ) / π)))) |
143 | 119, 142 | eqtr4d 2780 |
. . . . 5
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) Β· ((logβπ) / π))) = ((πβ(πΏβ(π Β· π))) Β· (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π))))) |
144 | 143 | sumeq2dv 15595 |
. . . 4
β’ ((π β§ π β (1...(ββπ΄))) β Ξ£π β (1...(ββ(π΄ / π)))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) Β· ((logβπ) / π))) = Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβ(π Β· π))) Β· (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π))))) |
145 | 116, 144 | eqtrd 2777 |
. . 3
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) = Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβ(π Β· π))) Β· (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π))))) |
146 | 145 | sumeq2dv 15595 |
. 2
β’ (π β Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) = Ξ£π β (1...(ββπ΄))Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβ(π Β· π))) Β· (((ΞΌβπ) / (π Β· π)) Β· (logβ((π Β· π) / π))))) |
147 | 34, 91, 146 | 3eqtr4d 2787 |
1
β’ (π β Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π)))) |