Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (1...(ββπ₯)) β Fin) |
2 | | elfznn 13477 |
. . . . . . . . . . . . 13
β’ (π β
(1...(ββπ₯))
β π β
β) |
3 | 2 | adantl 483 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
4 | 3 | nnrpd 12962 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β+) |
5 | 4 | relogcld 25994 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (logβπ) β
β) |
6 | 5, 3 | nndivred 12214 |
. . . . . . . . 9
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((logβπ) / π) β β) |
7 | 1, 6 | fsumrecl 15626 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((logβπ) / π) β β) |
8 | 7 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((logβπ) / π) β β) |
9 | | elioore 13301 |
. . . . . . . . . . . . 13
β’ (π₯ β (1(,)+β) β
π₯ β
β) |
10 | 9 | adantl 483 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β) |
11 | | 1rp 12926 |
. . . . . . . . . . . . 13
β’ 1 β
β+ |
12 | 11 | a1i 11 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β+) |
13 | | 1red 11163 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β) |
14 | | eliooord 13330 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (1(,)+β) β (1
< π₯ β§ π₯ <
+β)) |
15 | 14 | adantl 483 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (1 < π₯ β§ π₯ < +β)) |
16 | 15 | simpld 496 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β 1 < π₯) |
17 | 13, 10, 16 | ltled 11310 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β€ π₯) |
18 | 10, 12, 17 | rpgecld 13003 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β+) |
19 | 18 | relogcld 25994 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β β) |
20 | 19 | resqcld 14037 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((logβπ₯)β2) β β) |
21 | 20 | rehalfcld 12407 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (((logβπ₯)β2) / 2) β
β) |
22 | 21 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((logβπ₯)β2) / 2) β
β) |
23 | 19 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β β) |
24 | 10, 16 | rplogcld 26000 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β
β+) |
25 | 24 | rpne0d 12969 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β 0) |
26 | 8, 22, 23, 25 | divsubdird 11977 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2)) / (logβπ₯)) = ((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((((logβπ₯)β2) / 2) / (logβπ₯)))) |
27 | 7, 21 | resubcld 11590 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2)) β
β) |
28 | 27 | recnd 11190 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2)) β
β) |
29 | 28, 23, 25 | divrecd 11941 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2)) / (logβπ₯)) = ((Ξ£π β (1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2)) Β· (1 /
(logβπ₯)))) |
30 | 20 | recnd 11190 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((logβπ₯)β2) β β) |
31 | | 2cnd 12238 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β 2 β β) |
32 | | 2ne0 12264 |
. . . . . . . . . 10
β’ 2 β
0 |
33 | 32 | a1i 11 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β 2 β 0) |
34 | 30, 31, 23, 33, 25 | divdiv32d 11963 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((((logβπ₯)β2) / 2) / (logβπ₯)) = ((((logβπ₯)β2) / (logβπ₯)) / 2)) |
35 | 23 | sqvald 14055 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β ((logβπ₯)β2) = ((logβπ₯) Β· (logβπ₯))) |
36 | 35 | oveq1d 7377 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (((logβπ₯)β2) / (logβπ₯)) = (((logβπ₯) Β· (logβπ₯)) / (logβπ₯))) |
37 | 23, 23, 25 | divcan3d 11943 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (((logβπ₯) Β· (logβπ₯)) / (logβπ₯)) = (logβπ₯)) |
38 | 36, 37 | eqtrd 2777 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (((logβπ₯)β2) / (logβπ₯)) = (logβπ₯)) |
39 | 38 | oveq1d 7377 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((((logβπ₯)β2) / (logβπ₯)) / 2) = ((logβπ₯) / 2)) |
40 | 34, 39 | eqtrd 2777 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β ((((logβπ₯)β2) / 2) / (logβπ₯)) = ((logβπ₯) / 2)) |
41 | 40 | oveq2d 7378 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((((logβπ₯)β2) / 2) / (logβπ₯))) = ((Ξ£π β
(1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2))) |
42 | 26, 29, 41 | 3eqtr3rd 2786 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2)) = ((Ξ£π β (1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2)) Β· (1 /
(logβπ₯)))) |
43 | 42 | mpteq2dva 5210 |
. . . 4
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2))) = (π₯ β (1(,)+β) β¦ ((Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2)) Β· (1 /
(logβπ₯))))) |
44 | 24 | rprecred 12975 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (1 / (logβπ₯)) β β) |
45 | 18 | ex 414 |
. . . . . . 7
β’ (β€
β (π₯ β
(1(,)+β) β π₯
β β+)) |
46 | 45 | ssrdv 3955 |
. . . . . 6
β’ (β€
β (1(,)+β) β β+) |
47 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2))) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2))) |
48 | 47 | logdivsum 26897 |
. . . . . . . 8
β’ ((π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) /
2))):β+βΆβ β§ (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2))) β dom
βπ β§ (((π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2))) βπ
1 β§ 1 β β+ β§ e β€ 1) β (absβ(((π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2)))β1) β 1)) β€
((logβ1) / 1))) |
49 | 48 | simp2i 1141 |
. . . . . . 7
β’ (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2))) β dom
βπ |
50 | | rlimdmo1 15507 |
. . . . . . 7
β’ ((π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2))) β dom
βπ β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2))) β
π(1)) |
51 | 49, 50 | mp1i 13 |
. . . . . 6
β’ (β€
β (π₯ β
β+ β¦ (Ξ£π β (1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2))) β
π(1)) |
52 | 46, 51 | o1res2 15452 |
. . . . 5
β’ (β€
β (π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2))) β
π(1)) |
53 | | divlogrlim 26006 |
. . . . . 6
β’ (π₯ β (1(,)+β) β¦
(1 / (logβπ₯)))
βπ 0 |
54 | | rlimo1 15506 |
. . . . . 6
β’ ((π₯ β (1(,)+β) β¦
(1 / (logβπ₯)))
βπ 0 β (π₯ β (1(,)+β) β¦ (1 /
(logβπ₯))) β
π(1)) |
55 | 53, 54 | mp1i 13 |
. . . . 5
β’ (β€
β (π₯ β
(1(,)+β) β¦ (1 / (logβπ₯))) β π(1)) |
56 | 27, 44, 52, 55 | o1mul2 15514 |
. . . 4
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((Ξ£π β (1...(ββπ₯))((logβπ) / π) β (((logβπ₯)β2) / 2)) Β· (1 /
(logβπ₯)))) β
π(1)) |
57 | 43, 56 | eqeltrd 2838 |
. . 3
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2))) β
π(1)) |
58 | 8, 23, 25 | divcld 11938 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β β) |
59 | 23 | halfcld 12405 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((logβπ₯) / 2) β β) |
60 | 58, 59 | subcld 11519 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2)) β β) |
61 | | elfznn 13477 |
. . . . . . . . . . . 12
β’ (π β
(1...(ββπ₯))
β π β
β) |
62 | 61 | adantl 483 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
63 | | vmacl 26483 |
. . . . . . . . . . 11
β’ (π β β β
(Ξβπ) β
β) |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξβπ) β
β) |
65 | 64, 62 | nndivred 12214 |
. . . . . . . . 9
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ) / π) β
β) |
66 | 18 | adantr 482 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π₯ β β+) |
67 | 62 | nnrpd 12962 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β+) |
68 | 66, 67 | rpdivcld 12981 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π₯ / π) β
β+) |
69 | 68 | relogcld 25994 |
. . . . . . . . 9
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (logβ(π₯ / π)) β β) |
70 | 65, 69 | remulcld 11192 |
. . . . . . . 8
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ) /
π) Β·
(logβ(π₯ / π))) β
β) |
71 | 1, 70 | fsumrecl 15626 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) β β) |
72 | 71 | recnd 11190 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) β β) |
73 | 24 | rpcnd 12966 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β β) |
74 | 72, 73, 25 | divcld 11938 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)) β β) |
75 | 73 | halfcld 12405 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((logβπ₯) / 2) β β) |
76 | 74, 75 | subcld 11519 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)) β ((logβπ₯) / 2)) β β) |
77 | 58, 74, 59 | nnncan2d 11554 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2)) β ((Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)) β ((logβπ₯) / 2))) = ((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)))) |
78 | 8, 72, 23, 25 | divsubdird 11977 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((logβπ) / π) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π)))) / (logβπ₯)) = ((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)))) |
79 | | fzfid 13885 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(1...(ββ(π₯ /
π))) β
Fin) |
80 | 64 | adantr 482 |
. . . . . . . . . . . . 13
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (Ξβπ) β
β) |
81 | 62 | adantr 482 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β β) |
82 | | elfznn 13477 |
. . . . . . . . . . . . . . 15
β’ (π β
(1...(ββ(π₯ /
π))) β π β
β) |
83 | 82 | adantl 483 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β β) |
84 | 81, 83 | nnmulcld 12213 |
. . . . . . . . . . . . 13
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (π Β· π) β β) |
85 | 80, 84 | nndivred 12214 |
. . . . . . . . . . . 12
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((Ξβπ) / (π Β· π)) β β) |
86 | 79, 85 | fsumrecl 15626 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) / (π Β· π)) β β) |
87 | 86 | recnd 11190 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) / (π Β· π)) β β) |
88 | 70 | recnd 11190 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ) /
π) Β·
(logβ(π₯ / π))) β
β) |
89 | 1, 87, 88 | fsumsub 15680 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) / (π Β· π)) β (((Ξβπ) / π) Β· (logβ(π₯ / π)))) = (Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) / (π Β· π)) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))))) |
90 | 64 | recnd 11190 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξβπ) β
β) |
91 | 62 | nncnd 12176 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
92 | 62 | nnne0d 12210 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β 0) |
93 | 90, 91, 92 | divcld 11938 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
((Ξβπ) / π) β
β) |
94 | 83 | nnrecred 12211 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (1 / π) β β) |
95 | 79, 94 | fsumrecl 15626 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β β) |
96 | 95 | recnd 11190 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β β) |
97 | 69 | recnd 11190 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (logβ(π₯ / π)) β β) |
98 | 93, 96, 97 | subdid 11618 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π)))) = ((((Ξβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π)) β (((Ξβπ) / π) Β· (logβ(π₯ / π))))) |
99 | 90 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (Ξβπ) β
β) |
100 | 91 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β β) |
101 | 83 | nncnd 12176 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β β) |
102 | 92 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β 0) |
103 | 83 | nnne0d 12210 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β π β 0) |
104 | 99, 100, 101, 102, 103 | divdiv1d 11969 |
. . . . . . . . . . . . . . 15
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (((Ξβπ) / π) / π) = ((Ξβπ) / (π Β· π))) |
105 | 99, 100, 102 | divcld 11938 |
. . . . . . . . . . . . . . . 16
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((Ξβπ) / π) β β) |
106 | 105, 101,
103 | divrecd 11941 |
. . . . . . . . . . . . . . 15
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (((Ξβπ) / π) / π) = (((Ξβπ) / π) Β· (1 / π))) |
107 | 104, 106 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β ((Ξβπ) / (π Β· π)) = (((Ξβπ) / π) Β· (1 / π))) |
108 | 107 | sumeq2dv 15595 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) / (π Β· π)) = Ξ£π β (1...(ββ(π₯ / π)))(((Ξβπ) / π) Β· (1 / π))) |
109 | 101, 103 | reccld 11931 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β (1...(ββ(π₯ / π)))) β (1 / π) β β) |
110 | 79, 93, 109 | fsummulc2 15676 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ) /
π) Β· Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π)) = Ξ£π β (1...(ββ(π₯ / π)))(((Ξβπ) / π) Β· (1 / π))) |
111 | 108, 110 | eqtr4d 2780 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) / (π Β· π)) = (((Ξβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π))) |
112 | 111 | oveq1d 7377 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β
(1...(ββ(π₯ /
π)))((Ξβπ) / (π Β· π)) β (((Ξβπ) / π) Β· (logβ(π₯ / π)))) = ((((Ξβπ) / π) Β· Ξ£π β (1...(ββ(π₯ / π)))(1 / π)) β (((Ξβπ) / π) Β· (logβ(π₯ / π))))) |
113 | 98, 112 | eqtr4d 2780 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π)))) = (Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) / (π Β· π)) β (((Ξβπ) / π) Β· (logβ(π₯ / π))))) |
114 | 113 | sumeq2dv 15595 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) = Ξ£π β (1...(ββπ₯))(Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) / (π Β· π)) β (((Ξβπ) / π) Β· (logβ(π₯ / π))))) |
115 | | vmasum 26580 |
. . . . . . . . . . . . . . 15
β’ (π β β β
Ξ£π β {π¦ β β β£ π¦ β₯ π} (Ξβπ) = (logβπ)) |
116 | 3, 115 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β {π¦ β β β£ π¦ β₯ π} (Ξβπ) = (logβπ)) |
117 | 116 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β {π¦ β β β£ π¦ β₯ π} (Ξβπ) / π) = ((logβπ) / π)) |
118 | | fzfid 13885 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (1...π) β Fin) |
119 | | dvdsssfz1 16207 |
. . . . . . . . . . . . . . . 16
β’ (π β β β {π¦ β β β£ π¦ β₯ π} β (1...π)) |
120 | 3, 119 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β {π¦ β β β£ π¦ β₯ π} β (1...π)) |
121 | 118, 120 | ssfid 9218 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β {π¦ β β β£ π¦ β₯ π} β Fin) |
122 | 3 | nncnd 12176 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
123 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . . 18
β’ {π¦ β β β£ π¦ β₯ π} β β |
124 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β π β {π¦ β β β£ π¦ β₯ π}) |
125 | 123, 124 | sselid 3947 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β) |
126 | 125, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β (Ξβπ) β β) |
127 | 126 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β (Ξβπ) β β) |
128 | 127 | anassrs 469 |
. . . . . . . . . . . . . 14
β’
((((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β§ π β {π¦ β β β£ π¦ β₯ π}) β (Ξβπ) β β) |
129 | 3 | nnne0d 12210 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β 0) |
130 | 121, 122,
128, 129 | fsumdivc 15678 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β {π¦ β β β£ π¦ β₯ π} (Ξβπ) / π) = Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) / π)) |
131 | 117, 130 | eqtr3d 2779 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((logβπ) / π) = Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) / π)) |
132 | 131 | sumeq2dv 15595 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((logβπ) / π) = Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) / π)) |
133 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = (π Β· π) β ((Ξβπ) / π) = ((Ξβπ) / (π Β· π))) |
134 | 2 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β) |
135 | 134 | nncnd 12176 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β) |
136 | 134 | nnne0d 12210 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β π β 0) |
137 | 127, 135,
136 | divcld 11938 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ (π β (1...(ββπ₯)) β§ π β {π¦ β β β£ π¦ β₯ π})) β ((Ξβπ) / π) β β) |
138 | 133, 10, 137 | dvdsflsumcom 26553 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) / π) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) / (π Β· π))) |
139 | 132, 138 | eqtrd 2777 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((logβπ) / π) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) / (π Β· π))) |
140 | 139 | oveq1d 7377 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((logβπ) / π) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π)))) = (Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((Ξβπ) / (π Β· π)) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))))) |
141 | 89, 114, 140 | 3eqtr4rd 2788 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((logβπ) / π) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π)))) = Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π))))) |
142 | 141 | oveq1d 7377 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((logβπ) / π) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π)))) / (logβπ₯)) = (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯))) |
143 | 77, 78, 142 | 3eqtr2d 2783 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2)) β ((Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)) β ((logβπ₯) / 2))) = (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯))) |
144 | 143 | mpteq2dva 5210 |
. . . . 5
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2)) β ((Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)) β ((logβπ₯) / 2)))) = (π₯ β (1(,)+β) β¦ (Ξ£π β
(1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯)))) |
145 | | 1red 11163 |
. . . . . . 7
β’ (β€
β 1 β β) |
146 | 1, 65 | fsumrecl 15626 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β β) |
147 | 146, 24 | rerpdivcld 12995 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯)) β β) |
148 | | ioossre 13332 |
. . . . . . . . . . 11
β’
(1(,)+β) β β |
149 | | ax-1cn 11116 |
. . . . . . . . . . 11
β’ 1 β
β |
150 | | o1const 15509 |
. . . . . . . . . . 11
β’
(((1(,)+β) β β β§ 1 β β) β (π₯ β (1(,)+β) β¦
1) β π(1)) |
151 | 148, 149,
150 | mp2an 691 |
. . . . . . . . . 10
β’ (π₯ β (1(,)+β) β¦
1) β π(1) |
152 | 151 | a1i 11 |
. . . . . . . . 9
β’ (β€
β (π₯ β
(1(,)+β) β¦ 1) β π(1)) |
153 | 147 | recnd 11190 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯)) β β) |
154 | 12 | rpcnd 12966 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β) |
155 | 146 | recnd 11190 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β β) |
156 | 155, 23, 23, 25 | divsubdird 11977 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β (logβπ₯)) / (logβπ₯)) = ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯)) β ((logβπ₯) / (logβπ₯)))) |
157 | 155, 23 | subcld 11519 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β (logβπ₯)) β β) |
158 | 157, 23, 25 | divrecd 11941 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β (logβπ₯)) / (logβπ₯)) = ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β (logβπ₯)) Β· (1 / (logβπ₯)))) |
159 | 23, 25 | dividd 11936 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β ((logβπ₯) / (logβπ₯)) = 1) |
160 | 159 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯)) β ((logβπ₯) / (logβπ₯))) = ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯)) β 1)) |
161 | 156, 158,
160 | 3eqtr3rd 2786 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯)) β 1) = ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β (logβπ₯)) Β· (1 / (logβπ₯)))) |
162 | 161 | mpteq2dva 5210 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯)) β 1)) = (π₯ β (1(,)+β) β¦ ((Ξ£π β
(1...(ββπ₯))((Ξβπ) / π) β (logβπ₯)) Β· (1 / (logβπ₯))))) |
163 | 146, 19 | resubcld 11590 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β (logβπ₯)) β β) |
164 | | vmadivsum 26846 |
. . . . . . . . . . . . . 14
β’ (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((Ξβπ) / π) β (logβπ₯))) β π(1) |
165 | 164 | a1i 11 |
. . . . . . . . . . . . 13
β’ (β€
β (π₯ β
β+ β¦ (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β (logβπ₯))) β π(1)) |
166 | 46, 165 | o1res2 15452 |
. . . . . . . . . . . 12
β’ (β€
β (π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β (logβπ₯))) β π(1)) |
167 | 163, 44, 166, 55 | o1mul2 15514 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) β (logβπ₯)) Β· (1 / (logβπ₯)))) β
π(1)) |
168 | 162, 167 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯)) β 1)) β
π(1)) |
169 | 153, 154,
168 | o1dif 15519 |
. . . . . . . . 9
β’ (β€
β ((π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯))) β π(1) β (π₯ β (1(,)+β) β¦
1) β π(1))) |
170 | 152, 169 | mpbird 257 |
. . . . . . . 8
β’ (β€
β (π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯))) β π(1)) |
171 | 147, 170 | o1lo1d 15428 |
. . . . . . 7
β’ (β€
β (π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯))) β β€π(1)) |
172 | 95, 69 | resubcld 11590 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))) β β) |
173 | 65, 172 | remulcld 11192 |
. . . . . . . . 9
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π)))) β β) |
174 | 1, 173 | fsumrecl 15626 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β β) |
175 | 174, 24 | rerpdivcld 12995 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯)) β β) |
176 | | 1red 11163 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 1 β
β) |
177 | | vmage0 26486 |
. . . . . . . . . . . . . 14
β’ (π β β β 0 β€
(Ξβπ)) |
178 | 62, 177 | syl 17 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 0 β€
(Ξβπ)) |
179 | 64, 67, 178 | divge0d 13004 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 0 β€
((Ξβπ) / π)) |
180 | 68 | rpred 12964 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π₯ / π) β β) |
181 | 91 | mulid2d 11180 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (1 Β· π) = π) |
182 | | fznnfl 13774 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (π β
(1...(ββπ₯))
β (π β β
β§ π β€ π₯))) |
183 | 10, 182 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (π β (1...(ββπ₯)) β (π β β β§ π β€ π₯))) |
184 | 183 | simplbda 501 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β€ π₯) |
185 | 181, 184 | eqbrtrd 5132 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (1 Β· π) β€ π₯) |
186 | 10 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π₯ β β) |
187 | 176, 186,
67 | lemuldivd 13013 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((1 Β· π) β€ π₯ β 1 β€ (π₯ / π))) |
188 | 185, 187 | mpbid 231 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 1 β€ (π₯ / π)) |
189 | | harmonicubnd 26375 |
. . . . . . . . . . . . . 14
β’ (((π₯ / π) β β β§ 1 β€ (π₯ / π)) β Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β€ ((logβ(π₯ / π)) + 1)) |
190 | 180, 188,
189 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β€ ((logβ(π₯ / π)) + 1)) |
191 | 95, 69, 176 | lesubadd2d 11761 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))) β€ 1 β Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β€ ((logβ(π₯ / π)) + 1))) |
192 | 190, 191 | mpbird 257 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))) β€ 1) |
193 | 172, 176,
65, 179, 192 | lemul2ad 12102 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π)))) β€ (((Ξβπ) / π) Β· 1)) |
194 | 93 | mulid1d 11179 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ) /
π) Β· 1) =
((Ξβπ) / π)) |
195 | 193, 194 | breqtrd 5136 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β
(((Ξβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π)))) β€ ((Ξβπ) / π)) |
196 | 1, 173, 65, 195 | fsumle 15691 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) β€ Ξ£π β (1...(ββπ₯))((Ξβπ) / π)) |
197 | 174, 146,
24, 196 | lediv1dd 13022 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯)) β€ (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯))) |
198 | 197 | adantrr 716 |
. . . . . . 7
β’
((β€ β§ (π₯
β (1(,)+β) β§ 1 β€ π₯)) β (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯)) β€ (Ξ£π β (1...(ββπ₯))((Ξβπ) / π) / (logβπ₯))) |
199 | 145, 171,
147, 175, 198 | lo1le 15543 |
. . . . . 6
β’ (β€
β (π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯))) β β€π(1)) |
200 | | 0red 11165 |
. . . . . . 7
β’ (β€
β 0 β β) |
201 | | harmoniclbnd 26374 |
. . . . . . . . . . . 12
β’ ((π₯ / π) β β+ β
(logβ(π₯ / π)) β€ Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π)) |
202 | 68, 201 | syl 17 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (logβ(π₯ / π)) β€ Ξ£π β (1...(ββ(π₯ / π)))(1 / π)) |
203 | 95, 69 | subge0d 11752 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (0 β€ (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))) β (logβ(π₯ / π)) β€ Ξ£π β (1...(ββ(π₯ / π)))(1 / π))) |
204 | 202, 203 | mpbird 257 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 0 β€ (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π)))) |
205 | 65, 172, 179, 204 | mulge0d 11739 |
. . . . . . . . 9
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 0 β€
(((Ξβπ) /
π) Β· (Ξ£π β
(1...(ββ(π₯ /
π)))(1 / π) β (logβ(π₯ / π))))) |
206 | 1, 173, 205 | fsumge0 15687 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π))))) |
207 | 174, 24, 206 | divge0d 13004 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯))) |
208 | 175, 200,
207 | o1lo12 15427 |
. . . . . 6
β’ (β€
β ((π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯))) β π(1) β (π₯ β (1(,)+β) β¦
(Ξ£π β
(1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯))) β
β€π(1))) |
209 | 199, 208 | mpbird 257 |
. . . . 5
β’ (β€
β (π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (Ξ£π β (1...(ββ(π₯ / π)))(1 / π) β (logβ(π₯ / π)))) / (logβπ₯))) β π(1)) |
210 | 144, 209 | eqeltrd 2838 |
. . . 4
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2)) β ((Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)) β ((logβπ₯) / 2)))) β
π(1)) |
211 | 60, 76, 210 | o1dif 15519 |
. . 3
β’ (β€
β ((π₯ β
(1(,)+β) β¦ ((Ξ£π β (1...(ββπ₯))((logβπ) / π) / (logβπ₯)) β ((logβπ₯) / 2))) β π(1) β (π₯ β (1(,)+β) β¦
((Ξ£π β
(1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)) β ((logβπ₯) / 2))) β
π(1))) |
212 | 57, 211 | mpbid 231 |
. 2
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((Ξ£π β (1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)) β ((logβπ₯) / 2))) β
π(1)) |
213 | 212 | mptru 1549 |
1
β’ (π₯ β (1(,)+β) β¦
((Ξ£π β
(1...(ββπ₯))(((Ξβπ) / π) Β· (logβ(π₯ / π))) / (logβπ₯)) β ((logβπ₯) / 2))) β π(1) |