Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (Ξβπ) = (Ξβπ)) |
2 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π = π β (π₯ / π) = (π₯ / π)) |
3 | 2 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π = π β (Οβ(π₯ / π)) = (Οβ(π₯ / π))) |
4 | 1, 3 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π = π β ((Ξβπ) Β· (Οβ(π₯ / π))) = ((Ξβπ) Β· (Οβ(π₯ / π)))) |
5 | 4 | cbvsumv 15588 |
. . . . . . . . . . 11
β’
Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· (Οβ(π₯ / π))) = Ξ£π β (1...(ββπ₯))((Ξβπ) Β· (Οβ(π₯ / π))) |
6 | | fzfid 13885 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (1...(ββ(π₯ / π))) β Fin) |
7 | | elfznn 13477 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(1...(ββπ₯))
β π β
β) |
8 | 7 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β π β
β) |
9 | | vmacl 26483 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
(Ξβπ) β
β) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Ξβπ)
β β) |
11 | 10 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Ξβπ)
β β) |
12 | | elfznn 13477 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(1...(ββ(π₯ /
π))) β π β
β) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
14 | | vmacl 26483 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
(Ξβπ) β
β) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(Ξβπ) β
β) |
16 | 15 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(Ξβπ) β
β) |
17 | 6, 11, 16 | fsummulc2 15676 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
Β· Ξ£π β
(1...(ββ(π₯ /
π)))(Ξβπ)) = Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (Ξβπ))) |
18 | 7 | nnrpd 12962 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(1...(ββπ₯))
β π β
β+) |
19 | | rpdivcl 12947 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β+
β§ π β
β+) β (π₯ / π) β
β+) |
20 | 18, 19 | sylan2 594 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
21 | 20 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β) |
22 | | chpval 26487 |
. . . . . . . . . . . . . . 15
β’ ((π₯ / π) β β β (Οβ(π₯ / π)) = Ξ£π β (1...(ββ(π₯ / π)))(Ξβπ)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Οβ(π₯ /
π)) = Ξ£π β
(1...(ββ(π₯ /
π)))(Ξβπ)) |
24 | 23 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
Β· (Οβ(π₯ /
π))) =
((Ξβπ)
Β· Ξ£π β
(1...(ββ(π₯ /
π)))(Ξβπ))) |
25 | 13 | nncnd 12176 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
26 | 7 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
27 | 26 | nncnd 12176 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
28 | 26 | nnne0d 12210 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β 0) |
29 | 25, 27, 28 | divcan3d 11943 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β ((π Β· π) / π) = π) |
30 | 29 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(Ξβ((π
Β· π) / π)) = (Ξβπ)) |
31 | 30 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((Ξβπ)
Β· (Ξβ((π Β· π) / π))) = ((Ξβπ) Β· (Ξβπ))) |
32 | 31 | sumeq2dv 15595 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β·
(Ξβ((π
Β· π) / π))) = Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (Ξβπ))) |
33 | 17, 24, 32 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
Β· (Οβ(π₯ /
π))) = Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) Β·
(Ξβ((π
Β· π) / π)))) |
34 | 33 | sumeq2dv 15595 |
. . . . . . . . . . 11
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· (Οβ(π₯ / π))) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (Ξβ((π Β· π) / π)))) |
35 | 5, 34 | eqtrid 2789 |
. . . . . . . . . 10
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· (Οβ(π₯ / π))) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (Ξβ((π Β· π) / π)))) |
36 | | fvoveq1 7385 |
. . . . . . . . . . . 12
β’ (π = (π Β· π) β (Ξβ(π / π)) = (Ξβ((π Β· π) / π))) |
37 | 36 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = (π Β· π) β ((Ξβπ) Β· (Ξβ(π / π))) = ((Ξβπ) Β· (Ξβ((π Β· π) / π)))) |
38 | | rpre 12930 |
. . . . . . . . . . 11
β’ (π₯ β β+
β π₯ β
β) |
39 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . 17
β’ {π¦ β β β£ π¦ β₯ π} β β |
40 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β {π¦ β β β£ π¦ β₯ π}) |
41 | 39, 40 | sselid 3947 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β) |
42 | 41 | anassrs 469 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β {π¦ β β β£ π¦ β₯ π}) β π β β) |
43 | 42, 9 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β {π¦ β β β£ π¦ β₯ π}) β (Ξβπ) β β) |
44 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(1...(ββπ₯))
β π β
β) |
45 | 44 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β π β
β) |
46 | | dvdsdivcl 16205 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β {π¦ β β β£ π¦ β₯ π}) |
47 | 45, 46 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β {π¦ β β β£ π¦ β₯ π}) |
48 | 39, 47 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β {π¦ β β β£ π¦ β₯ π}) β (π / π) β β) |
49 | | vmacl 26483 |
. . . . . . . . . . . . . . 15
β’ ((π / π) β β β
(Ξβ(π / π)) β
β) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β {π¦ β β β£ π¦ β₯ π}) β (Ξβ(π / π)) β β) |
51 | 43, 50 | remulcld 11192 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β {π¦ β β β£ π¦ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) β β) |
52 | 51 | recnd 11190 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β {π¦ β β β£ π¦ β₯ π}) β ((Ξβπ) Β· (Ξβ(π / π))) β β) |
53 | 52 | anasss 468 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β ((Ξβπ) Β·
(Ξβ(π / π))) β
β) |
54 | 37, 38, 53 | dvdsflsumcom 26553 |
. . . . . . . . . 10
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) Β· (Ξβ((π Β· π) / π)))) |
55 | 35, 54 | eqtr4d 2780 |
. . . . . . . . 9
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· (Οβ(π₯ / π))) = Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) |
56 | 55 | oveq1d 7377 |
. . . . . . . 8
β’ (π₯ β β+
β (Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· (Οβ(π₯ / π))) + Ξ£π β (1...(ββπ₯))((Ξβπ) Β· (logβπ))) = (Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + Ξ£π β (1...(ββπ₯))((Ξβπ) Β· (logβπ)))) |
57 | | fzfid 13885 |
. . . . . . . . 9
β’ (π₯ β β+
β (1...(ββπ₯)) β Fin) |
58 | | vmacl 26483 |
. . . . . . . . . . . 12
β’ (π β β β
(Ξβπ) β
β) |
59 | 45, 58 | syl 17 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Ξβπ)
β β) |
60 | 59 | recnd 11190 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Ξβπ)
β β) |
61 | 44 | nnrpd 12962 |
. . . . . . . . . . . . . 14
β’ (π β
(1...(ββπ₯))
β π β
β+) |
62 | | rpdivcl 12947 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ π β
β+) β (π₯ / π) β
β+) |
63 | 61, 62 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
64 | 63 | rpred 12964 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β) |
65 | | chpcl 26489 |
. . . . . . . . . . . 12
β’ ((π₯ / π) β β β (Οβ(π₯ / π)) β β) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Οβ(π₯ /
π)) β
β) |
67 | 66 | recnd 11190 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (Οβ(π₯ /
π)) β
β) |
68 | 60, 67 | mulcld 11182 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
Β· (Οβ(π₯ /
π))) β
β) |
69 | 45 | nnrpd 12962 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β π β
β+) |
70 | | relogcl 25947 |
. . . . . . . . . . . 12
β’ (π β β+
β (logβπ) β
β) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (logβπ) β
β) |
72 | 71 | recnd 11190 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (logβπ) β
β) |
73 | 60, 72 | mulcld 11182 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
Β· (logβπ))
β β) |
74 | 57, 68, 73 | fsumadd 15632 |
. . . . . . . 8
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(((Ξβπ) Β· (Οβ(π₯ / π))) + ((Ξβπ) Β· (logβπ))) = (Ξ£π β (1...(ββπ₯))((Ξβπ) Β· (Οβ(π₯ / π))) + Ξ£π β (1...(ββπ₯))((Ξβπ) Β· (logβπ)))) |
75 | | fzfid 13885 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (1...π) β
Fin) |
76 | | dvdsssfz1 16207 |
. . . . . . . . . . . . 13
β’ (π β β β {π¦ β β β£ π¦ β₯ π} β (1...π)) |
77 | 45, 76 | syl 17 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β {π¦ β β
β£ π¦ β₯ π} β (1...π)) |
78 | 75, 77 | ssfid 9218 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β {π¦ β β
β£ π¦ β₯ π} β Fin) |
79 | 78, 51 | fsumrecl 15626 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β Ξ£π β
{π¦ β β β£
π¦ β₯ π} ((Ξβπ) Β·
(Ξβ(π / π))) β
β) |
80 | 79 | recnd 11190 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β Ξ£π β
{π¦ β β β£
π¦ β₯ π} ((Ξβπ) Β·
(Ξβ(π / π))) β
β) |
81 | 57, 80, 73 | fsumadd 15632 |
. . . . . . . 8
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ))) = (Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + Ξ£π β (1...(ββπ₯))((Ξβπ) Β· (logβπ)))) |
82 | 56, 74, 81 | 3eqtr4d 2787 |
. . . . . . 7
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(((Ξβπ) Β· (Οβ(π₯ / π))) + ((Ξβπ) Β· (logβπ))) = Ξ£π β (1...(ββπ₯))(Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
83 | 72, 67 | addcomd 11364 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((logβπ) +
(Οβ(π₯ / π))) = ((Οβ(π₯ / π)) + (logβπ))) |
84 | 83 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
Β· ((logβπ) +
(Οβ(π₯ / π)))) = ((Ξβπ) Β· ((Οβ(π₯ / π)) + (logβπ)))) |
85 | 60, 67, 72 | adddid 11186 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
Β· ((Οβ(π₯ /
π)) + (logβπ))) = (((Ξβπ) Β· (Οβ(π₯ / π))) + ((Ξβπ) Β· (logβπ)))) |
86 | 84, 85 | eqtrd 2777 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
Β· ((logβπ) +
(Οβ(π₯ / π)))) = (((Ξβπ) Β· (Οβ(π₯ / π))) + ((Ξβπ) Β· (logβπ)))) |
87 | 86 | sumeq2dv 15595 |
. . . . . . 7
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· ((logβπ) + (Οβ(π₯ / π)))) = Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (Οβ(π₯ / π))) + ((Ξβπ) Β· (logβπ)))) |
88 | | logsqvma2 26907 |
. . . . . . . . 9
β’ (π β β β
Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) = (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
89 | 45, 88 | syl 17 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β Ξ£π β
{π¦ β β β£
π¦ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) = (Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
90 | 89 | sumeq2dv 15595 |
. . . . . . 7
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) = Ξ£π β (1...(ββπ₯))(Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))) + ((Ξβπ) Β· (logβπ)))) |
91 | 82, 87, 90 | 3eqtr4d 2787 |
. . . . . 6
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· ((logβπ) + (Οβ(π₯ / π)))) = Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2))) |
92 | | fvoveq1 7385 |
. . . . . . . . 9
β’ (π = (π Β· π) β (logβ(π / π)) = (logβ((π Β· π) / π))) |
93 | 92 | oveq1d 7377 |
. . . . . . . 8
β’ (π = (π Β· π) β ((logβ(π / π))β2) = ((logβ((π Β· π) / π))β2)) |
94 | 93 | oveq2d 7378 |
. . . . . . 7
β’ (π = (π Β· π) β ((ΞΌβπ) Β· ((logβ(π / π))β2)) = ((ΞΌβπ) Β· ((logβ((π Β· π) / π))β2))) |
95 | | mucl 26506 |
. . . . . . . . . 10
β’ (π β β β
(ΞΌβπ) β
β€) |
96 | 41, 95 | syl 17 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β€) |
97 | 96 | zcnd 12615 |
. . . . . . . 8
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β) |
98 | 61 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β+) |
99 | 41 | nnrpd 12962 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β+) |
100 | 98, 99 | rpdivcld 12981 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (π / π) β
β+) |
101 | | relogcl 25947 |
. . . . . . . . . . 11
β’ ((π / π) β β+ β
(logβ(π / π)) β
β) |
102 | 101 | recnd 11190 |
. . . . . . . . . 10
β’ ((π / π) β β+ β
(logβ(π / π)) β
β) |
103 | 100, 102 | syl 17 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (logβ(π / π)) β β) |
104 | 103 | sqcld 14056 |
. . . . . . . 8
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β ((logβ(π / π))β2) β β) |
105 | 97, 104 | mulcld 11182 |
. . . . . . 7
β’ ((π₯ β β+
β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β ((ΞΌβπ) Β· ((logβ(π / π))β2)) β β) |
106 | 94, 38, 105 | dvdsflsumcom 26553 |
. . . . . 6
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((logβ(π / π))β2)) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβ((π Β· π) / π))β2))) |
107 | 29 | fveq2d 6851 |
. . . . . . . . . 10
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(logβ((π Β·
π) / π)) = (logβπ)) |
108 | 107 | oveq1d 7377 |
. . . . . . . . 9
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((logβ((π Β·
π) / π))β2) = ((logβπ)β2)) |
109 | 108 | oveq2d 7378 |
. . . . . . . 8
β’ (((π₯ β β+
β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((ΞΌβπ) Β·
((logβ((π Β·
π) / π))β2)) = ((ΞΌβπ) Β· ((logβπ)β2))) |
110 | 109 | sumeq2dv 15595 |
. . . . . . 7
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))((ΞΌβπ) Β· ((logβ((π Β· π) / π))β2)) = Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβπ)β2))) |
111 | 110 | sumeq2dv 15595 |
. . . . . 6
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβ((π Β· π) / π))β2)) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβπ)β2))) |
112 | 91, 106, 111 | 3eqtrd 2781 |
. . . . 5
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· ((logβπ) + (Οβ(π₯ / π)))) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβπ)β2))) |
113 | 112 | oveq1d 7377 |
. . . 4
β’ (π₯ β β+
β (Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· ((logβπ) + (Οβ(π₯ / π)))) / π₯) = (Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβπ)β2)) / π₯)) |
114 | 113 | oveq1d 7377 |
. . 3
β’ (π₯ β β+
β ((Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· ((logβπ) + (Οβ(π₯ / π)))) / π₯) β (2 Β· (logβπ₯))) = ((Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβπ)β2)) / π₯) β (2 Β· (logβπ₯)))) |
115 | 114 | mpteq2ia 5213 |
. 2
β’ (π₯ β β+
β¦ ((Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· ((logβπ) + (Οβ(π₯ / π)))) / π₯) β (2 Β· (logβπ₯)))) = (π₯ β β+ β¦
((Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβπ)β2)) / π₯) β (2 Β· (logβπ₯)))) |
116 | | eqid 2737 |
. . 3
β’
((((logβ(π₯ /
π))β2) + (2 β (2
Β· (logβ(π₯ /
π))))) / π) = ((((logβ(π₯ / π))β2) + (2 β (2 Β·
(logβ(π₯ / π))))) / π) |
117 | 116 | selberglem2 26910 |
. 2
β’ (π₯ β β+
β¦ ((Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβπ)β2)) / π₯) β (2 Β· (logβπ₯)))) β
π(1) |
118 | 115, 117 | eqeltri 2834 |
1
β’ (π₯ β β+
β¦ ((Ξ£π β
(1...(ββπ₯))((Ξβπ) Β· ((logβπ) + (Οβ(π₯ / π)))) / π₯) β (2 Β· (logβπ₯)))) β
π(1) |