Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6852 |
. . . . . 6
β’ (π = (π Β· π) β (πβ(πΏβπ)) = (πβ(πΏβ(π Β· π)))) |
2 | | id 22 |
. . . . . 6
β’ (π = (π Β· π) β π = (π Β· π)) |
3 | 1, 2 | oveq12d 7380 |
. . . . 5
β’ (π = (π Β· π) β ((πβ(πΏβπ)) / π) = ((πβ(πΏβ(π Β· π))) / (π Β· π))) |
4 | | oveq2 7370 |
. . . . . 6
β’ (π = (π Β· π) β (π΄ / π) = (π΄ / (π Β· π))) |
5 | 4 | fveq2d 6851 |
. . . . 5
β’ (π = (π Β· π) β (logβ(π΄ / π)) = (logβ(π΄ / (π Β· π)))) |
6 | 3, 5 | oveq12d 7380 |
. . . 4
β’ (π = (π Β· π) β (((πβ(πΏβπ)) / π) Β· (logβ(π΄ / π))) = (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π))))) |
7 | 6 | oveq2d 7378 |
. . 3
β’ (π = (π Β· π) β ((ΞΌβπ) Β· (((πβ(πΏβπ)) / π) Β· (logβ(π΄ / π)))) = ((ΞΌβπ) Β· (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π)))))) |
8 | | dchrvmasum.a |
. . . 4
β’ (π β π΄ β
β+) |
9 | 8 | rpred 12964 |
. . 3
β’ (π β π΄ β β) |
10 | | elrabi 3644 |
. . . . . . 7
β’ (π β {π₯ β β β£ π₯ β₯ π} β π β β) |
11 | 10 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β π β β) |
12 | | mucl 26506 |
. . . . . 6
β’ (π β β β
(ΞΌβπ) β
β€) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (ΞΌβπ) β β€) |
14 | 13 | zcnd 12615 |
. . . 4
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (ΞΌβπ) β β) |
15 | | rpvmasum.g |
. . . . . . . 8
β’ πΊ = (DChrβπ) |
16 | | rpvmasum.z |
. . . . . . . 8
β’ π =
(β€/nβ€βπ) |
17 | | rpvmasum.d |
. . . . . . . 8
β’ π· = (BaseβπΊ) |
18 | | rpvmasum.l |
. . . . . . . 8
β’ πΏ = (β€RHomβπ) |
19 | | dchrisum.b |
. . . . . . . . 9
β’ (π β π β π·) |
20 | 19 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β π β π·) |
21 | | elfzelz 13448 |
. . . . . . . . 9
β’ (π β
(1...(ββπ΄))
β π β
β€) |
22 | 21 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β π β β€) |
23 | 15, 16, 17, 18, 20, 22 | dchrzrhcl 26609 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β (πβ(πΏβπ)) β β) |
24 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ΄))
β π β
β) |
25 | 24 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
26 | 25 | nncnd 12176 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
27 | 25 | nnne0d 12210 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β π β 0) |
28 | 23, 26, 27 | divcld 11938 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β ((πβ(πΏβπ)) / π) β β) |
29 | 24 | nnrpd 12962 |
. . . . . . . . 9
β’ (π β
(1...(ββπ΄))
β π β
β+) |
30 | | rpdivcl 12947 |
. . . . . . . . 9
β’ ((π΄ β β+
β§ π β
β+) β (π΄ / π) β
β+) |
31 | 8, 29, 30 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β (π΄ / π) β
β+) |
32 | 31 | relogcld 25994 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β (logβ(π΄ / π)) β β) |
33 | 32 | recnd 11190 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β (logβ(π΄ / π)) β β) |
34 | 28, 33 | mulcld 11182 |
. . . . 5
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) / π) Β· (logβ(π΄ / π))) β β) |
35 | 34 | adantrr 716 |
. . . 4
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β (((πβ(πΏβπ)) / π) Β· (logβ(π΄ / π))) β β) |
36 | 14, 35 | mulcld 11182 |
. . 3
β’ ((π β§ (π β (1...(ββπ΄)) β§ π β {π₯ β β β£ π₯ β₯ π})) β ((ΞΌβπ) Β· (((πβ(πΏβπ)) / π) Β· (logβ(π΄ / π)))) β β) |
37 | 7, 9, 36 | dvdsflsumcom 26553 |
. 2
β’ (π β Ξ£π β (1...(ββπ΄))Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (((πβ(πΏβπ)) / π) Β· (logβ(π΄ / π)))) = Ξ£π β (1...(ββπ΄))Ξ£π β (1...(ββ(π΄ / π)))((ΞΌβπ) Β· (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π)))))) |
38 | | 2fveq3 6852 |
. . . . . 6
β’ (π = 1 β (πβ(πΏβπ)) = (πβ(πΏβ1))) |
39 | | id 22 |
. . . . . 6
β’ (π = 1 β π = 1) |
40 | 38, 39 | oveq12d 7380 |
. . . . 5
β’ (π = 1 β ((πβ(πΏβπ)) / π) = ((πβ(πΏβ1)) / 1)) |
41 | | oveq2 7370 |
. . . . . 6
β’ (π = 1 β (π΄ / π) = (π΄ / 1)) |
42 | 41 | fveq2d 6851 |
. . . . 5
β’ (π = 1 β (logβ(π΄ / π)) = (logβ(π΄ / 1))) |
43 | 40, 42 | oveq12d 7380 |
. . . 4
β’ (π = 1 β (((πβ(πΏβπ)) / π) Β· (logβ(π΄ / π))) = (((πβ(πΏβ1)) / 1) Β· (logβ(π΄ / 1)))) |
44 | | fzfid 13885 |
. . . 4
β’ (π β (1...(ββπ΄)) β Fin) |
45 | | fz1ssnn 13479 |
. . . . 5
β’
(1...(ββπ΄)) β β |
46 | 45 | a1i 11 |
. . . 4
β’ (π β (1...(ββπ΄)) β
β) |
47 | | dchrvmasum2.2 |
. . . . . . 7
β’ (π β 1 β€ π΄) |
48 | | flge1nn 13733 |
. . . . . . 7
β’ ((π΄ β β β§ 1 β€
π΄) β
(ββπ΄) β
β) |
49 | 9, 47, 48 | syl2anc 585 |
. . . . . 6
β’ (π β (ββπ΄) β
β) |
50 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
51 | 49, 50 | eleqtrdi 2848 |
. . . . 5
β’ (π β (ββπ΄) β
(β€β₯β1)) |
52 | | eluzfz1 13455 |
. . . . 5
β’
((ββπ΄)
β (β€β₯β1) β 1 β
(1...(ββπ΄))) |
53 | 51, 52 | syl 17 |
. . . 4
β’ (π β 1 β
(1...(ββπ΄))) |
54 | 43, 44, 46, 53, 34 | musumsum 26557 |
. . 3
β’ (π β Ξ£π β (1...(ββπ΄))Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (((πβ(πΏβπ)) / π) Β· (logβ(π΄ / π)))) = (((πβ(πΏβ1)) / 1) Β· (logβ(π΄ / 1)))) |
55 | 15, 16, 17, 18, 19 | dchrzrh1 26608 |
. . . . . 6
β’ (π β (πβ(πΏβ1)) = 1) |
56 | 55 | oveq1d 7377 |
. . . . 5
β’ (π β ((πβ(πΏβ1)) / 1) = (1 / 1)) |
57 | | 1div1e1 11852 |
. . . . 5
β’ (1 / 1) =
1 |
58 | 56, 57 | eqtrdi 2793 |
. . . 4
β’ (π β ((πβ(πΏβ1)) / 1) = 1) |
59 | 8 | rpcnd 12966 |
. . . . . 6
β’ (π β π΄ β β) |
60 | 59 | div1d 11930 |
. . . . 5
β’ (π β (π΄ / 1) = π΄) |
61 | 60 | fveq2d 6851 |
. . . 4
β’ (π β (logβ(π΄ / 1)) = (logβπ΄)) |
62 | 58, 61 | oveq12d 7380 |
. . 3
β’ (π β (((πβ(πΏβ1)) / 1) Β· (logβ(π΄ / 1))) = (1 Β·
(logβπ΄))) |
63 | 8 | relogcld 25994 |
. . . . 5
β’ (π β (logβπ΄) β
β) |
64 | 63 | recnd 11190 |
. . . 4
β’ (π β (logβπ΄) β
β) |
65 | 64 | mulid2d 11180 |
. . 3
β’ (π β (1 Β·
(logβπ΄)) =
(logβπ΄)) |
66 | 54, 62, 65 | 3eqtrrd 2782 |
. 2
β’ (π β (logβπ΄) = Ξ£π β (1...(ββπ΄))Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (((πβ(πΏβπ)) / π) Β· (logβ(π΄ / π))))) |
67 | | fzfid 13885 |
. . . . 5
β’ ((π β§ π β (1...(ββπ΄))) β (1...(ββ(π΄ / π))) β Fin) |
68 | 19 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β π β π·) |
69 | | elfzelz 13448 |
. . . . . . . 8
β’ (π β
(1...(ββπ΄))
β π β
β€) |
70 | 69 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β π β β€) |
71 | 15, 16, 17, 18, 68, 70 | dchrzrhcl 26609 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β (πβ(πΏβπ)) β β) |
72 | | fznnfl 13774 |
. . . . . . . . . . . 12
β’ (π΄ β β β (π β
(1...(ββπ΄))
β (π β β
β§ π β€ π΄))) |
73 | 9, 72 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π β (1...(ββπ΄)) β (π β β β§ π β€ π΄))) |
74 | 73 | simprbda 500 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββπ΄))) β π β β) |
75 | 74, 12 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (1...(ββπ΄))) β (ΞΌβπ) β β€) |
76 | 75 | zred 12614 |
. . . . . . . 8
β’ ((π β§ π β (1...(ββπ΄))) β (ΞΌβπ) β β) |
77 | 76, 74 | nndivred 12214 |
. . . . . . 7
β’ ((π β§ π β (1...(ββπ΄))) β ((ΞΌβπ) / π) β β) |
78 | 77 | recnd 11190 |
. . . . . 6
β’ ((π β§ π β (1...(ββπ΄))) β ((ΞΌβπ) / π) β β) |
79 | 71, 78 | mulcld 11182 |
. . . . 5
β’ ((π β§ π β (1...(ββπ΄))) β ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) β β) |
80 | 19 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β π·) |
81 | | elfzelz 13448 |
. . . . . . . 8
β’ (π β
(1...(ββ(π΄ /
π))) β π β
β€) |
82 | 81 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β€) |
83 | 15, 16, 17, 18, 80, 82 | dchrzrhcl 26609 |
. . . . . 6
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (πβ(πΏβπ)) β β) |
84 | | elfznn 13477 |
. . . . . . . . . . . 12
β’ (π β
(1...(ββπ΄))
β π β
β) |
85 | 84 | nnrpd 12962 |
. . . . . . . . . . 11
β’ (π β
(1...(ββπ΄))
β π β
β+) |
86 | | rpdivcl 12947 |
. . . . . . . . . . 11
β’ ((π΄ β β+
β§ π β
β+) β (π΄ / π) β
β+) |
87 | 8, 85, 86 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββπ΄))) β (π΄ / π) β
β+) |
88 | | elfznn 13477 |
. . . . . . . . . . 11
β’ (π β
(1...(ββ(π΄ /
π))) β π β
β) |
89 | 88 | nnrpd 12962 |
. . . . . . . . . 10
β’ (π β
(1...(ββ(π΄ /
π))) β π β
β+) |
90 | | rpdivcl 12947 |
. . . . . . . . . 10
β’ (((π΄ / π) β β+ β§ π β β+)
β ((π΄ / π) / π) β
β+) |
91 | 87, 89, 90 | syl2an 597 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((π΄ / π) / π) β
β+) |
92 | 91 | relogcld 25994 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβ((π΄ / π) / π)) β β) |
93 | 88 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β) |
94 | 92, 93 | nndivred 12214 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβ((π΄ / π) / π)) / π) β β) |
95 | 94 | recnd 11190 |
. . . . . 6
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((logβ((π΄ / π) / π)) / π) β β) |
96 | 83, 95 | mulcld 11182 |
. . . . 5
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)) β β) |
97 | 67, 79, 96 | fsummulc2 15676 |
. . . 4
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))) = Ξ£π β (1...(ββ(π΄ / π)))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) |
98 | 71 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (πβ(πΏβπ)) β β) |
99 | 76 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (ΞΌβπ) β β) |
100 | 99 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (ΞΌβπ) β β) |
101 | 74 | nnrpd 12962 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(ββπ΄))) β π β β+) |
102 | 101 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β+) |
103 | 102 | rpcnne0d 12973 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (π β β β§ π β 0)) |
104 | | div12 11842 |
. . . . . . . 8
β’ (((πβ(πΏβπ)) β β β§ (ΞΌβπ) β β β§ (π β β β§ π β 0)) β ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) = ((ΞΌβπ) Β· ((πβ(πΏβπ)) / π))) |
105 | 98, 100, 103, 104 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) = ((ΞΌβπ) Β· ((πβ(πΏβπ)) / π))) |
106 | 92 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβ((π΄ / π) / π)) β β) |
107 | 93 | nnrpd 12962 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β+) |
108 | 107 | rpcnne0d 12973 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (π β β β§ π β 0)) |
109 | | div12 11842 |
. . . . . . . 8
β’ (((πβ(πΏβπ)) β β β§ (logβ((π΄ / π) / π)) β β β§ (π β β β§ π β 0)) β ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)) = ((logβ((π΄ / π) / π)) Β· ((πβ(πΏβπ)) / π))) |
110 | 83, 106, 108, 109 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)) = ((logβ((π΄ / π) / π)) Β· ((πβ(πΏβπ)) / π))) |
111 | 105, 110 | oveq12d 7380 |
. . . . . 6
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))) = (((ΞΌβπ) Β· ((πβ(πΏβπ)) / π)) Β· ((logβ((π΄ / π) / π)) Β· ((πβ(πΏβπ)) / π)))) |
112 | 102 | rpcnd 12966 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β) |
113 | 102 | rpne0d 12969 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β 0) |
114 | 98, 112, 113 | divcld 11938 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) / π) β β) |
115 | 93 | nncnd 12176 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β) |
116 | 93 | nnne0d 12210 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β 0) |
117 | 83, 115, 116 | divcld 11938 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβπ)) / π) β β) |
118 | 114, 117 | mulcld 11182 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)) β β) |
119 | 100, 106,
118 | mulassd 11185 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((ΞΌβπ) Β· (logβ((π΄ / π) / π))) Β· (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π))) = ((ΞΌβπ) Β· ((logβ((π΄ / π) / π)) Β· (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π))))) |
120 | 100, 114,
106, 117 | mul4d 11374 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((ΞΌβπ) Β· ((πβ(πΏβπ)) / π)) Β· ((logβ((π΄ / π) / π)) Β· ((πβ(πΏβπ)) / π))) = (((ΞΌβπ) Β· (logβ((π΄ / π) / π))) Β· (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)))) |
121 | 69 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π β β€) |
122 | 15, 16, 17, 18, 80, 121, 82 | dchrzrhmul 26610 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (πβ(πΏβ(π Β· π))) = ((πβ(πΏβπ)) Β· (πβ(πΏβπ)))) |
123 | 122 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβ(π Β· π))) / (π Β· π)) = (((πβ(πΏβπ)) Β· (πβ(πΏβπ))) / (π Β· π))) |
124 | | divmuldiv 11862 |
. . . . . . . . . . . 12
β’ ((((πβ(πΏβπ)) β β β§ (πβ(πΏβπ)) β β) β§ ((π β β β§ π β 0) β§ (π β β β§ π β 0))) β (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)) = (((πβ(πΏβπ)) Β· (πβ(πΏβπ))) / (π Β· π))) |
125 | 98, 83, 103, 108, 124 | syl22anc 838 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)) = (((πβ(πΏβπ)) Β· (πβ(πΏβπ))) / (π Β· π))) |
126 | 123, 125 | eqtr4d 2780 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((πβ(πΏβ(π Β· π))) / (π Β· π)) = (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π))) |
127 | 59 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β π΄ β β) |
128 | | divdiv1 11873 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ (π β β β§ π β 0) β§ (π β β β§ π β 0)) β ((π΄ / π) / π) = (π΄ / (π Β· π))) |
129 | 127, 103,
108, 128 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((π΄ / π) / π) = (π΄ / (π Β· π))) |
130 | 129 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (π΄ / (π Β· π)) = ((π΄ / π) / π)) |
131 | 130 | fveq2d 6851 |
. . . . . . . . . 10
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (logβ(π΄ / (π Β· π))) = (logβ((π΄ / π) / π))) |
132 | 126, 131 | oveq12d 7380 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π)))) = ((((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)) Β· (logβ((π΄ / π) / π)))) |
133 | 118, 106 | mulcomd 11183 |
. . . . . . . . 9
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)) Β· (logβ((π΄ / π) / π))) = ((logβ((π΄ / π) / π)) Β· (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)))) |
134 | 132, 133 | eqtrd 2777 |
. . . . . . . 8
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π)))) = ((logβ((π΄ / π) / π)) Β· (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)))) |
135 | 134 | oveq2d 7378 |
. . . . . . 7
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β ((ΞΌβπ) Β· (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π))))) = ((ΞΌβπ) Β· ((logβ((π΄ / π) / π)) Β· (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π))))) |
136 | 119, 120,
135 | 3eqtr4d 2787 |
. . . . . 6
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((ΞΌβπ) Β· ((πβ(πΏβπ)) / π)) Β· ((logβ((π΄ / π) / π)) Β· ((πβ(πΏβπ)) / π))) = ((ΞΌβπ) Β· (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π)))))) |
137 | 111, 136 | eqtrd 2777 |
. . . . 5
β’ (((π β§ π β (1...(ββπ΄))) β§ π β (1...(ββ(π΄ / π)))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))) = ((ΞΌβπ) Β· (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π)))))) |
138 | 137 | sumeq2dv 15595 |
. . . 4
β’ ((π β§ π β (1...(ββπ΄))) β Ξ£π β (1...(ββ(π΄ / π)))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))) = Ξ£π β (1...(ββ(π΄ / π)))((ΞΌβπ) Β· (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π)))))) |
139 | 97, 138 | eqtrd 2777 |
. . 3
β’ ((π β§ π β (1...(ββπ΄))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))) = Ξ£π β (1...(ββ(π΄ / π)))((ΞΌβπ) Β· (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π)))))) |
140 | 139 | sumeq2dv 15595 |
. 2
β’ (π β Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π))) = Ξ£π β (1...(ββπ΄))Ξ£π β (1...(ββ(π΄ / π)))((ΞΌβπ) Β· (((πβ(πΏβ(π Β· π))) / (π Β· π)) Β· (logβ(π΄ / (π Β· π)))))) |
141 | 37, 66, 140 | 3eqtr4d 2787 |
1
β’ (π β (logβπ΄) = Ξ£π β (1...(ββπ΄))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π΄ / π)))((πβ(πΏβπ)) Β· ((logβ((π΄ / π) / π)) / π)))) |