Step | Hyp | Ref
| Expression |
1 | | rpssre 12977 |
. . . 4
β’
β+ β β |
2 | | ax-1cn 11164 |
. . . 4
β’ 1 β
β |
3 | | o1const 15560 |
. . . 4
β’
((β+ β β β§ 1 β β) β
(π₯ β
β+ β¦ 1) β π(1)) |
4 | 1, 2, 3 | mp2an 691 |
. . 3
β’ (π₯ β β+
β¦ 1) β π(1) |
5 | | 1cnd 11205 |
. . . 4
β’
((β€ β§ π₯
β β+) β 1 β β) |
6 | | fzfid 13934 |
. . . . . 6
β’ (π₯ β β+
β (1...(ββπ₯)) β Fin) |
7 | | elfznn 13526 |
. . . . . . . . . . . 12
β’ (π β
(1...(ββπ₯))
β π β
β) |
8 | 7 | adantl 483 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β π β
β) |
9 | | mucl 26625 |
. . . . . . . . . . 11
β’ (π β β β
(ΞΌβπ) β
β€) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β€) |
11 | 10 | zred 12662 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
12 | 11, 8 | nndivred 12262 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
13 | 7 | nnrpd 13010 |
. . . . . . . . . 10
β’ (π β
(1...(ββπ₯))
β π β
β+) |
14 | | rpdivcl 12995 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
β+) β (π₯ / π) β
β+) |
15 | 13, 14 | sylan2 594 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
16 | 15 | relogcld 26113 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
17 | 12, 16 | remulcld 11240 |
. . . . . . 7
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β·
(logβ(π₯ / π))) β
β) |
18 | 17 | recnd 11238 |
. . . . . 6
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β·
(logβ(π₯ / π))) β
β) |
19 | 6, 18 | fsumcl 15675 |
. . . . 5
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π))) β β) |
20 | 19 | adantl 483 |
. . . 4
β’
((β€ β§ π₯
β β+) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π))) β β) |
21 | | mulogsumlem 27014 |
. . . . 5
β’ (π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π))))) β π(1) |
22 | | sumex 15630 |
. . . . . . . 8
β’
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β V |
23 | 22 | a1i 11 |
. . . . . . 7
β’
((β€ β§ π₯
β β+) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β V) |
24 | 21 | a1i 11 |
. . . . . . 7
β’ (β€
β (π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π))))) β π(1)) |
25 | 23, 24 | o1mptrcl 15563 |
. . . . . 6
β’
((β€ β§ π₯
β β+) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β β) |
26 | 5, 20 | subcld 11567 |
. . . . . 6
β’
((β€ β§ π₯
β β+) β (1 β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π)))) β β) |
27 | | 1red 11211 |
. . . . . 6
β’ (β€
β 1 β β) |
28 | | fz1ssnn 13528 |
. . . . . . . . . . . . . . . 16
β’
(1...(ββπ₯)) β β |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(1...(ββπ₯))
β β) |
30 | 29 | sselda 3981 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β π β
β) |
31 | 30, 9 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β€) |
32 | 31 | zred 12662 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
33 | 32, 30 | nndivred 12262 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
34 | 33 | recnd 11238 |
. . . . . . . . . 10
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
35 | | fzfid 13934 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (1...(ββ(π₯ / π))) β Fin) |
36 | | elfznn 13526 |
. . . . . . . . . . . . . . 15
β’ (π β
(1...(ββ(π₯ /
π))) β π β
β) |
37 | 36 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
38 | 37 | nnrpd 13010 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β+) |
39 | 38 | rpcnne0d 13021 |
. . . . . . . . . . . 12
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (π β β β§ π β 0)) |
40 | | reccl 11875 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β 0) β (1 / π) β
β) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (1 / π) β
β) |
42 | 35, 41 | fsumcl 15675 |
. . . . . . . . . 10
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β β) |
43 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ 1 β€ π₯) β
π₯ β
β+) |
44 | 43, 13, 14 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
45 | 44 | relogcld 26113 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
46 | 45 | recnd 11238 |
. . . . . . . . . 10
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
47 | 34, 42, 46 | subdid 11666 |
. . . . . . . . 9
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π)))) = ((((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π)) β (((ΞΌβπ) / π) Β· (logβ(π₯ / π))))) |
48 | 47 | sumeq2dv 15645 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) = Ξ£π β (1...(ββπ₯))((((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π)) β (((ΞΌβπ) / π) Β· (logβ(π₯ / π))))) |
49 | | fzfid 13934 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(1...(ββπ₯))
β Fin) |
50 | 34, 42 | mulcld 11230 |
. . . . . . . . 9
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π)) β β) |
51 | 18 | adantlr 714 |
. . . . . . . . 9
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β·
(logβ(π₯ / π))) β
β) |
52 | 49, 50, 51 | fsumsub 15730 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))((((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π)) β (((ΞΌβπ) / π) Β· (logβ(π₯ / π)))) = (Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π)) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π))))) |
53 | | oveq2 7412 |
. . . . . . . . . . . 12
β’ (π = (π Β· π) β (1 / π) = (1 / (π Β· π))) |
54 | 53 | oveq2d 7420 |
. . . . . . . . . . 11
β’ (π = (π Β· π) β ((ΞΌβπ) Β· (1 / π)) = ((ΞΌβπ) Β· (1 / (π Β· π)))) |
55 | | rpre 12978 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β π₯ β
β) |
56 | 55 | adantr 482 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 1 β€ π₯) β
π₯ β
β) |
57 | | ssrab2 4076 |
. . . . . . . . . . . . . . 15
β’ {π¦ β β β£ π¦ β₯ π} β β |
58 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β {π¦ β β β£ π¦ β₯ π}) |
59 | 57, 58 | sselid 3979 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β) |
60 | 59, 9 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β€) |
61 | 60 | zcnd 12663 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β) |
62 | | elfznn 13526 |
. . . . . . . . . . . . . . . 16
β’ (π β
(1...(ββπ₯))
β π β
β) |
63 | 62 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β π β
β) |
64 | 63 | nnrecred 12259 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
65 | 64 | recnd 11238 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
66 | 65 | adantrr 716 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (1 / π) β β) |
67 | 61, 66 | mulcld 11230 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β ((ΞΌβπ) Β· (1 / π)) β β) |
68 | 54, 56, 67 | dvdsflsumcom 26672 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· (1 / π)) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· (1 / (π Β· π)))) |
69 | | oveq2 7412 |
. . . . . . . . . . . 12
β’ (π = 1 β (1 / π) = (1 / 1)) |
70 | | 1div1e1 11900 |
. . . . . . . . . . . 12
β’ (1 / 1) =
1 |
71 | 69, 70 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (π = 1 β (1 / π) = 1) |
72 | | flge1nn 13782 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ 1 β€
π₯) β
(ββπ₯) β
β) |
73 | 55, 72 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(ββπ₯) β
β) |
74 | | nnuz 12861 |
. . . . . . . . . . . . 13
β’ β =
(β€β₯β1) |
75 | 73, 74 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(ββπ₯) β
(β€β₯β1)) |
76 | | eluzfz1 13504 |
. . . . . . . . . . . 12
β’
((ββπ₯)
β (β€β₯β1) β 1 β
(1...(ββπ₯))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 1 β€ π₯) β 1
β (1...(ββπ₯))) |
78 | 71, 49, 29, 77, 65 | musumsum 26676 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· (1 / π)) = 1) |
79 | 31 | zcnd 12663 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
80 | 79 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(ΞΌβπ) β
β) |
81 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
82 | 81 | nnrpd 13010 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β+) |
83 | 82 | rpcnne0d 13021 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (π β β β§ π β 0)) |
84 | | divdiv1 11921 |
. . . . . . . . . . . . . . 15
β’
(((ΞΌβπ)
β β β§ (π
β β β§ π β
0) β§ (π β β
β§ π β 0)) β
(((ΞΌβπ) / π) / π) = ((ΞΌβπ) / (π Β· π))) |
85 | 80, 83, 39, 84 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(((ΞΌβπ) / π) / π) = ((ΞΌβπ) / (π Β· π))) |
86 | 34 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((ΞΌβπ) / π) β
β) |
87 | 37 | nncnd 12224 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
88 | 37 | nnne0d 12258 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β 0) |
89 | 86, 87, 88 | divrecd 11989 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(((ΞΌβπ) / π) / π) = (((ΞΌβπ) / π) Β· (1 / π))) |
90 | | nnmulcl 12232 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β) β (π Β· π) β β) |
91 | 30, 36, 90 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (π Β· π) β β) |
92 | 91 | nncnd 12224 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (π Β· π) β β) |
93 | 91 | nnne0d 12258 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (π Β· π) β 0) |
94 | 80, 92, 93 | divrecd 11989 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((ΞΌβπ) / (π Β· π)) = ((ΞΌβπ) Β· (1 / (π Β· π)))) |
95 | 85, 89, 94 | 3eqtr3rd 2782 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((ΞΌβπ) Β· (1
/ (π Β· π))) = (((ΞΌβπ) / π) Β· (1 / π))) |
96 | 95 | sumeq2dv 15645 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))((ΞΌβπ) Β· (1 / (π Β· π))) = Ξ£π β (1...(ββ(π₯ / π)))(((ΞΌβπ) / π) Β· (1 / π))) |
97 | 35, 34, 41 | fsummulc2 15726 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π)) = Ξ£π β (1...(ββ(π₯ / π)))(((ΞΌβπ) / π) Β· (1 / π))) |
98 | 96, 97 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))((ΞΌβπ) Β· (1 / (π Β· π))) = (((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π))) |
99 | 98 | sumeq2dv 15645 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· (1 / (π Β· π))) = Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π))) |
100 | 68, 78, 99 | 3eqtr3rd 2782 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π)) = 1) |
101 | 100 | oveq1d 7419 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π)) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π)))) = (1 β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π))))) |
102 | 48, 52, 101 | 3eqtrd 2777 |
. . . . . . 7
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) = (1 β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π))))) |
103 | 102 | adantl 483 |
. . . . . 6
β’
((β€ β§ (π₯
β β+ β§ 1 β€ π₯)) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) = (1 β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π))))) |
104 | 25, 26, 27, 103 | o1eq 15510 |
. . . . 5
β’ (β€
β ((π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π))))) β π(1) β (π₯ β β+
β¦ (1 β Ξ£π
β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π))))) β π(1))) |
105 | 21, 104 | mpbii 232 |
. . . 4
β’ (β€
β (π₯ β
β+ β¦ (1 β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π))))) β π(1)) |
106 | 5, 20, 105 | o1dif 15570 |
. . 3
β’ (β€
β ((π₯ β
β+ β¦ 1) β π(1) β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π)))) β π(1))) |
107 | 4, 106 | mpbii 232 |
. 2
β’ (β€
β (π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π)))) β π(1)) |
108 | 107 | mptru 1549 |
1
β’ (π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· (logβ(π₯ / π)))) β π(1) |