Step | Hyp | Ref
| Expression |
1 | | 1red 11163 |
. 2
β’ (π β 1 β
β) |
2 | | 2re 12234 |
. . . 4
β’ 2 β
β |
3 | | fzfid 13885 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
4 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
5 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ₯))
β π β
β) |
6 | 5 | nnrpd 12962 |
. . . . . . . 8
β’ (π β
(1...(ββπ₯))
β π β
β+) |
7 | | rpdivcl 12947 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
β+) β (π₯ / π) β
β+) |
8 | 4, 6, 7 | syl2an 597 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
9 | 8 | relogcld 25994 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
10 | | simplr 768 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π₯ β
β+) |
11 | 9, 10 | rerpdivcld 12995 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / π₯) β β) |
12 | 3, 11 | fsumrecl 15626 |
. . . 4
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯) β β) |
13 | | remulcl 11143 |
. . . 4
β’ ((2
β β β§ Ξ£π β (1...(ββπ₯))((logβ(π₯ / π)) / π₯) β β) β (2 Β·
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) β β) |
14 | 2, 12, 13 | sylancr 588 |
. . 3
β’ ((π β§ π₯ β β+) β (2
Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) β β) |
15 | | mulog2sumlem2.r |
. . . . . 6
β’ π
= (((1 / 2) + (Ξ³ +
(absβπΏ))) +
Ξ£π β
(1...2)((logβ(e / π))
/ π)) |
16 | | halfre 12374 |
. . . . . . . 8
β’ (1 / 2)
β β |
17 | | emre 26371 |
. . . . . . . . 9
β’ Ξ³
β β |
18 | | mulog2sumlem.1 |
. . . . . . . . . . 11
β’ (π β πΉ βπ πΏ) |
19 | | rlimcl 15392 |
. . . . . . . . . . 11
β’ (πΉ βπ
πΏ β πΏ β β) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
β’ (π β πΏ β β) |
21 | 20 | abscld 15328 |
. . . . . . . . 9
β’ (π β (absβπΏ) β
β) |
22 | | readdcl 11141 |
. . . . . . . . 9
β’ ((Ξ³
β β β§ (absβπΏ) β β) β (Ξ³ +
(absβπΏ)) β
β) |
23 | 17, 21, 22 | sylancr 588 |
. . . . . . . 8
β’ (π β (Ξ³ +
(absβπΏ)) β
β) |
24 | | readdcl 11141 |
. . . . . . . 8
β’ (((1 / 2)
β β β§ (Ξ³ + (absβπΏ)) β β) β ((1 / 2) +
(Ξ³ + (absβπΏ)))
β β) |
25 | 16, 23, 24 | sylancr 588 |
. . . . . . 7
β’ (π β ((1 / 2) + (Ξ³ +
(absβπΏ))) β
β) |
26 | | fzfid 13885 |
. . . . . . . 8
β’ (π β (1...2) β
Fin) |
27 | | epr 16097 |
. . . . . . . . . . 11
β’ e β
β+ |
28 | | elfznn 13477 |
. . . . . . . . . . . . 13
β’ (π β (1...2) β π β
β) |
29 | 28 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...2)) β π β β) |
30 | 29 | nnrpd 12962 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...2)) β π β β+) |
31 | | rpdivcl 12947 |
. . . . . . . . . . 11
β’ ((e
β β+ β§ π β β+) β (e /
π) β
β+) |
32 | 27, 30, 31 | sylancr 588 |
. . . . . . . . . 10
β’ ((π β§ π β (1...2)) β (e / π) β
β+) |
33 | 32 | relogcld 25994 |
. . . . . . . . 9
β’ ((π β§ π β (1...2)) β (logβ(e / π)) β
β) |
34 | 33, 29 | nndivred 12214 |
. . . . . . . 8
β’ ((π β§ π β (1...2)) β ((logβ(e /
π)) / π) β β) |
35 | 26, 34 | fsumrecl 15626 |
. . . . . . 7
β’ (π β Ξ£π β (1...2)((logβ(e / π)) / π) β β) |
36 | 25, 35 | readdcld 11191 |
. . . . . 6
β’ (π β (((1 / 2) + (Ξ³ +
(absβπΏ))) +
Ξ£π β
(1...2)((logβ(e / π))
/ π)) β
β) |
37 | 15, 36 | eqeltrid 2842 |
. . . . 5
β’ (π β π
β β) |
38 | | remulcl 11143 |
. . . . 5
β’ ((π
β β β§ 2 β
β) β (π
Β·
2) β β) |
39 | 37, 2, 38 | sylancl 587 |
. . . 4
β’ (π β (π
Β· 2) β
β) |
40 | 39 | adantr 482 |
. . 3
β’ ((π β§ π₯ β β+) β (π
Β· 2) β
β) |
41 | 2 | a1i 11 |
. . . 4
β’ ((π β§ π₯ β β+) β 2 β
β) |
42 | | rpssre 12929 |
. . . . 5
β’
β+ β β |
43 | | 2cnd 12238 |
. . . . 5
β’ (π β 2 β
β) |
44 | | o1const 15509 |
. . . . 5
β’
((β+ β β β§ 2 β β) β
(π₯ β
β+ β¦ 2) β π(1)) |
45 | 42, 43, 44 | sylancr 588 |
. . . 4
β’ (π β (π₯ β β+ β¦ 2) β
π(1)) |
46 | | logfacrlim2 26590 |
. . . . 5
β’ (π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) βπ
1 |
47 | | rlimo1 15506 |
. . . . 5
β’ ((π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) βπ 1 β
(π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))((logβ(π₯ / π)) / π₯)) β π(1)) |
48 | 46, 47 | mp1i 13 |
. . . 4
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) β π(1)) |
49 | 41, 12, 45, 48 | o1mul2 15514 |
. . 3
β’ (π β (π₯ β β+ β¦ (2
Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯))) β π(1)) |
50 | 39 | recnd 11190 |
. . . 4
β’ (π β (π
Β· 2) β
β) |
51 | | o1const 15509 |
. . . 4
β’
((β+ β β β§ (π
Β· 2) β β) β (π₯ β β+
β¦ (π
Β· 2))
β π(1)) |
52 | 42, 50, 51 | sylancr 588 |
. . 3
β’ (π β (π₯ β β+ β¦ (π
Β· 2)) β
π(1)) |
53 | 14, 40, 49, 52 | o1add2 15513 |
. 2
β’ (π β (π₯ β β+ β¦ ((2
Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2))) β
π(1)) |
54 | 14, 40 | readdcld 11191 |
. 2
β’ ((π β§ π₯ β β+) β ((2
Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2)) β
β) |
55 | 5 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
56 | | mucl 26506 |
. . . . . . . . 9
β’ (π β β β
(ΞΌβπ) β
β€) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β€) |
58 | 57 | zred 12614 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
59 | 58, 55 | nndivred 12214 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
60 | 59 | recnd 11190 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
61 | | mulog2sumlem2.t |
. . . . . 6
β’ π = ((((logβ(π₯ / π))β2) / 2) + ((Ξ³ Β·
(logβ(π₯ / π))) β πΏ)) |
62 | 9 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
63 | 62 | sqcld 14056 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π))β2) β
β) |
64 | 63 | halfcld 12405 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((logβ(π₯ /
π))β2) / 2) β
β) |
65 | | remulcl 11143 |
. . . . . . . . . 10
β’ ((Ξ³
β β β§ (logβ(π₯ / π)) β β) β (Ξ³ Β·
(logβ(π₯ / π))) β
β) |
66 | 17, 9, 65 | sylancr 588 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (Ξ³ Β· (logβ(π₯ / π))) β β) |
67 | 66 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (Ξ³ Β· (logβ(π₯ / π))) β β) |
68 | 20 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β πΏ β
β) |
69 | 67, 68 | subcld 11519 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((Ξ³ Β· (logβ(π₯ / π))) β πΏ) β β) |
70 | 64, 69 | addcld 11181 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((((logβ(π₯ /
π))β2) / 2) +
((Ξ³ Β· (logβ(π₯ / π))) β πΏ)) β β) |
71 | 61, 70 | eqeltrid 2842 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
72 | 60, 71 | mulcld 11182 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· π) β
β) |
73 | 3, 72 | fsumcl 15625 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β β) |
74 | | relogcl 25947 |
. . . . 5
β’ (π₯ β β+
β (logβπ₯) β
β) |
75 | 74 | adantl 483 |
. . . 4
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
76 | 75 | recnd 11190 |
. . 3
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
77 | 73, 76 | subcld 11519 |
. 2
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β (logβπ₯)) β β) |
78 | 77 | abscld 15328 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβ(Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β (logβπ₯))) β β) |
79 | 78 | adantrr 716 |
. . 3
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβ(Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β (logβπ₯))) β β) |
80 | 54 | adantrr 716 |
. . 3
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β ((2 Β·
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2)) β
β) |
81 | 54 | recnd 11190 |
. . . . 5
β’ ((π β§ π₯ β β+) β ((2
Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2)) β
β) |
82 | 81 | abscld 15328 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβ((2 Β· Ξ£π β (1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2))) β
β) |
83 | 82 | adantrr 716 |
. . 3
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (absβ((2
Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2))) β
β) |
84 | 57 | zcnd 12615 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
85 | | fzfid 13885 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1...(ββ(π₯ / π))) β Fin) |
86 | | elfznn 13477 |
. . . . . . . . . . . . . 14
β’ (π β
(1...(ββ(π₯ /
π))) β π β
β) |
87 | | nnrp 12933 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β+) |
88 | | rpdivcl 12947 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ / π) β β+ β§ π β β+)
β ((π₯ / π) / π) β
β+) |
89 | 8, 87, 88 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β ((π₯ / π) / π) β
β+) |
90 | 89 | relogcld 25994 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (logβ((π₯ /
π) / π)) β β) |
91 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β π β
β) |
92 | 90, 91 | nndivred 12214 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β ((logβ((π₯ /
π) / π)) / π) β β) |
93 | 92 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β ((logβ((π₯ /
π) / π)) / π) β β) |
94 | 86, 93 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((logβ((π₯ / π) / π)) / π) β β) |
95 | 85, 94 | fsumcl 15625 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π) β β) |
96 | 71, 95 | subcld 11519 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)) β β) |
97 | 55 | nncnd 12176 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
98 | 55 | nnne0d 12210 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
0) |
99 | 84, 96, 97, 98 | div23d 11975 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ)
Β· (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) / π) = (((ΞΌβπ) / π) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
100 | 60, 71, 95 | subdid 11618 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· (π β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) = ((((ΞΌβπ) / π) Β· π) β (((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
101 | 99, 100 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ)
Β· (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) / π) = ((((ΞΌβπ) / π) Β· π) β (((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
102 | 101 | sumeq2dv 15595 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) / π) = Ξ£π β (1...(ββπ₯))((((ΞΌβπ) / π) Β· π) β (((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
103 | 60, 95 | mulcld 11182 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)) β β) |
104 | 3, 72, 103 | fsumsub 15680 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((((ΞΌβπ) / π) Β· π) β (((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) = (Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
105 | 102, 104 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) / π) = (Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
106 | 105 | adantrr 716 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) / π) = (Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
107 | 85, 60, 94 | fsummulc2 15676 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)) = Ξ£π β (1...(ββ(π₯ / π)))(((ΞΌβπ) / π) Β· ((logβ((π₯ / π) / π)) / π))) |
108 | 84 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (ΞΌβπ)
β β) |
109 | 97, 98 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π β β
β§ π β
0)) |
110 | 109 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (π β β
β§ π β
0)) |
111 | | div23 11839 |
. . . . . . . . . . . . . . . . 17
β’
(((ΞΌβπ)
β β β§ ((logβ((π₯ / π) / π)) / π) β β β§ (π β β β§ π β 0)) β (((ΞΌβπ) Β· ((logβ((π₯ / π) / π)) / π)) / π) = (((ΞΌβπ) / π) Β· ((logβ((π₯ / π) / π)) / π))) |
112 | | divass 11838 |
. . . . . . . . . . . . . . . . 17
β’
(((ΞΌβπ)
β β β§ ((logβ((π₯ / π) / π)) / π) β β β§ (π β β β§ π β 0)) β (((ΞΌβπ) Β· ((logβ((π₯ / π) / π)) / π)) / π) = ((ΞΌβπ) Β· (((logβ((π₯ / π) / π)) / π) / π))) |
113 | 111, 112 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
β’
(((ΞΌβπ)
β β β§ ((logβ((π₯ / π) / π)) / π) β β β§ (π β β β§ π β 0)) β (((ΞΌβπ) / π) Β· ((logβ((π₯ / π) / π)) / π)) = ((ΞΌβπ) Β· (((logβ((π₯ / π) / π)) / π) / π))) |
114 | 108, 93, 110, 113 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (((ΞΌβπ) /
π) Β·
((logβ((π₯ / π) / π)) / π)) = ((ΞΌβπ) Β· (((logβ((π₯ / π) / π)) / π) / π))) |
115 | 90 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (logβ((π₯ /
π) / π)) β β) |
116 | 91 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β π β
β+) |
117 | | rpcnne0 12940 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β (π β β
β§ π β
0)) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (π β β
β§ π β
0)) |
119 | | divdiv1 11873 |
. . . . . . . . . . . . . . . . . 18
β’
(((logβ((π₯ /
π) / π)) β β β§ (π β β β§ π β 0) β§ (π β β β§ π β 0)) β (((logβ((π₯ / π) / π)) / π) / π) = ((logβ((π₯ / π) / π)) / (π Β· π))) |
120 | 115, 118,
110, 119 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (((logβ((π₯ /
π) / π)) / π) / π) = ((logβ((π₯ / π) / π)) / (π Β· π))) |
121 | | rpre 12930 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β β+
β π₯ β
β) |
122 | 121 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β β+) β π₯ β
β) |
123 | 122 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π₯ β
β) |
124 | 123 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π₯ β
β) |
125 | 124 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β π₯ β
β) |
126 | | divdiv1 11873 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β β β§ (π β β β§ π β 0) β§ (π β β β§ π β 0)) β ((π₯ / π) / π) = (π₯ / (π Β· π))) |
127 | 125, 110,
118, 126 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β ((π₯ / π) / π) = (π₯ / (π Β· π))) |
128 | 127 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (logβ((π₯ /
π) / π)) = (logβ(π₯ / (π Β· π)))) |
129 | 91 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β π β
β) |
130 | 97 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β π β
β) |
131 | 129, 130 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (π Β· π) = (π Β· π)) |
132 | 128, 131 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β ((logβ((π₯ /
π) / π)) / (π Β· π)) = ((logβ(π₯ / (π Β· π))) / (π Β· π))) |
133 | 120, 132 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (((logβ((π₯ /
π) / π)) / π) / π) = ((logβ(π₯ / (π Β· π))) / (π Β· π))) |
134 | 133 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β ((ΞΌβπ)
Β· (((logβ((π₯ /
π) / π)) / π) / π)) = ((ΞΌβπ) Β· ((logβ(π₯ / (π Β· π))) / (π Β· π)))) |
135 | 114, 134 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (((ΞΌβπ) /
π) Β·
((logβ((π₯ / π) / π)) / π)) = ((ΞΌβπ) Β· ((logβ(π₯ / (π Β· π))) / (π Β· π)))) |
136 | 86, 135 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(((ΞΌβπ) / π) Β· ((logβ((π₯ / π) / π)) / π)) = ((ΞΌβπ) Β· ((logβ(π₯ / (π Β· π))) / (π Β· π)))) |
137 | 136 | sumeq2dv 15595 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))(((ΞΌβπ) / π) Β· ((logβ((π₯ / π) / π)) / π)) = Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβ(π₯ / (π Β· π))) / (π Β· π)))) |
138 | 107, 137 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ΞΌβπ) /
π) Β· Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)) = Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβ(π₯ / (π Β· π))) / (π Β· π)))) |
139 | 138 | sumeq2dv 15595 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβ(π₯ / (π Β· π))) / (π Β· π)))) |
140 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π = (π Β· π) β (π₯ / π) = (π₯ / (π Β· π))) |
141 | 140 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π = (π Β· π) β (logβ(π₯ / π)) = (logβ(π₯ / (π Β· π)))) |
142 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = (π Β· π) β π = (π Β· π)) |
143 | 141, 142 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π = (π Β· π) β ((logβ(π₯ / π)) / π) = ((logβ(π₯ / (π Β· π))) / (π Β· π))) |
144 | 143 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = (π Β· π) β ((ΞΌβπ) Β· ((logβ(π₯ / π)) / π)) = ((ΞΌβπ) Β· ((logβ(π₯ / (π Β· π))) / (π Β· π)))) |
145 | 4 | rpred 12964 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β π₯ β
β) |
146 | | ssrab2 4042 |
. . . . . . . . . . . . . . . 16
β’ {π¦ β β β£ π¦ β₯ π} β β |
147 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β {π¦ β β β£ π¦ β₯ π}) |
148 | 146, 147 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β) |
149 | 148, 56 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β€) |
150 | 149 | zred 12614 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β) |
151 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(1...(ββπ₯))
β π β
β) |
152 | 151 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π}) β π β β) |
153 | 152 | nnrpd 12962 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π}) β π β β+) |
154 | | rpdivcl 12947 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β+
β§ π β
β+) β (π₯ / π) β
β+) |
155 | 4, 153, 154 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (π₯ / π) β
β+) |
156 | 155 | relogcld 25994 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (logβ(π₯ / π)) β β) |
157 | 151 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β) |
158 | 156, 157 | nndivred 12214 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β ((logβ(π₯ / π)) / π) β β) |
159 | 150, 158 | remulcld 11192 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β ((ΞΌβπ) Β· ((logβ(π₯ / π)) / π)) β β) |
160 | 159 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β ((ΞΌβπ) Β· ((logβ(π₯ / π)) / π)) β β) |
161 | 144, 145,
160 | dvdsflsumcom 26553 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((logβ(π₯ / π)) / π)) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((logβ(π₯ / (π Β· π))) / (π Β· π)))) |
162 | 139, 161 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)) = Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((logβ(π₯ / π)) / π))) |
163 | 162 | adantrr 716 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)) = Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((logβ(π₯ / π)) / π))) |
164 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = 1 β (π₯ / π) = (π₯ / 1)) |
165 | 164 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = 1 β (logβ(π₯ / π)) = (logβ(π₯ / 1))) |
166 | | id 22 |
. . . . . . . . . 10
β’ (π = 1 β π = 1) |
167 | 165, 166 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = 1 β ((logβ(π₯ / π)) / π) = ((logβ(π₯ / 1)) / 1)) |
168 | | fzfid 13885 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(1...(ββπ₯))
β Fin) |
169 | | fz1ssnn 13479 |
. . . . . . . . . 10
β’
(1...(ββπ₯)) β β |
170 | 169 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(1...(ββπ₯))
β β) |
171 | 122 | adantrr 716 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β
β) |
172 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 β€ π₯) |
173 | | flge1nn 13733 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ 1 β€
π₯) β
(ββπ₯) β
β) |
174 | 171, 172,
173 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β
β) |
175 | | nnuz 12813 |
. . . . . . . . . . 11
β’ β =
(β€β₯β1) |
176 | 174, 175 | eleqtrdi 2848 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β
(β€β₯β1)) |
177 | | eluzfz1 13455 |
. . . . . . . . . 10
β’
((ββπ₯)
β (β€β₯β1) β 1 β
(1...(ββπ₯))) |
178 | 176, 177 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 β
(1...(ββπ₯))) |
179 | 151 | nnrpd 12962 |
. . . . . . . . . . . . . 14
β’ (π β
(1...(ββπ₯))
β π β
β+) |
180 | 4, 179, 154 | syl2an 597 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
181 | 180 | relogcld 25994 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
182 | 169 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β β) |
183 | 182 | sselda 3949 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
184 | 181, 183 | nndivred 12214 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / π) β β) |
185 | 184 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / π) β β) |
186 | 185 | adantlrr 720 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / π) β β) |
187 | 167, 168,
170, 178, 186 | musumsum 26557 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((logβ(π₯ / π)) / π)) = ((logβ(π₯ / 1)) / 1)) |
188 | 4 | rpcnd 12966 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β π₯ β
β) |
189 | 188 | div1d 11930 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β (π₯ / 1) = π₯) |
190 | 189 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β
(logβ(π₯ / 1)) =
(logβπ₯)) |
191 | 190 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
((logβ(π₯ / 1)) / 1) =
((logβπ₯) /
1)) |
192 | 76 | div1d 11930 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
((logβπ₯) / 1) =
(logβπ₯)) |
193 | 191, 192 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
((logβ(π₯ / 1)) / 1) =
(logβπ₯)) |
194 | 193 | adantrr 716 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
((logβ(π₯ / 1)) / 1) =
(logβπ₯)) |
195 | 163, 187,
194 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)) = (logβπ₯)) |
196 | 195 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) = (Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β (logβπ₯))) |
197 | 106, 196 | eqtrd 2777 |
. . . . 5
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) / π) = (Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β (logβπ₯))) |
198 | 197 | fveq2d 6851 |
. . . 4
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))(((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) / π)) = (absβ(Ξ£π β (1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β (logβπ₯)))) |
199 | | ere 15978 |
. . . . . . . . 9
β’ e β
β |
200 | 199 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β e β
β) |
201 | | 1re 11162 |
. . . . . . . . 9
β’ 1 β
β |
202 | | 1lt2 12331 |
. . . . . . . . . 10
β’ 1 <
2 |
203 | | egt2lt3 16095 |
. . . . . . . . . . 11
β’ (2 < e
β§ e < 3) |
204 | 203 | simpli 485 |
. . . . . . . . . 10
β’ 2 <
e |
205 | 201, 2, 199 | lttri 11288 |
. . . . . . . . . 10
β’ ((1 <
2 β§ 2 < e) β 1 < e) |
206 | 202, 204,
205 | mp2an 691 |
. . . . . . . . 9
β’ 1 <
e |
207 | 201, 199,
206 | ltleii 11285 |
. . . . . . . 8
β’ 1 β€
e |
208 | 200, 207 | jctir 522 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β (e β
β β§ 1 β€ e)) |
209 | 37 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β π
β
β) |
210 | 16 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (1 / 2) β
β) |
211 | | 1rp 12926 |
. . . . . . . . . . . . . 14
β’ 1 β
β+ |
212 | | rphalfcl 12949 |
. . . . . . . . . . . . . 14
β’ (1 β
β+ β (1 / 2) β β+) |
213 | 211, 212 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (1 / 2)
β β+ |
214 | | rpge0 12935 |
. . . . . . . . . . . . 13
β’ ((1 / 2)
β β+ β 0 β€ (1 / 2)) |
215 | 213, 214 | mp1i 13 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (1 /
2)) |
216 | 17 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β Ξ³ β
β) |
217 | | 0re 11164 |
. . . . . . . . . . . . . . 15
β’ 0 β
β |
218 | | emgt0 26372 |
. . . . . . . . . . . . . . 15
β’ 0 <
Ξ³ |
219 | 217, 17, 218 | ltleii 11285 |
. . . . . . . . . . . . . 14
β’ 0 β€
Ξ³ |
220 | 219 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 0 β€
Ξ³) |
221 | 20 | absge0d 15336 |
. . . . . . . . . . . . 13
β’ (π β 0 β€ (absβπΏ)) |
222 | 216, 21, 220, 221 | addge0d 11738 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (Ξ³ +
(absβπΏ))) |
223 | 210, 23, 215, 222 | addge0d 11738 |
. . . . . . . . . . 11
β’ (π β 0 β€ ((1 / 2) + (Ξ³
+ (absβπΏ)))) |
224 | | log1 25957 |
. . . . . . . . . . . . . 14
β’
(logβ1) = 0 |
225 | 29 | nncnd 12176 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...2)) β π β β) |
226 | 225 | mulid2d 11180 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...2)) β (1 Β· π) = π) |
227 | 30 | rpred 12964 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...2)) β π β β) |
228 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...2)) β 2 β
β) |
229 | 199 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...2)) β e β
β) |
230 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...2) β π β€ 2) |
231 | 230 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...2)) β π β€ 2) |
232 | 2, 199, 204 | ltleii 11285 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β€
e |
233 | 232 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...2)) β 2 β€
e) |
234 | 227, 228,
229, 231, 233 | letrd 11319 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...2)) β π β€ e) |
235 | 226, 234 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...2)) β (1 Β· π) β€ e) |
236 | | 1red 11163 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...2)) β 1 β
β) |
237 | 236, 229,
30 | lemuldivd 13013 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...2)) β ((1 Β· π) β€ e β 1 β€ (e /
π))) |
238 | 235, 237 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...2)) β 1 β€ (e / π)) |
239 | | logleb 25974 |
. . . . . . . . . . . . . . . 16
β’ ((1
β β+ β§ (e / π) β β+) β (1 β€
(e / π) β
(logβ1) β€ (logβ(e / π)))) |
240 | 211, 32, 239 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...2)) β (1 β€ (e / π) β (logβ1) β€
(logβ(e / π)))) |
241 | 238, 240 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...2)) β (logβ1) β€
(logβ(e / π))) |
242 | 224, 241 | eqbrtrrid 5146 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...2)) β 0 β€ (logβ(e
/ π))) |
243 | 33, 30, 242 | divge0d 13004 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...2)) β 0 β€ ((logβ(e
/ π)) / π)) |
244 | 26, 34, 243 | fsumge0 15687 |
. . . . . . . . . . 11
β’ (π β 0 β€ Ξ£π β (1...2)((logβ(e /
π)) / π)) |
245 | 25, 35, 223, 244 | addge0d 11738 |
. . . . . . . . . 10
β’ (π β 0 β€ (((1 / 2) +
(Ξ³ + (absβπΏ)))
+ Ξ£π β
(1...2)((logβ(e / π))
/ π))) |
246 | 245, 15 | breqtrrdi 5152 |
. . . . . . . . 9
β’ (π β 0 β€ π
) |
247 | 246 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β 0 β€
π
) |
248 | 209, 247 | jca 513 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β (π
β β β§ 0 β€
π
)) |
249 | 84, 96 | mulcld 11182 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ)
Β· (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β β) |
250 | | remulcl 11143 |
. . . . . . . 8
β’ ((2
β β β§ ((logβ(π₯ / π)) / π₯) β β) β (2 Β·
((logβ(π₯ / π)) / π₯)) β β) |
251 | 2, 11, 250 | sylancr 588 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (2 Β· ((logβ(π₯ / π)) / π₯)) β β) |
252 | 2 | a1i 11 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 2 β β) |
253 | | 0le2 12262 |
. . . . . . . . 9
β’ 0 β€
2 |
254 | 253 | a1i 11 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ 2) |
255 | 97 | mulid2d 11180 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 Β· π) =
π) |
256 | | fznnfl 13774 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (π β
(1...(ββπ₯))
β (π β β
β§ π β€ π₯))) |
257 | 122, 256 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β (π β
(1...(ββπ₯))
β (π β β
β§ π β€ π₯))) |
258 | 257 | simplbda 501 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β€ π₯) |
259 | 255, 258 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 Β· π) β€
π₯) |
260 | | 1red 11163 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 1 β β) |
261 | 55 | nnrpd 12962 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β+) |
262 | 260, 123,
261 | lemuldivd 13013 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((1 Β· π) β€
π₯ β 1 β€ (π₯ / π))) |
263 | 259, 262 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 1 β€ (π₯ / π)) |
264 | | logleb 25974 |
. . . . . . . . . . . 12
β’ ((1
β β+ β§ (π₯ / π) β β+) β (1 β€
(π₯ / π) β (logβ1) β€ (logβ(π₯ / π)))) |
265 | 211, 8, 264 | sylancr 588 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 β€ (π₯ / π) β (logβ1) β€
(logβ(π₯ / π)))) |
266 | 263, 265 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (logβ1) β€ (logβ(π₯ / π))) |
267 | 224, 266 | eqbrtrrid 5146 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (logβ(π₯
/ π))) |
268 | | rpregt0 12936 |
. . . . . . . . . 10
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
269 | 268 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ β β
β§ 0 < π₯)) |
270 | | divge0 12031 |
. . . . . . . . 9
β’
((((logβ(π₯ /
π)) β β β§ 0
β€ (logβ(π₯ / π))) β§ (π₯ β β β§ 0 < π₯)) β 0 β€
((logβ(π₯ / π)) / π₯)) |
271 | 9, 267, 269, 270 | syl21anc 837 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ ((logβ(π₯ / π)) / π₯)) |
272 | 252, 11, 254, 271 | mulge0d 11739 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (2 Β· ((logβ(π₯ / π)) / π₯))) |
273 | 249 | abscld 15328 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) β β) |
274 | 273 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β
(absβ((ΞΌβπ)
Β· (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)))) β β) |
275 | 96 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)) β β) |
276 | 275 | abscld 15328 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β (absβ(π β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β β) |
277 | 261 | rpred 12964 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
278 | 251, 277 | remulcld 11192 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((2 Β· ((logβ(π₯ / π)) / π₯)) Β· π) β β) |
279 | 278 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β ((2 Β·
((logβ(π₯ / π)) / π₯)) Β· π) β β) |
280 | 84, 96 | absmuld 15346 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) = ((absβ(ΞΌβπ)) Β· (absβ(π β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))))) |
281 | 84 | abscld 15328 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β β) |
282 | 96 | abscld 15328 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(π
β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β β) |
283 | 96 | absge0d 15336 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ(π
β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)))) |
284 | | mule1 26513 |
. . . . . . . . . . . . 13
β’ (π β β β
(absβ(ΞΌβπ))
β€ 1) |
285 | 55, 284 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β€ 1) |
286 | 281, 260,
282, 283, 285 | lemul1ad 12101 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(ΞΌβπ)) Β· (absβ(π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) β€ (1 Β· (absβ(π β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))))) |
287 | 282 | recnd 11190 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(π
β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β β) |
288 | 287 | mulid2d 11180 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 Β· (absβ(π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) = (absβ(π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
289 | 286, 288 | breqtrd 5136 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(ΞΌβπ)) Β· (absβ(π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) β€ (absβ(π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
290 | 280, 289 | eqbrtrd 5132 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) β€ (absβ(π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
291 | 290 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β
(absβ((ΞΌβπ)
Β· (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)))) β€ (absβ(π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
292 | | logdivsum.1 |
. . . . . . . . . 10
β’ πΉ = (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))((logβπ) / π) β (((logβπ¦)β2) / 2))) |
293 | 18 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β πΉ βπ πΏ) |
294 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β (π₯ / π) β
β+) |
295 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β e β€ (π₯ / π)) |
296 | 292, 293,
294, 295 | mulog2sumlem1 26898 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β
(absβ(Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π) β ((((logβ(π₯ / π))β2) / 2) + ((Ξ³ Β·
(logβ(π₯ / π))) β πΏ)))) β€ (2 Β· ((logβ(π₯ / π)) / (π₯ / π)))) |
297 | 71, 95 | abssubd 15345 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(π
β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) = (absβ(Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π) β π))) |
298 | 297 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β (absβ(π β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) = (absβ(Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π) β π))) |
299 | 61 | oveq2i 7373 |
. . . . . . . . . . 11
β’
(Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π) β π) = (Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π) β ((((logβ(π₯ / π))β2) / 2) + ((Ξ³ Β·
(logβ(π₯ / π))) β πΏ))) |
300 | 299 | fveq2i 6850 |
. . . . . . . . . 10
β’
(absβ(Ξ£π
β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π) β π)) = (absβ(Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π) β ((((logβ(π₯ / π))β2) / 2) + ((Ξ³ Β·
(logβ(π₯ / π))) β πΏ)))) |
301 | 298, 300 | eqtrdi 2793 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β (absβ(π β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) = (absβ(Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π) β ((((logβ(π₯ / π))β2) / 2) + ((Ξ³ Β·
(logβ(π₯ / π))) β πΏ))))) |
302 | | 2cnd 12238 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 2 β β) |
303 | 11 | recnd 11190 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / π₯) β β) |
304 | 302, 303,
97 | mulassd 11185 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((2 Β· ((logβ(π₯ / π)) / π₯)) Β· π) = (2 Β· (((logβ(π₯ / π)) / π₯) Β· π))) |
305 | | rpcnne0 12940 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β (π₯ β β
β§ π₯ β
0)) |
306 | 305 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ β β
β§ π₯ β
0)) |
307 | | divdiv2 11874 |
. . . . . . . . . . . . . 14
β’
(((logβ(π₯ /
π)) β β β§
(π₯ β β β§
π₯ β 0) β§ (π β β β§ π β 0)) β
((logβ(π₯ / π)) / (π₯ / π)) = (((logβ(π₯ / π)) Β· π) / π₯)) |
308 | 62, 306, 109, 307 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / (π₯ / π)) = (((logβ(π₯ / π)) Β· π) / π₯)) |
309 | | div23 11839 |
. . . . . . . . . . . . . 14
β’
(((logβ(π₯ /
π)) β β β§
π β β β§
(π₯ β β β§
π₯ β 0)) β
(((logβ(π₯ / π)) Β· π) / π₯) = (((logβ(π₯ / π)) / π₯) Β· π)) |
310 | 62, 97, 306, 309 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((logβ(π₯ /
π)) Β· π) / π₯) = (((logβ(π₯ / π)) / π₯) Β· π)) |
311 | 308, 310 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / (π₯ / π)) = (((logβ(π₯ / π)) / π₯) Β· π)) |
312 | 311 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (2 Β· ((logβ(π₯ / π)) / (π₯ / π))) = (2 Β· (((logβ(π₯ / π)) / π₯) Β· π))) |
313 | 304, 312 | eqtr4d 2780 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((2 Β· ((logβ(π₯ / π)) / π₯)) Β· π) = (2 Β· ((logβ(π₯ / π)) / (π₯ / π)))) |
314 | 313 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β ((2 Β·
((logβ(π₯ / π)) / π₯)) Β· π) = (2 Β· ((logβ(π₯ / π)) / (π₯ / π)))) |
315 | 296, 301,
314 | 3brtr4d 5142 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β (absβ(π β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β€ ((2 Β· ((logβ(π₯ / π)) / π₯)) Β· π)) |
316 | 274, 276,
279, 291, 315 | letrd 11319 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ e β€ (π₯ / π)) β
(absβ((ΞΌβπ)
Β· (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)))) β€ ((2 Β· ((logβ(π₯ / π)) / π₯)) Β· π)) |
317 | 273 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((ΞΌβπ)
Β· (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)))) β β) |
318 | 282 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ(π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β β) |
319 | 37 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β π
β
β) |
320 | 290 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((ΞΌβπ)
Β· (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)))) β€ (absβ(π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
321 | 71 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β π β
β) |
322 | 321 | abscld 15328 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβπ) β
β) |
323 | 95 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π) β β) |
324 | 323 | abscld 15328 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβΞ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)) β β) |
325 | 322, 324 | readdcld 11191 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((absβπ) +
(absβΞ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β β) |
326 | 321, 323 | abs2dif2d 15350 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ(π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β€ ((absβπ) + (absβΞ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)))) |
327 | 25 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β ((1 / 2) +
(Ξ³ + (absβπΏ)))
β β) |
328 | 35 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β Ξ£π β (1...2)((logβ(e /
π)) / π) β β) |
329 | 61 | fveq2i 6850 |
. . . . . . . . . . . 12
β’
(absβπ) =
(absβ((((logβ(π₯
/ π))β2) / 2) +
((Ξ³ Β· (logβ(π₯ / π))) β πΏ))) |
330 | 329, 322 | eqeltrrid 2843 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((((logβ(π₯
/ π))β2) / 2) +
((Ξ³ Β· (logβ(π₯ / π))) β πΏ))) β β) |
331 | 64 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(((logβ(π₯ / π))β2) / 2) β
β) |
332 | 331 | abscld 15328 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ(((logβ(π₯
/ π))β2) / 2)) β
β) |
333 | 69 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β ((Ξ³
Β· (logβ(π₯ /
π))) β πΏ) β
β) |
334 | 333 | abscld 15328 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((Ξ³ Β· (logβ(π₯ / π))) β πΏ)) β β) |
335 | 332, 334 | readdcld 11191 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((absβ(((logβ(π₯
/ π))β2) / 2)) +
(absβ((Ξ³ Β· (logβ(π₯ / π))) β πΏ))) β β) |
336 | 331, 333 | abstrid 15348 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((((logβ(π₯
/ π))β2) / 2) +
((Ξ³ Β· (logβ(π₯ / π))) β πΏ))) β€ ((absβ(((logβ(π₯ / π))β2) / 2)) + (absβ((Ξ³
Β· (logβ(π₯ /
π))) β πΏ)))) |
337 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (1 / 2) β
β) |
338 | 23 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (Ξ³ +
(absβπΏ)) β
β) |
339 | 9 | resqcld 14037 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π))β2) β
β) |
340 | 339 | rehalfcld 12407 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((logβ(π₯ /
π))β2) / 2) β
β) |
341 | 9 | sqge0d 14049 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ ((logβ(π₯ / π))β2)) |
342 | | 2pos 12263 |
. . . . . . . . . . . . . . . . . . . 20
β’ 0 <
2 |
343 | 2, 342 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . 19
β’ (2 β
β β§ 0 < 2) |
344 | 343 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (2 β β β§ 0 < 2)) |
345 | | divge0 12031 |
. . . . . . . . . . . . . . . . . 18
β’
(((((logβ(π₯ /
π))β2) β β
β§ 0 β€ ((logβ(π₯
/ π))β2)) β§ (2
β β β§ 0 < 2)) β 0 β€ (((logβ(π₯ / π))β2) / 2)) |
346 | 339, 341,
344, 345 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (((logβ(π₯ / π))β2) / 2)) |
347 | 340, 346 | absidd 15314 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(((logβ(π₯ / π))β2) / 2)) = (((logβ(π₯ / π))β2) / 2)) |
348 | 347 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ(((logβ(π₯
/ π))β2) / 2)) =
(((logβ(π₯ / π))β2) /
2)) |
349 | 8 | rpred 12964 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β) |
350 | | ltle 11250 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ / π) β β β§ e β β)
β ((π₯ / π) < e β (π₯ / π) β€ e)) |
351 | 349, 199,
350 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((π₯ / π) < e β (π₯ / π) β€ e)) |
352 | 351 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (π₯ / π) β€ e) |
353 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (π₯ / π) β
β+) |
354 | | logleb 25974 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ / π) β β+ β§ e β
β+) β ((π₯ / π) β€ e β (logβ(π₯ / π)) β€ (logβe))) |
355 | 353, 27, 354 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β ((π₯ / π) β€ e β (logβ(π₯ / π)) β€ (logβe))) |
356 | 352, 355 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(logβ(π₯ / π)) β€
(logβe)) |
357 | | loge 25958 |
. . . . . . . . . . . . . . . . . . 19
β’
(logβe) = 1 |
358 | 356, 357 | breqtrdi 5151 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(logβ(π₯ / π)) β€ 1) |
359 | | 0le1 11685 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β€
1 |
360 | 359 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ 1) |
361 | 9, 260, 267, 360 | le2sqd 14167 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) β€ 1 β
((logβ(π₯ / π))β2) β€
(1β2))) |
362 | 361 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((logβ(π₯ / π)) β€ 1 β
((logβ(π₯ / π))β2) β€
(1β2))) |
363 | 358, 362 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((logβ(π₯ / π))β2) β€
(1β2)) |
364 | | sq1 14106 |
. . . . . . . . . . . . . . . . 17
β’
(1β2) = 1 |
365 | 363, 364 | breqtrdi 5151 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((logβ(π₯ / π))β2) β€
1) |
366 | 339 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((logβ(π₯ / π))β2) β
β) |
367 | | 1red 11163 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β 1 β
β) |
368 | 343 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (2 β
β β§ 0 < 2)) |
369 | | lediv1 12027 |
. . . . . . . . . . . . . . . . 17
β’
((((logβ(π₯ /
π))β2) β β
β§ 1 β β β§ (2 β β β§ 0 < 2)) β
(((logβ(π₯ / π))β2) β€ 1 β
(((logβ(π₯ / π))β2) / 2) β€ (1 /
2))) |
370 | 366, 367,
368, 369 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(((logβ(π₯ / π))β2) β€ 1 β
(((logβ(π₯ / π))β2) / 2) β€ (1 /
2))) |
371 | 365, 370 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(((logβ(π₯ / π))β2) / 2) β€ (1 /
2)) |
372 | 348, 371 | eqbrtrd 5132 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ(((logβ(π₯
/ π))β2) / 2)) β€ (1
/ 2)) |
373 | 68 | abscld 15328 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβπΏ) β
β) |
374 | 66, 373 | readdcld 11191 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((Ξ³ Β· (logβ(π₯ / π))) + (absβπΏ)) β β) |
375 | 374 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β ((Ξ³
Β· (logβ(π₯ /
π))) + (absβπΏ)) β
β) |
376 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (Ξ³
Β· (logβ(π₯ /
π))) β
β) |
377 | 20 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β πΏ β
β) |
378 | 376, 377 | abs2dif2d 15350 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((Ξ³ Β· (logβ(π₯ / π))) β πΏ)) β€ ((absβ(Ξ³ Β·
(logβ(π₯ / π)))) + (absβπΏ))) |
379 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ³ β β) |
380 | 219 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ Ξ³) |
381 | 379, 9, 380, 267 | mulge0d 11739 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (Ξ³ Β· (logβ(π₯ / π)))) |
382 | 66, 381 | absidd 15314 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(Ξ³ Β· (logβ(π₯ / π)))) = (Ξ³ Β· (logβ(π₯ / π)))) |
383 | 382 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ(Ξ³ Β· (logβ(π₯ / π)))) = (Ξ³ Β· (logβ(π₯ / π)))) |
384 | 383 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((absβ(Ξ³ Β· (logβ(π₯ / π)))) + (absβπΏ)) = ((Ξ³ Β· (logβ(π₯ / π))) + (absβπΏ))) |
385 | 378, 384 | breqtrd 5136 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((Ξ³ Β· (logβ(π₯ / π))) β πΏ)) β€ ((Ξ³ Β· (logβ(π₯ / π))) + (absβπΏ))) |
386 | 66 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (Ξ³
Β· (logβ(π₯ /
π))) β
β) |
387 | 17 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β Ξ³ β
β) |
388 | 377 | abscld 15328 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβπΏ) β
β) |
389 | 9 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(logβ(π₯ / π)) β
β) |
390 | 387, 218 | jctir 522 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (Ξ³ β
β β§ 0 < Ξ³)) |
391 | | lemul2 12015 |
. . . . . . . . . . . . . . . . . . 19
β’
(((logβ(π₯ /
π)) β β β§ 1
β β β§ (Ξ³ β β β§ 0 < Ξ³)) β
((logβ(π₯ / π)) β€ 1 β (Ξ³
Β· (logβ(π₯ /
π))) β€ (Ξ³ Β·
1))) |
392 | 389, 367,
390, 391 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((logβ(π₯ / π)) β€ 1 β (Ξ³
Β· (logβ(π₯ /
π))) β€ (Ξ³ Β·
1))) |
393 | 358, 392 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (Ξ³
Β· (logβ(π₯ /
π))) β€ (Ξ³ Β·
1)) |
394 | 17 | recni 11176 |
. . . . . . . . . . . . . . . . . 18
β’ Ξ³
β β |
395 | 394 | mulid1i 11166 |
. . . . . . . . . . . . . . . . 17
β’ (Ξ³
Β· 1) = Ξ³ |
396 | 393, 395 | breqtrdi 5151 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (Ξ³
Β· (logβ(π₯ /
π))) β€
Ξ³) |
397 | 386, 387,
388, 396 | leadd1dd 11776 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β ((Ξ³
Β· (logβ(π₯ /
π))) + (absβπΏ)) β€ (Ξ³ +
(absβπΏ))) |
398 | 334, 375,
338, 385, 397 | letrd 11319 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((Ξ³ Β· (logβ(π₯ / π))) β πΏ)) β€ (Ξ³ + (absβπΏ))) |
399 | 332, 334,
337, 338, 372, 398 | le2addd 11781 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((absβ(((logβ(π₯
/ π))β2) / 2)) +
(absβ((Ξ³ Β· (logβ(π₯ / π))) β πΏ))) β€ ((1 / 2) + (Ξ³ +
(absβπΏ)))) |
400 | 330, 335,
327, 336, 399 | letrd 11319 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((((logβ(π₯
/ π))β2) / 2) +
((Ξ³ Β· (logβ(π₯ / π))) β πΏ))) β€ ((1 / 2) + (Ξ³ +
(absβπΏ)))) |
401 | 329, 400 | eqbrtrid 5145 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβπ) β€ ((1 / 2)
+ (Ξ³ + (absβπΏ)))) |
402 | 86, 92 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((logβ((π₯ / π) / π)) / π) β β) |
403 | 85, 402 | fsumrecl 15626 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π) β β) |
404 | 403 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π) β β) |
405 | 86, 90 | sylan2 594 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(logβ((π₯ / π) / π)) β β) |
406 | 86, 129 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
407 | 406 | mulid2d 11180 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (1 Β·
π) = π) |
408 | | fznnfl 13774 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ / π) β β β (π β (1...(ββ(π₯ / π))) β (π β β β§ π β€ (π₯ / π)))) |
409 | 349, 408 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π β
(1...(ββ(π₯ /
π))) β (π β β β§ π β€ (π₯ / π)))) |
410 | 409 | simplbda 501 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β€ (π₯ / π)) |
411 | 407, 410 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (1 Β·
π) β€ (π₯ / π)) |
412 | | 1red 11163 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β 1 β
β) |
413 | 349 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (π₯ / π) β β) |
414 | 116 | rpregt0d 12970 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β β)
β (π β β
β§ 0 < π)) |
415 | 86, 414 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (π β β β§ 0 <
π)) |
416 | | lemuldiv 12042 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((1
β β β§ (π₯ /
π) β β β§
(π β β β§ 0
< π)) β ((1
Β· π) β€ (π₯ / π) β 1 β€ ((π₯ / π) / π))) |
417 | 412, 413,
415, 416 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β ((1 Β·
π) β€ (π₯ / π) β 1 β€ ((π₯ / π) / π))) |
418 | 411, 417 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β 1 β€ ((π₯ / π) / π)) |
419 | 86, 89 | sylan2 594 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β ((π₯ / π) / π) β
β+) |
420 | | logleb 25974 |
. . . . . . . . . . . . . . . . . . 19
β’ ((1
β β+ β§ ((π₯ / π) / π) β β+) β (1 β€
((π₯ / π) / π) β (logβ1) β€
(logβ((π₯ / π) / π)))) |
421 | 211, 419,
420 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (1 β€
((π₯ / π) / π) β (logβ1) β€
(logβ((π₯ / π) / π)))) |
422 | 418, 421 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (logβ1)
β€ (logβ((π₯ / π) / π))) |
423 | 224, 422 | eqbrtrrid 5146 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β 0 β€
(logβ((π₯ / π) / π))) |
424 | | divge0 12031 |
. . . . . . . . . . . . . . . 16
β’
((((logβ((π₯ /
π) / π)) β β β§ 0 β€
(logβ((π₯ / π) / π))) β§ (π β β β§ 0 < π)) β 0 β€
((logβ((π₯ / π) / π)) / π)) |
425 | 405, 423,
415, 424 | syl21anc 837 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β 0 β€
((logβ((π₯ / π) / π)) / π)) |
426 | 85, 402, 425 | fsumge0 15687 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ Ξ£π
β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)) |
427 | 426 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β 0 β€
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)) |
428 | 404, 427 | absidd 15314 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβΞ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)) = Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π)) |
429 | | fzfid 13885 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(1...(ββ(π₯ /
π))) β
Fin) |
430 | 349 | flcld 13710 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ(π₯ /
π)) β
β€) |
431 | 430 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(ββ(π₯ / π)) β
β€) |
432 | | 2z 12542 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
β€ |
433 | 432 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β 2 β
β€) |
434 | 349 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (π₯ / π) β β) |
435 | 199 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β e β
β) |
436 | | 3re 12240 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 3 β
β |
437 | 436 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β 3 β
β) |
438 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (π₯ / π) < e) |
439 | 203 | simpri 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ e <
3 |
440 | 439 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β e <
3) |
441 | 434, 435,
437, 438, 440 | lttrd 11323 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (π₯ / π) < 3) |
442 | | 3z 12543 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 3 β
β€ |
443 | | fllt 13718 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ / π) β β β§ 3 β β€)
β ((π₯ / π) < 3 β
(ββ(π₯ / π)) < 3)) |
444 | 434, 442,
443 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β ((π₯ / π) < 3 β (ββ(π₯ / π)) < 3)) |
445 | 441, 444 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(ββ(π₯ / π)) < 3) |
446 | | df-3 12224 |
. . . . . . . . . . . . . . . . . . . 20
β’ 3 = (2 +
1) |
447 | 445, 446 | breqtrdi 5151 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(ββ(π₯ / π)) < (2 +
1)) |
448 | | zleltp1 12561 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((ββ(π₯
/ π)) β β€ β§
2 β β€) β ((ββ(π₯ / π)) β€ 2 β (ββ(π₯ / π)) < (2 + 1))) |
449 | 431, 432,
448 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((ββ(π₯ / π)) β€ 2 β
(ββ(π₯ / π)) < (2 +
1))) |
450 | 447, 449 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(ββ(π₯ / π)) β€ 2) |
451 | | eluz2 12776 |
. . . . . . . . . . . . . . . . . 18
β’ (2 β
(β€β₯β(ββ(π₯ / π))) β ((ββ(π₯ / π)) β β€ β§ 2 β β€
β§ (ββ(π₯ /
π)) β€
2)) |
452 | 431, 433,
450, 451 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β 2 β
(β€β₯β(ββ(π₯ / π)))) |
453 | | fzss2 13488 |
. . . . . . . . . . . . . . . . 17
β’ (2 β
(β€β₯β(ββ(π₯ / π))) β (1...(ββ(π₯ / π))) β (1...2)) |
454 | 452, 453 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(1...(ββ(π₯ /
π))) β
(1...2)) |
455 | 454 | sselda 3949 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β
(1...(ββ(π₯ /
π)))) β π β
(1...2)) |
456 | 34 | ad5ant15 758 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β
((logβ(e / π)) /
π) β
β) |
457 | 455, 456 | syldan 592 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β
(1...(ββ(π₯ /
π)))) β ((logβ(e
/ π)) / π) β β) |
458 | 429, 457 | fsumrecl 15626 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ(e / π)) / π) β β) |
459 | 92 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β β) β
((logβ((π₯ / π) / π)) / π) β β) |
460 | 86, 459 | sylan2 594 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β
(1...(ββ(π₯ /
π)))) β
((logβ((π₯ / π) / π)) / π) β β) |
461 | 352 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β (π₯ / π) β€ e) |
462 | 434 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β (π₯ / π) β β) |
463 | 199 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β e β
β) |
464 | 30 | rpregt0d 12970 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...2)) β (π β β β§ 0 < π)) |
465 | 464 | ad5ant15 758 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β (π β β β§ 0 <
π)) |
466 | | lediv1 12027 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ / π) β β β§ e β β β§
(π β β β§ 0
< π)) β ((π₯ / π) β€ e β ((π₯ / π) / π) β€ (e / π))) |
467 | 462, 463,
465, 466 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β ((π₯ / π) β€ e β ((π₯ / π) / π) β€ (e / π))) |
468 | 461, 467 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β ((π₯ / π) / π) β€ (e / π)) |
469 | 89 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β β) β ((π₯ / π) / π) β
β+) |
470 | 28, 469 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β ((π₯ / π) / π) β
β+) |
471 | 32 | ad5ant15 758 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β (e /
π) β
β+) |
472 | 470, 471 | logled 25998 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β (((π₯ / π) / π) β€ (e / π) β (logβ((π₯ / π) / π)) β€ (logβ(e / π)))) |
473 | 468, 472 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β
(logβ((π₯ / π) / π)) β€ (logβ(e / π))) |
474 | 90 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β β) β
(logβ((π₯ / π) / π)) β β) |
475 | 28, 474 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β
(logβ((π₯ / π) / π)) β β) |
476 | 33 | ad5ant15 758 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β
(logβ(e / π)) β
β) |
477 | | lediv1 12027 |
. . . . . . . . . . . . . . . . 17
β’
(((logβ((π₯ /
π) / π)) β β β§ (logβ(e / π)) β β β§ (π β β β§ 0 <
π)) β
((logβ((π₯ / π) / π)) β€ (logβ(e / π)) β ((logβ((π₯ / π) / π)) / π) β€ ((logβ(e / π)) / π))) |
478 | 475, 476,
465, 477 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β
((logβ((π₯ / π) / π)) β€ (logβ(e / π)) β ((logβ((π₯ / π) / π)) / π) β€ ((logβ(e / π)) / π))) |
479 | 473, 478 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β
((logβ((π₯ / π) / π)) / π) β€ ((logβ(e / π)) / π)) |
480 | 455, 479 | syldan 592 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β
(1...(ββ(π₯ /
π)))) β
((logβ((π₯ / π) / π)) / π) β€ ((logβ(e / π)) / π)) |
481 | 429, 460,
457, 480 | fsumle 15691 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π) β€ Ξ£π β (1...(ββ(π₯ / π)))((logβ(e / π)) / π)) |
482 | | fzfid 13885 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β (1...2) β
Fin) |
483 | 243 | ad5ant15 758 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β+)
β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β§ π β (1...2)) β 0 β€
((logβ(e / π)) /
π)) |
484 | 482, 456,
483, 454 | fsumless 15688 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ(e / π)) / π) β€ Ξ£π β (1...2)((logβ(e / π)) / π)) |
485 | 404, 458,
328, 481, 484 | letrd 11319 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π) β€ Ξ£π β (1...2)((logβ(e / π)) / π)) |
486 | 428, 485 | eqbrtrd 5132 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβΞ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)) β€ Ξ£π β (1...2)((logβ(e / π)) / π)) |
487 | 322, 324,
327, 328, 401, 486 | le2addd 11781 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((absβπ) +
(absβΞ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β€ (((1 / 2) + (Ξ³ +
(absβπΏ))) +
Ξ£π β
(1...2)((logβ(e / π))
/ π))) |
488 | 487, 15 | breqtrrdi 5152 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
((absβπ) +
(absβΞ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β€ π
) |
489 | 318, 325,
319, 326, 488 | letrd 11319 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ(π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π))) β€ π
) |
490 | 317, 318,
319, 320, 489 | letrd 11319 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < e) β
(absβ((ΞΌβπ)
Β· (π β
Ξ£π β
(1...(ββ(π₯ /
π)))((logβ((π₯ / π) / π)) / π)))) β€ π
) |
491 | 4, 208, 248, 249, 251, 272, 316, 490 | fsumharmonic 26377 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))(((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) / π)) β€ (Ξ£π β (1...(ββπ₯))(2 Β· ((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβe) +
1)))) |
492 | | 2cnd 12238 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β 2 β
β) |
493 | 3, 492, 303 | fsummulc2 15676 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β (2
Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) = Ξ£π β (1...(ββπ₯))(2 Β· ((logβ(π₯ / π)) / π₯))) |
494 | | df-2 12223 |
. . . . . . . . . 10
β’ 2 = (1 +
1) |
495 | 357 | oveq1i 7372 |
. . . . . . . . . 10
β’
((logβe) + 1) = (1 + 1) |
496 | 494, 495 | eqtr4i 2768 |
. . . . . . . . 9
β’ 2 =
((logβe) + 1) |
497 | 496 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β 2 =
((logβe) + 1)) |
498 | 497 | oveq2d 7378 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β (π
Β· 2) = (π
Β· ((logβe) +
1))) |
499 | 493, 498 | oveq12d 7380 |
. . . . . 6
β’ ((π β§ π₯ β β+) β ((2
Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2)) = (Ξ£π β (1...(ββπ₯))(2 Β· ((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβe) +
1)))) |
500 | 491, 499 | breqtrrd 5138 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))(((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) / π)) β€ ((2 Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2))) |
501 | 500 | adantrr 716 |
. . . 4
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))(((ΞΌβπ) Β· (π β Ξ£π β (1...(ββ(π₯ / π)))((logβ((π₯ / π) / π)) / π))) / π)) β€ ((2 Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2))) |
502 | 198, 501 | eqbrtrrd 5134 |
. . 3
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβ(Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β (logβπ₯))) β€ ((2 Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2))) |
503 | 54 | leabsd 15306 |
. . . 4
β’ ((π β§ π₯ β β+) β ((2
Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2)) β€ (absβ((2 Β·
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2)))) |
504 | 503 | adantrr 716 |
. . 3
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β ((2 Β·
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2)) β€ (absβ((2 Β·
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2)))) |
505 | 79, 80, 83, 502, 504 | letrd 11319 |
. 2
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβ(Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β (logβπ₯))) β€ (absβ((2 Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· 2)))) |
506 | 1, 53, 54, 77, 505 | o1le 15544 |
1
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))(((ΞΌβπ) / π) Β· π) β (logβπ₯))) β π(1)) |