Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . . . 6
β’ (π β (1...(ββπ΄)) β Fin) |
2 | | rpvmasum.g |
. . . . . . . . 9
β’ πΊ = (DChrβπ) |
3 | | rpvmasum.z |
. . . . . . . . 9
β’ π =
(β€/nβ€βπ) |
4 | | rpvmasum.d |
. . . . . . . . 9
β’ π· = (BaseβπΊ) |
5 | | rpvmasum.l |
. . . . . . . . 9
β’ πΏ = (β€RHomβπ) |
6 | | dchrisum.b |
. . . . . . . . . 10
β’ (π β π β π·) |
7 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β π β π·) |
8 | | elfzelz 13448 |
. . . . . . . . . 10
β’ (π β
(1...(ββπ΄))
β π β
β€) |
9 | 8 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β π β β€) |
10 | 2, 3, 4, 5, 7, 9 | dchrzrhcl 26609 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β (πβ(πΏβπ)) β β) |
11 | | elfznn 13477 |
. . . . . . . . . . 11
β’ (π β
(1...(ββπ΄))
β π β
β) |
12 | 11 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
13 | | mucl 26506 |
. . . . . . . . . . . 12
β’ (π β β β
(ΞΌβπ) β
β€) |
14 | 13 | zred 12614 |
. . . . . . . . . . 11
β’ (π β β β
(ΞΌβπ) β
β) |
15 | | nndivre 12201 |
. . . . . . . . . . 11
β’
(((ΞΌβπ)
β β β§ π
β β) β ((ΞΌβπ) / π) β β) |
16 | 14, 15 | mpancom 687 |
. . . . . . . . . 10
β’ (π β β β
((ΞΌβπ) / π) β
β) |
17 | 12, 16 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β ((ΞΌβπ) / π) β β) |
18 | 17 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β ((ΞΌβπ) / π) β β) |
19 | 10, 18 | mulcld 11182 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) β β) |
20 | | fzfid 13885 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β (1...(ββ(π΄ / π))) β Fin) |
21 | 7 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β π·) |
22 | | elfzelz 13448 |
. . . . . . . . . . 11
β’ (π β
(1...(ββ(π΄ /
π))) β π β
β€) |
23 | 22 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β€) |
24 | 2, 3, 4, 5, 21, 23 | dchrzrhcl 26609 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (πβ(πΏβπ)) β β) |
25 | | elfznn 13477 |
. . . . . . . . . . . . . 14
β’ (π β
(1...(ββ(π΄ /
π))) β π β
β) |
26 | 25 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β) |
27 | 26 | nnrpd 12962 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β+) |
28 | 27 | relogcld 25994 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβπ) β β) |
29 | 28, 26 | nndivred 12214 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβπ) / π) β β) |
30 | 29 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβπ) / π) β β) |
31 | 24, 30 | mulcld 11182 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) Β· ((logβπ) / π)) β β) |
32 | 20, 31 | fsumcl 15625 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π)) β β) |
33 | 19, 32 | mulcld 11182 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) β β) |
34 | | dchrvmasum.a |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β
β+) |
35 | 11 | nnrpd 12962 |
. . . . . . . . . . . . . . 15
β’ (π β
(1...(ββπ΄))
β π β
β+) |
36 | | rpdivcl 12947 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β+
β§ π β
β+) β (π΄ / π) β
β+) |
37 | 34, 35, 36 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(ββπ΄))) β (π΄ / π) β
β+) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (π΄ / π) β
β+) |
39 | 38, 27 | rpdivcld 12981 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((π΄ / π) / π) β
β+) |
40 | 39 | relogcld 25994 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβ((π΄ / π) / π)) β β) |
41 | 40, 26 | nndivred 12214 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβ((π΄ / π) / π)) / π) β β) |
42 | 41 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβ((π΄ / π) / π)) / π) β β) |
43 | 24, 42 | mulcld 11182 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)) β β) |
44 | 20, 43 | fsumcl 15625 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)) β β) |
45 | 19, 44 | mulcld 11182 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))) β β) |
46 | 1, 33, 45 | fsumadd 15632 |
. . . . 5
β’ (π β Ξ£π β (1...(ββπ΄))((((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) + (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) = (Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) + Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))))) |
47 | 38, 27 | relogdivd 25997 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβ((π΄ / π) / π)) = ((logβ(π΄ / π)) β (logβπ))) |
48 | 47 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβπ) + (logβ((π΄ / π) / π))) = ((logβπ) + ((logβ(π΄ / π)) β (logβπ)))) |
49 | 28 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβπ) β β) |
50 | 37 | relogcld 25994 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...(ββπ΄))) β (logβ(π΄ / π)) β β) |
51 | 50 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...(ββπ΄))) β (logβ(π΄ / π)) β β) |
52 | 51 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβ(π΄ / π)) β β) |
53 | 49, 52 | pncan3d 11522 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβπ) + ((logβ(π΄ / π)) β (logβπ))) = (logβ(π΄ / π))) |
54 | 48, 53 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβ(π΄ / π)) = ((logβπ) + (logβ((π΄ / π) / π)))) |
55 | 54 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβ(π΄ / π)) / π) = (((logβπ) + (logβ((π΄ / π) / π))) / π)) |
56 | 40 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβ((π΄ / π) / π)) β β) |
57 | 26 | nncnd 12176 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β) |
58 | 26 | nnne0d 12210 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β 0) |
59 | 49, 56, 57, 58 | divdird 11976 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((logβπ) + (logβ((π΄ / π) / π))) / π) = (((logβπ) / π) + ((logβ((π΄ / π) / π)) / π))) |
60 | 55, 59 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβ(π΄ / π)) / π) = (((logβπ) / π) + ((logβ((π΄ / π) / π)) / π))) |
61 | 60 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π)) = ((πβ(πΏβπ)) Β· (((logβπ) / π) + ((logβ((π΄ / π) / π)) / π)))) |
62 | 24, 30, 42 | adddid 11186 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) Β· (((logβπ) / π) + ((logβ((π΄ / π) / π)) / π))) = (((πβ(πΏβπ)) Β· ((logβπ) / π)) + ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) |
63 | 61, 62 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π)) = (((πβ(πΏβπ)) Β· ((logβπ) / π)) + ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) |
64 | 63 | sumeq2dv 15595 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π)) = Ξ£π β (1...(ββ(π΄ / π)))(((πβ(πΏβπ)) Β· ((logβπ) / π)) + ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) |
65 | 20, 31, 43 | fsumadd 15632 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β Ξ£π β (1...(ββ(π΄ / π)))(((πβ(πΏβπ)) Β· ((logβπ) / π)) + ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))) = (Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π)) + Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) |
66 | 64, 65 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π)) = (Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π)) + Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) |
67 | 66 | oveq2d 7378 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π))) = (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π)) + Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))))) |
68 | 19, 32, 44 | adddid 11186 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π)) + Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) = ((((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) + (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))))) |
69 | 67, 68 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π))) = ((((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) + (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))))) |
70 | 69 | sumeq2dv 15595 |
. . . . 5
β’ (π β Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π))) = Ξ£π β (1...(ββπ΄))((((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) + (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))))) |
71 | | rpvmasum.a |
. . . . . . 7
β’ (π β π β β) |
72 | | rpvmasum.1 |
. . . . . . 7
β’ 1 =
(0gβπΊ) |
73 | | dchrisum.n1 |
. . . . . . 7
β’ (π β π β 1 ) |
74 | 3, 5, 71, 2, 4, 72, 6, 73, 34 | dchrvmasumlem1 26859 |
. . . . . 6
β’ (π β Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π)))) |
75 | | dchrvmasum2.2 |
. . . . . . 7
β’ (π β 1 β€ π΄) |
76 | 3, 5, 71, 2, 4, 72, 6, 73, 34, 75 | dchrvmasum2lem 26860 |
. . . . . 6
β’ (π β (logβπ΄) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) |
77 | 74, 76 | oveq12d 7380 |
. . . . 5
β’ (π β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + (logβπ΄)) = (Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) + Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))))) |
78 | 46, 70, 77 | 3eqtr4rd 2788 |
. . . 4
β’ (π β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + (logβπ΄)) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π)))) |
79 | 78 | adantr 482 |
. . 3
β’ ((π β§ π) β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + (logβπ΄)) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π)))) |
80 | | iftrue 4497 |
. . . . 5
β’ (π β if(π, (logβπ΄), 0) = (logβπ΄)) |
81 | 80 | oveq2d 7378 |
. . . 4
β’ (π β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π, (logβπ΄), 0)) = (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + (logβπ΄))) |
82 | 81 | adantl 483 |
. . 3
β’ ((π β§ π) β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π, (logβπ΄), 0)) = (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + (logβπ΄))) |
83 | | iftrue 4497 |
. . . . . . . . . 10
β’ (π β if(π, (π΄ / π), π) = (π΄ / π)) |
84 | 83 | fveq2d 6851 |
. . . . . . . . 9
β’ (π β (logβif(π, (π΄ / π), π)) = (logβ(π΄ / π))) |
85 | 84 | oveq1d 7377 |
. . . . . . . 8
β’ (π β ((logβif(π, (π΄ / π), π)) / π) = ((logβ(π΄ / π)) / π)) |
86 | 85 | oveq2d 7378 |
. . . . . . 7
β’ (π β ((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π)) = ((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π))) |
87 | 86 | sumeq2sdv 15596 |
. . . . . 6
β’ (π β Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π)) = Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π))) |
88 | 87 | oveq2d 7378 |
. . . . 5
β’ (π β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π))) = (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π)))) |
89 | 88 | sumeq2sdv 15596 |
. . . 4
β’ (π β Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π))) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π)))) |
90 | 89 | adantl 483 |
. . 3
β’ ((π β§ π) β Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π))) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ(π΄ / π)) / π)))) |
91 | 79, 82, 90 | 3eqtr4d 2787 |
. 2
β’ ((π β§ π) β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π, (logβπ΄), 0)) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π)))) |
92 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β π β π·) |
93 | | elfzelz 13448 |
. . . . . . . . 9
β’ (π β
(1...(ββπ΄))
β π β
β€) |
94 | 93 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β π β β€) |
95 | 2, 3, 4, 5, 92, 94 | dchrzrhcl 26609 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β (πβ(πΏβπ)) β β) |
96 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ΄))
β π β
β) |
97 | 96 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
98 | | vmacl 26483 |
. . . . . . . . . 10
β’ (π β β β
(Ξβπ) β
β) |
99 | | nndivre 12201 |
. . . . . . . . . 10
β’
(((Ξβπ)
β β β§ π
β β) β ((Ξβπ) / π) β β) |
100 | 98, 99 | mpancom 687 |
. . . . . . . . 9
β’ (π β β β
((Ξβπ) / π) β
β) |
101 | 100 | recnd 11190 |
. . . . . . . 8
β’ (π β β β
((Ξβπ) / π) β
β) |
102 | 97, 101 | syl 17 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β ((Ξβπ) / π) β β) |
103 | 95, 102 | mulcld 11182 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β ((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β β) |
104 | 1, 103 | fsumcl 15625 |
. . . . 5
β’ (π β Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β β) |
105 | 104 | adantr 482 |
. . . 4
β’ ((π β§ Β¬ π) β Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β β) |
106 | 105 | addid1d 11362 |
. . 3
β’ ((π β§ Β¬ π) β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + 0) = Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π))) |
107 | | iffalse 4500 |
. . . . 5
β’ (Β¬
π β if(π, (logβπ΄), 0) = 0) |
108 | 107 | adantl 483 |
. . . 4
β’ ((π β§ Β¬ π) β if(π, (logβπ΄), 0) = 0) |
109 | 108 | oveq2d 7378 |
. . 3
β’ ((π β§ Β¬ π) β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π, (logβπ΄), 0)) = (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + 0)) |
110 | | iffalse 4500 |
. . . . . . . . . 10
β’ (Β¬
π β if(π, (π΄ / π), π) = π) |
111 | 110 | fveq2d 6851 |
. . . . . . . . 9
β’ (Β¬
π β (logβif(π, (π΄ / π), π)) = (logβπ)) |
112 | 111 | oveq1d 7377 |
. . . . . . . 8
β’ (Β¬
π β ((logβif(π, (π΄ / π), π)) / π) = ((logβπ) / π)) |
113 | 112 | oveq2d 7378 |
. . . . . . 7
β’ (Β¬
π β ((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π)) = ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
114 | 113 | sumeq2sdv 15596 |
. . . . . 6
β’ (Β¬
π β Ξ£π β
(1...(ββ(π΄ /
π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π)) = Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) |
115 | 114 | oveq2d 7378 |
. . . . 5
β’ (Β¬
π β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π))) = (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π)))) |
116 | 115 | sumeq2sdv 15596 |
. . . 4
β’ (Β¬
π β Ξ£π β
(1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π))) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π)))) |
117 | 74 | eqcomd 2743 |
. . . 4
β’ (π β Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβπ) / π))) = Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π))) |
118 | 116, 117 | sylan9eqr 2799 |
. . 3
β’ ((π β§ Β¬ π) β Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π))) = Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π))) |
119 | 106, 109,
118 | 3eqtr4d 2787 |
. 2
β’ ((π β§ Β¬ π) β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π, (logβπ΄), 0)) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π)))) |
120 | 91, 119 | pm2.61dan 812 |
1
β’ (π β (Ξ£π β (1...(ββπ΄))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π, (logβπ΄), 0)) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβif(π, (π΄ / π), π)) / π)))) |