Step | Hyp | Ref
| Expression |
1 | | 1red 11163 |
. 2
β’ (π β 1 β
β) |
2 | | dchrvmasum.c |
. . . . . . 7
β’ (π β πΆ β (0[,)+β)) |
3 | | elrege0 13378 |
. . . . . . 7
β’ (πΆ β (0[,)+β) β
(πΆ β β β§ 0
β€ πΆ)) |
4 | 2, 3 | sylib 217 |
. . . . . 6
β’ (π β (πΆ β β β§ 0 β€ πΆ)) |
5 | 4 | simpld 496 |
. . . . 5
β’ (π β πΆ β β) |
6 | 5 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β β+) β πΆ β
β) |
7 | | fzfid 13885 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
8 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
9 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ₯))
β π β
β) |
10 | 9 | nnrpd 12962 |
. . . . . . . 8
β’ (π β
(1...(ββπ₯))
β π β
β+) |
11 | | rpdivcl 12947 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
β+) β (π₯ / π) β
β+) |
12 | 8, 10, 11 | syl2an 597 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
13 | 12 | relogcld 25994 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
14 | 8 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π₯ β
β+) |
15 | 13, 14 | rerpdivcld 12995 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / π₯) β β) |
16 | 7, 15 | fsumrecl 15626 |
. . . 4
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯) β β) |
17 | 6, 16 | remulcld 11192 |
. . 3
β’ ((π β§ π₯ β β+) β (πΆ Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) β β) |
18 | | dchrvmasum.r |
. . . . 5
β’ (π β π
β β) |
19 | | 3nn 12239 |
. . . . . . 7
β’ 3 β
β |
20 | | nnrp 12933 |
. . . . . . 7
β’ (3 β
β β 3 β β+) |
21 | | relogcl 25947 |
. . . . . . 7
β’ (3 β
β+ β (logβ3) β β) |
22 | 19, 20, 21 | mp2b 10 |
. . . . . 6
β’
(logβ3) β β |
23 | | 1re 11162 |
. . . . . 6
β’ 1 β
β |
24 | 22, 23 | readdcli 11177 |
. . . . 5
β’
((logβ3) + 1) β β |
25 | | remulcl 11143 |
. . . . 5
β’ ((π
β β β§
((logβ3) + 1) β β) β (π
Β· ((logβ3) + 1)) β
β) |
26 | 18, 24, 25 | sylancl 587 |
. . . 4
β’ (π β (π
Β· ((logβ3) + 1)) β
β) |
27 | 26 | adantr 482 |
. . 3
β’ ((π β§ π₯ β β+) β (π
Β· ((logβ3) + 1))
β β) |
28 | | rpssre 12929 |
. . . . 5
β’
β+ β β |
29 | 5 | recnd 11190 |
. . . . 5
β’ (π β πΆ β β) |
30 | | o1const 15509 |
. . . . 5
β’
((β+ β β β§ πΆ β β) β (π₯ β β+ β¦ πΆ) β
π(1)) |
31 | 28, 29, 30 | sylancr 588 |
. . . 4
β’ (π β (π₯ β β+ β¦ πΆ) β
π(1)) |
32 | | logfacrlim2 26590 |
. . . . 5
β’ (π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) βπ
1 |
33 | | rlimo1 15506 |
. . . . 5
β’ ((π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) βπ 1 β
(π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))((logβ(π₯ / π)) / π₯)) β π(1)) |
34 | 32, 33 | mp1i 13 |
. . . 4
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) β π(1)) |
35 | 6, 16, 31, 34 | o1mul2 15514 |
. . 3
β’ (π β (π₯ β β+ β¦ (πΆ Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯))) β π(1)) |
36 | 26 | recnd 11190 |
. . . 4
β’ (π β (π
Β· ((logβ3) + 1)) β
β) |
37 | | o1const 15509 |
. . . 4
β’
((β+ β β β§ (π
Β· ((logβ3) + 1)) β
β) β (π₯ β
β+ β¦ (π
Β· ((logβ3) + 1))) β
π(1)) |
38 | 28, 36, 37 | sylancr 588 |
. . 3
β’ (π β (π₯ β β+ β¦ (π
Β· ((logβ3) + 1)))
β π(1)) |
39 | 17, 27, 35, 38 | o1add2 15513 |
. 2
β’ (π β (π₯ β β+ β¦ ((πΆ Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) + 1)))) β
π(1)) |
40 | 17, 27 | readdcld 11191 |
. 2
β’ ((π β§ π₯ β β+) β ((πΆ Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) + 1))) β
β) |
41 | | dchrvmasum.g |
. . . . . . . . 9
β’ (π = (π₯ / π) β πΉ = πΎ) |
42 | 41 | eleq1d 2823 |
. . . . . . . 8
β’ (π = (π₯ / π) β (πΉ β β β πΎ β β)) |
43 | | dchrvmasum.f |
. . . . . . . . . 10
β’ ((π β§ π β β+) β πΉ β
β) |
44 | 43 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β β+ πΉ β β) |
45 | 44 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β βπ β
β+ πΉ
β β) |
46 | 42, 45, 12 | rspcdva 3585 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β πΎ β
β) |
47 | | dchrvmasum.t |
. . . . . . . 8
β’ (π β π β β) |
48 | 47 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
49 | 46, 48 | subcld 11519 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΎ β π) β
β) |
50 | 49 | abscld 15328 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(πΎ
β π)) β
β) |
51 | 9 | adantl 483 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
52 | 50, 51 | nndivred 12214 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(πΎ
β π)) / π) β
β) |
53 | 7, 52 | fsumrecl 15626 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π) β β) |
54 | 53 | recnd 11190 |
. 2
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π) β β) |
55 | 51 | nnrpd 12962 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β+) |
56 | 49 | absge0d 15336 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ(πΎ
β π))) |
57 | 50, 55, 56 | divge0d 13004 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ ((absβ(πΎ β π)) / π)) |
58 | 7, 52, 57 | fsumge0 15687 |
. . . . . 6
β’ ((π β§ π₯ β β+) β 0 β€
Ξ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) |
59 | 53, 58 | absidd 15314 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) = Ξ£π β (1...(ββπ₯))((absβ(πΎ β π)) / π)) |
60 | 59, 53 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) β β) |
61 | 40 | recnd 11190 |
. . . . 5
β’ ((π β§ π₯ β β+) β ((πΆ Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) + 1))) β
β) |
62 | 61 | abscld 15328 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβ((πΆ Β·
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) + 1)))) β
β) |
63 | | 3re 12240 |
. . . . . . . 8
β’ 3 β
β |
64 | 63 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β 3 β
β) |
65 | | 1le3 12372 |
. . . . . . 7
β’ 1 β€
3 |
66 | 64, 65 | jctir 522 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (3 β
β β§ 1 β€ 3)) |
67 | 18 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β π
β
β) |
68 | 23 | rexri 11220 |
. . . . . . . . . 10
β’ 1 β
β* |
69 | 63 | rexri 11220 |
. . . . . . . . . 10
β’ 3 β
β* |
70 | | 1lt3 12333 |
. . . . . . . . . 10
β’ 1 <
3 |
71 | | lbico1 13325 |
. . . . . . . . . 10
β’ ((1
β β* β§ 3 β β* β§ 1 < 3)
β 1 β (1[,)3)) |
72 | 68, 69, 70, 71 | mp3an 1462 |
. . . . . . . . 9
β’ 1 β
(1[,)3) |
73 | | 0red 11165 |
. . . . . . . . . . 11
β’ ((π β§ π β (1[,)3)) β 0 β
β) |
74 | | elico2 13335 |
. . . . . . . . . . . . . . 15
β’ ((1
β β β§ 3 β β*) β (π β (1[,)3) β (π β β β§ 1 β€ π β§ π < 3))) |
75 | 23, 69, 74 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (π β (1[,)3) β (π β β β§ 1 β€
π β§ π < 3)) |
76 | 75 | simp1bi 1146 |
. . . . . . . . . . . . 13
β’ (π β (1[,)3) β π β
β) |
77 | | 0red 11165 |
. . . . . . . . . . . . . 14
β’ (π β (1[,)3) β 0 β
β) |
78 | | 1red 11163 |
. . . . . . . . . . . . . 14
β’ (π β (1[,)3) β 1 β
β) |
79 | | 0lt1 11684 |
. . . . . . . . . . . . . . 15
β’ 0 <
1 |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (1[,)3) β 0 <
1) |
81 | 75 | simp2bi 1147 |
. . . . . . . . . . . . . 14
β’ (π β (1[,)3) β 1 β€
π) |
82 | 77, 78, 76, 80, 81 | ltletrd 11322 |
. . . . . . . . . . . . 13
β’ (π β (1[,)3) β 0 <
π) |
83 | 76, 82 | elrpd 12961 |
. . . . . . . . . . . 12
β’ (π β (1[,)3) β π β
β+) |
84 | 47 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β+) β π β
β) |
85 | 43, 84 | subcld 11519 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β+) β (πΉ β π) β β) |
86 | 85 | abscld 15328 |
. . . . . . . . . . . 12
β’ ((π β§ π β β+) β
(absβ(πΉ β π)) β
β) |
87 | 83, 86 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ π β (1[,)3)) β (absβ(πΉ β π)) β β) |
88 | 18 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (1[,)3)) β π
β β) |
89 | 85 | absge0d 15336 |
. . . . . . . . . . . 12
β’ ((π β§ π β β+) β 0 β€
(absβ(πΉ β π))) |
90 | 83, 89 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ π β (1[,)3)) β 0 β€
(absβ(πΉ β π))) |
91 | | dchrvmasum.2 |
. . . . . . . . . . . 12
β’ (π β βπ β (1[,)3)(absβ(πΉ β π)) β€ π
) |
92 | 91 | r19.21bi 3237 |
. . . . . . . . . . 11
β’ ((π β§ π β (1[,)3)) β (absβ(πΉ β π)) β€ π
) |
93 | 73, 87, 88, 90, 92 | letrd 11319 |
. . . . . . . . . 10
β’ ((π β§ π β (1[,)3)) β 0 β€ π
) |
94 | 93 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β (1[,)3)0 β€ π
) |
95 | | biidd 262 |
. . . . . . . . . 10
β’ (π = 1 β (0 β€ π
β 0 β€ π
)) |
96 | 95 | rspcv 3580 |
. . . . . . . . 9
β’ (1 β
(1[,)3) β (βπ
β (1[,)3)0 β€ π
β 0 β€ π
)) |
97 | 72, 94, 96 | mpsyl 68 |
. . . . . . . 8
β’ (π β 0 β€ π
) |
98 | 97 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β 0 β€
π
) |
99 | 67, 98 | jca 513 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (π
β β β§ 0 β€
π
)) |
100 | 50 | recnd 11190 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(πΎ
β π)) β
β) |
101 | 5 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β πΆ β
β) |
102 | 101, 15 | remulcld 11192 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΆ Β·
((logβ(π₯ / π)) / π₯)) β β) |
103 | 4 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΆ β β
β§ 0 β€ πΆ)) |
104 | | log1 25957 |
. . . . . . . . 9
β’
(logβ1) = 0 |
105 | 51 | nncnd 12176 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
106 | 105 | mulid2d 11180 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 Β· π) =
π) |
107 | | rpre 12930 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β π₯ β
β) |
108 | 107 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β π₯ β
β) |
109 | | fznnfl 13774 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β (π β
(1...(ββπ₯))
β (π β β
β§ π β€ π₯))) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β (π β
(1...(ββπ₯))
β (π β β
β§ π β€ π₯))) |
111 | 110 | simplbda 501 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β€ π₯) |
112 | 106, 111 | eqbrtrd 5132 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 Β· π) β€
π₯) |
113 | | 1red 11163 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 1 β β) |
114 | 107 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π₯ β
β) |
115 | 113, 114,
55 | lemuldivd 13013 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((1 Β· π) β€
π₯ β 1 β€ (π₯ / π))) |
116 | 112, 115 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 1 β€ (π₯ / π)) |
117 | | 1rp 12926 |
. . . . . . . . . . . 12
β’ 1 β
β+ |
118 | 117 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 1 β β+) |
119 | 118, 12 | logled 25998 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 β€ (π₯ / π) β (logβ1) β€
(logβ(π₯ / π)))) |
120 | 116, 119 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (logβ1) β€ (logβ(π₯ / π))) |
121 | 104, 120 | eqbrtrrid 5146 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (logβ(π₯
/ π))) |
122 | | rpregt0 12936 |
. . . . . . . . 9
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
123 | 122 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ β β
β§ 0 < π₯)) |
124 | | divge0 12031 |
. . . . . . . 8
β’
((((logβ(π₯ /
π)) β β β§ 0
β€ (logβ(π₯ / π))) β§ (π₯ β β β§ 0 < π₯)) β 0 β€
((logβ(π₯ / π)) / π₯)) |
125 | 13, 121, 123, 124 | syl21anc 837 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ ((logβ(π₯ / π)) / π₯)) |
126 | | mulge0 11680 |
. . . . . . 7
β’ (((πΆ β β β§ 0 β€
πΆ) β§
(((logβ(π₯ / π)) / π₯) β β β§ 0 β€
((logβ(π₯ / π)) / π₯))) β 0 β€ (πΆ Β· ((logβ(π₯ / π)) / π₯))) |
127 | 103, 15, 125, 126 | syl12anc 836 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (πΆ Β·
((logβ(π₯ / π)) / π₯))) |
128 | | absidm 15215 |
. . . . . . . . 9
β’ ((πΎ β π) β β β
(absβ(absβ(πΎ
β π))) =
(absβ(πΎ β π))) |
129 | 49, 128 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(absβ(πΎ β π))) = (absβ(πΎ β π))) |
130 | 129 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ 3 β€ (π₯ / π)) β
(absβ(absβ(πΎ
β π))) =
(absβ(πΎ β π))) |
131 | 41 | fvoveq1d 7384 |
. . . . . . . . . 10
β’ (π = (π₯ / π) β (absβ(πΉ β π)) = (absβ(πΎ β π))) |
132 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = (π₯ / π) β (logβπ) = (logβ(π₯ / π))) |
133 | | id 22 |
. . . . . . . . . . . 12
β’ (π = (π₯ / π) β π = (π₯ / π)) |
134 | 132, 133 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = (π₯ / π) β ((logβπ) / π) = ((logβ(π₯ / π)) / (π₯ / π))) |
135 | 134 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = (π₯ / π) β (πΆ Β· ((logβπ) / π)) = (πΆ Β· ((logβ(π₯ / π)) / (π₯ / π)))) |
136 | 131, 135 | breq12d 5123 |
. . . . . . . . 9
β’ (π = (π₯ / π) β ((absβ(πΉ β π)) β€ (πΆ Β· ((logβπ) / π)) β (absβ(πΎ β π)) β€ (πΆ Β· ((logβ(π₯ / π)) / (π₯ / π))))) |
137 | | dchrvmasum.1 |
. . . . . . . . . . 11
β’ ((π β§ π β (3[,)+β)) β
(absβ(πΉ β π)) β€ (πΆ Β· ((logβπ) / π))) |
138 | 137 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (π β βπ β (3[,)+β)(absβ(πΉ β π)) β€ (πΆ Β· ((logβπ) / π))) |
139 | 138 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ 3 β€ (π₯ / π)) β βπ β
(3[,)+β)(absβ(πΉ
β π)) β€ (πΆ Β· ((logβπ) / π))) |
140 | | nndivre 12201 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π β β) β (π₯ / π) β β) |
141 | 108, 9, 140 | syl2an 597 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β) |
142 | 141 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ 3 β€ (π₯ / π)) β (π₯ / π) β β) |
143 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ 3 β€ (π₯ / π)) β 3 β€ (π₯ / π)) |
144 | | elicopnf 13369 |
. . . . . . . . . . 11
β’ (3 β
β β ((π₯ / π) β (3[,)+β) β
((π₯ / π) β β β§ 3 β€ (π₯ / π)))) |
145 | 63, 144 | ax-mp 5 |
. . . . . . . . . 10
β’ ((π₯ / π) β (3[,)+β) β ((π₯ / π) β β β§ 3 β€ (π₯ / π))) |
146 | 142, 143,
145 | sylanbrc 584 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ 3 β€ (π₯ / π)) β (π₯ / π) β (3[,)+β)) |
147 | 136, 139,
146 | rspcdva 3585 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ 3 β€ (π₯ / π)) β (absβ(πΎ β π)) β€ (πΆ Β· ((logβ(π₯ / π)) / (π₯ / π)))) |
148 | 13 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (logβ(π₯ /
π)) β
β) |
149 | | rpcnne0 12940 |
. . . . . . . . . . . . . 14
β’ (π₯ β β+
β (π₯ β β
β§ π₯ β
0)) |
150 | 149 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ β β
β§ π₯ β
0)) |
151 | 55 | rpcnne0d 12973 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π β β
β§ π β
0)) |
152 | | divdiv2 11874 |
. . . . . . . . . . . . 13
β’
(((logβ(π₯ /
π)) β β β§
(π₯ β β β§
π₯ β 0) β§ (π β β β§ π β 0)) β
((logβ(π₯ / π)) / (π₯ / π)) = (((logβ(π₯ / π)) Β· π) / π₯)) |
153 | 148, 150,
151, 152 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / (π₯ / π)) = (((logβ(π₯ / π)) Β· π) / π₯)) |
154 | | div23 11839 |
. . . . . . . . . . . . 13
β’
(((logβ(π₯ /
π)) β β β§
π β β β§
(π₯ β β β§
π₯ β 0)) β
(((logβ(π₯ / π)) Β· π) / π₯) = (((logβ(π₯ / π)) / π₯) Β· π)) |
155 | 148, 105,
150, 154 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((logβ(π₯ /
π)) Β· π) / π₯) = (((logβ(π₯ / π)) / π₯) Β· π)) |
156 | 153, 155 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / (π₯ / π)) = (((logβ(π₯ / π)) / π₯) Β· π)) |
157 | 156 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΆ Β·
((logβ(π₯ / π)) / (π₯ / π))) = (πΆ Β· (((logβ(π₯ / π)) / π₯) Β· π))) |
158 | 29 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β πΆ β
β) |
159 | 15 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((logβ(π₯ /
π)) / π₯) β β) |
160 | 158, 159,
105 | mulassd 11185 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((πΆ Β·
((logβ(π₯ / π)) / π₯)) Β· π) = (πΆ Β· (((logβ(π₯ / π)) / π₯) Β· π))) |
161 | 157, 160 | eqtr4d 2780 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΆ Β·
((logβ(π₯ / π)) / (π₯ / π))) = ((πΆ Β· ((logβ(π₯ / π)) / π₯)) Β· π)) |
162 | 161 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ 3 β€ (π₯ / π)) β (πΆ Β· ((logβ(π₯ / π)) / (π₯ / π))) = ((πΆ Β· ((logβ(π₯ / π)) / π₯)) Β· π)) |
163 | 147, 162 | breqtrd 5136 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ 3 β€ (π₯ / π)) β (absβ(πΎ β π)) β€ ((πΆ Β· ((logβ(π₯ / π)) / π₯)) Β· π)) |
164 | 130, 163 | eqbrtrd 5132 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ 3 β€ (π₯ / π)) β
(absβ(absβ(πΎ
β π))) β€ ((πΆ Β· ((logβ(π₯ / π)) / π₯)) Β· π)) |
165 | 129 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < 3) β
(absβ(absβ(πΎ
β π))) =
(absβ(πΎ β π))) |
166 | 131 | breq1d 5120 |
. . . . . . . 8
β’ (π = (π₯ / π) β ((absβ(πΉ β π)) β€ π
β (absβ(πΎ β π)) β€ π
)) |
167 | 91 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < 3) β βπ β (1[,)3)(absβ(πΉ β π)) β€ π
) |
168 | 141 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < 3) β (π₯ / π) β β) |
169 | 116 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < 3) β 1 β€ (π₯ / π)) |
170 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < 3) β (π₯ / π) < 3) |
171 | | elico2 13335 |
. . . . . . . . . 10
β’ ((1
β β β§ 3 β β*) β ((π₯ / π) β (1[,)3) β ((π₯ / π) β β β§ 1 β€ (π₯ / π) β§ (π₯ / π) < 3))) |
172 | 23, 69, 171 | mp2an 691 |
. . . . . . . . 9
β’ ((π₯ / π) β (1[,)3) β ((π₯ / π) β β β§ 1 β€ (π₯ / π) β§ (π₯ / π) < 3)) |
173 | 168, 169,
170, 172 | syl3anbrc 1344 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < 3) β (π₯ / π) β (1[,)3)) |
174 | 166, 167,
173 | rspcdva 3585 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < 3) β
(absβ(πΎ β π)) β€ π
) |
175 | 165, 174 | eqbrtrd 5132 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ (π₯ / π) < 3) β
(absβ(absβ(πΎ
β π))) β€ π
) |
176 | 8, 66, 99, 100, 102, 127, 164, 175 | fsumharmonic 26377 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) β€ (Ξ£π β (1...(ββπ₯))(πΆ Β· ((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) +
1)))) |
177 | 29 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β πΆ β
β) |
178 | 7, 177, 159 | fsummulc2 15676 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (πΆ Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) = Ξ£π β (1...(ββπ₯))(πΆ Β· ((logβ(π₯ / π)) / π₯))) |
179 | 178 | oveq1d 7377 |
. . . . 5
β’ ((π β§ π₯ β β+) β ((πΆ Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) + 1))) =
(Ξ£π β
(1...(ββπ₯))(πΆ Β· ((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) +
1)))) |
180 | 176, 179 | breqtrrd 5138 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) β€ ((πΆ Β· Ξ£π β (1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) +
1)))) |
181 | 40 | leabsd 15306 |
. . . 4
β’ ((π β§ π₯ β β+) β ((πΆ Β· Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) + 1))) β€
(absβ((πΆ Β·
Ξ£π β
(1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) +
1))))) |
182 | 60, 40, 62, 180, 181 | letrd 11319 |
. . 3
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) β€ (absβ((πΆ Β· Ξ£π β (1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) +
1))))) |
183 | 182 | adantrr 716 |
. 2
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) β€ (absβ((πΆ Β· Ξ£π β (1...(ββπ₯))((logβ(π₯ / π)) / π₯)) + (π
Β· ((logβ3) +
1))))) |
184 | 1, 39, 40, 54, 183 | o1le 15544 |
1
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) β π(1)) |