Step | Hyp | Ref
| Expression |
1 | | halfre 12374 |
. . . . . . . . 9
β’ (1 / 2)
β β |
2 | | 1re 11162 |
. . . . . . . . . 10
β’ 1 β
β |
3 | | rpre 12930 |
. . . . . . . . . 10
β’ (π¦ β β+
β π¦ β
β) |
4 | | resubcl 11472 |
. . . . . . . . . 10
β’ ((1
β β β§ π¦
β β) β (1 β π¦) β β) |
5 | 2, 3, 4 | sylancr 588 |
. . . . . . . . 9
β’ (π¦ β β+
β (1 β π¦) β
β) |
6 | | ifcl 4536 |
. . . . . . . . 9
β’ (((1 / 2)
β β β§ (1 β π¦) β β) β if((1 β π¦) β€ (1 / 2), (1 / 2), (1
β π¦)) β
β) |
7 | 1, 5, 6 | sylancr 588 |
. . . . . . . 8
β’ (π¦ β β+
β if((1 β π¦)
β€ (1 / 2), (1 / 2), (1 β π¦)) β β) |
8 | | 0red 11165 |
. . . . . . . . 9
β’ (π¦ β β+
β 0 β β) |
9 | 1 | a1i 11 |
. . . . . . . . 9
β’ (π¦ β β+
β (1 / 2) β β) |
10 | | halfgt0 12376 |
. . . . . . . . . 10
β’ 0 < (1
/ 2) |
11 | 10 | a1i 11 |
. . . . . . . . 9
β’ (π¦ β β+
β 0 < (1 / 2)) |
12 | | max2 13113 |
. . . . . . . . . 10
β’ (((1
β π¦) β β
β§ (1 / 2) β β) β (1 / 2) β€ if((1 β π¦) β€ (1 / 2), (1 / 2), (1
β π¦))) |
13 | 5, 1, 12 | sylancl 587 |
. . . . . . . . 9
β’ (π¦ β β+
β (1 / 2) β€ if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦))) |
14 | 8, 9, 7, 11, 13 | ltletrd 11322 |
. . . . . . . 8
β’ (π¦ β β+
β 0 < if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦))) |
15 | 7, 14 | elrpd 12961 |
. . . . . . 7
β’ (π¦ β β+
β if((1 β π¦)
β€ (1 / 2), (1 / 2), (1 β π¦)) β
β+) |
16 | 15 | rpsqrtcld 15303 |
. . . . . 6
β’ (π¦ β β+
β (ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦))) β
β+) |
17 | | halflt1 12378 |
. . . . . . . . 9
β’ (1 / 2)
< 1 |
18 | | ltsubrp 12958 |
. . . . . . . . . 10
β’ ((1
β β β§ π¦
β β+) β (1 β π¦) < 1) |
19 | 2, 18 | mpan 689 |
. . . . . . . . 9
β’ (π¦ β β+
β (1 β π¦) <
1) |
20 | | breq1 5113 |
. . . . . . . . . 10
β’ ((1 / 2)
= if((1 β π¦) β€ (1
/ 2), (1 / 2), (1 β π¦)) β ((1 / 2) < 1 β if((1
β π¦) β€ (1 / 2), (1
/ 2), (1 β π¦)) <
1)) |
21 | | breq1 5113 |
. . . . . . . . . 10
β’ ((1
β π¦) = if((1 β
π¦) β€ (1 / 2), (1 / 2),
(1 β π¦)) β ((1
β π¦) < 1 β
if((1 β π¦) β€ (1 /
2), (1 / 2), (1 β π¦))
< 1)) |
22 | 20, 21 | ifboth 4530 |
. . . . . . . . 9
β’ (((1 / 2)
< 1 β§ (1 β π¦)
< 1) β if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)) < 1) |
23 | 17, 19, 22 | sylancr 588 |
. . . . . . . 8
β’ (π¦ β β+
β if((1 β π¦)
β€ (1 / 2), (1 / 2), (1 β π¦)) < 1) |
24 | 15 | rpge0d 12968 |
. . . . . . . . 9
β’ (π¦ β β+
β 0 β€ if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦))) |
25 | 2 | a1i 11 |
. . . . . . . . 9
β’ (π¦ β β+
β 1 β β) |
26 | | 0le1 11685 |
. . . . . . . . . 10
β’ 0 β€
1 |
27 | 26 | a1i 11 |
. . . . . . . . 9
β’ (π¦ β β+
β 0 β€ 1) |
28 | 7, 24, 25, 27 | sqrtltd 15319 |
. . . . . . . 8
β’ (π¦ β β+
β (if((1 β π¦)
β€ (1 / 2), (1 / 2), (1 β π¦)) < 1 β (ββif((1 β
π¦) β€ (1 / 2), (1 / 2),
(1 β π¦))) <
(ββ1))) |
29 | 23, 28 | mpbid 231 |
. . . . . . 7
β’ (π¦ β β+
β (ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦))) <
(ββ1)) |
30 | | sqrt1 15163 |
. . . . . . 7
β’
(ββ1) = 1 |
31 | 29, 30 | breqtrdi 5151 |
. . . . . 6
β’ (π¦ β β+
β (ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦))) < 1) |
32 | 16, 31 | chtppilimlem2 26838 |
. . . . 5
β’ (π¦ β β+
β βπ§ β
β βπ₯ β
(2[,)+β)(π§ β€ π₯ β (((ββif((1
β π¦) β€ (1 / 2), (1
/ 2), (1 β π¦)))β2) Β·
((Οβπ₯)
Β· (logβπ₯)))
< (ΞΈβπ₯))) |
33 | 5 | adantr 482 |
. . . . . . . . . . 11
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β (1 β π¦) β β) |
34 | | max1 13111 |
. . . . . . . . . . 11
β’ (((1
β π¦) β β
β§ (1 / 2) β β) β (1 β π¦) β€ if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦))) |
35 | 33, 1, 34 | sylancl 587 |
. . . . . . . . . 10
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β (1 β π¦) β€ if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦))) |
36 | 7 | adantr 482 |
. . . . . . . . . . 11
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)) β
β) |
37 | | 2re 12234 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
38 | | elicopnf 13369 |
. . . . . . . . . . . . . . . 16
β’ (2 β
β β (π₯ β
(2[,)+β) β (π₯
β β β§ 2 β€ π₯))) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (2[,)+β) β
(π₯ β β β§ 2
β€ π₯)) |
40 | 39 | simplbi 499 |
. . . . . . . . . . . . . 14
β’ (π₯ β (2[,)+β) β
π₯ β
β) |
41 | | chtcl 26474 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β
(ΞΈβπ₯) β
β) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . 13
β’ (π₯ β (2[,)+β) β
(ΞΈβπ₯) β
β) |
43 | | ppinncl 26539 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ 2 β€
π₯) β
(Οβπ₯)
β β) |
44 | 39, 43 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (2[,)+β) β
(Οβπ₯)
β β) |
45 | 44 | nnrpd 12962 |
. . . . . . . . . . . . . 14
β’ (π₯ β (2[,)+β) β
(Οβπ₯)
β β+) |
46 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (2[,)+β) β 1
β β) |
47 | 37 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (2[,)+β) β 2
β β) |
48 | | 1lt2 12331 |
. . . . . . . . . . . . . . . . 17
β’ 1 <
2 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (2[,)+β) β 1
< 2) |
50 | 39 | simprbi 498 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (2[,)+β) β 2
β€ π₯) |
51 | 46, 47, 40, 49, 50 | ltletrd 11322 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (2[,)+β) β 1
< π₯) |
52 | 40, 51 | rplogcld 26000 |
. . . . . . . . . . . . . 14
β’ (π₯ β (2[,)+β) β
(logβπ₯) β
β+) |
53 | 45, 52 | rpmulcld 12980 |
. . . . . . . . . . . . 13
β’ (π₯ β (2[,)+β) β
((Οβπ₯)
Β· (logβπ₯))
β β+) |
54 | 42, 53 | rerpdivcld 12995 |
. . . . . . . . . . . 12
β’ (π₯ β (2[,)+β) β
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯)))
β β) |
55 | 54 | adantl 483 |
. . . . . . . . . . 11
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β β) |
56 | | lelttr 11252 |
. . . . . . . . . . 11
β’ (((1
β π¦) β β
β§ if((1 β π¦) β€
(1 / 2), (1 / 2), (1 β π¦)) β β β§ ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β β) β (((1
β π¦) β€ if((1
β π¦) β€ (1 / 2), (1
/ 2), (1 β π¦)) β§
if((1 β π¦) β€ (1 /
2), (1 / 2), (1 β π¦))
< ((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))
β (1 β π¦) <
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))) |
57 | 33, 36, 55, 56 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β (((1 β π¦) β€ if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)) β§ if((1 β π¦) β€ (1 / 2), (1 / 2), (1
β π¦)) <
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))
β (1 β π¦) <
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))) |
58 | 35, 57 | mpand 694 |
. . . . . . . . 9
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β (if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)) < ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β (1 β π¦) < ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) |
59 | 7 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (π¦ β β+
β if((1 β π¦)
β€ (1 / 2), (1 / 2), (1 β π¦)) β β) |
60 | 59 | sqsqrtd 15331 |
. . . . . . . . . . . . 13
β’ (π¦ β β+
β ((ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)))β2) = if((1 β
π¦) β€ (1 / 2), (1 / 2),
(1 β π¦))) |
61 | 60 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)))β2) = if((1 β
π¦) β€ (1 / 2), (1 / 2),
(1 β π¦))) |
62 | 61 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β (((ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)))β2) Β·
((Οβπ₯)
Β· (logβπ₯))) =
(if((1 β π¦) β€ (1 /
2), (1 / 2), (1 β π¦))
Β· ((Οβπ₯) Β· (logβπ₯)))) |
63 | 62 | breq1d 5120 |
. . . . . . . . . 10
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((((ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)))β2) Β·
((Οβπ₯)
Β· (logβπ₯)))
< (ΞΈβπ₯)
β (if((1 β π¦)
β€ (1 / 2), (1 / 2), (1 β π¦)) Β· ((Οβπ₯) Β· (logβπ₯))) < (ΞΈβπ₯))) |
64 | 42 | adantl 483 |
. . . . . . . . . . 11
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β (ΞΈβπ₯) β β) |
65 | 53 | rpregt0d 12970 |
. . . . . . . . . . . 12
β’ (π₯ β (2[,)+β) β
(((Οβπ₯)
Β· (logβπ₯))
β β β§ 0 < ((Οβπ₯) Β· (logβπ₯)))) |
66 | 65 | adantl 483 |
. . . . . . . . . . 11
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β (((Οβπ₯) Β· (logβπ₯)) β β β§ 0 <
((Οβπ₯)
Β· (logβπ₯)))) |
67 | | ltmuldiv 12035 |
. . . . . . . . . . 11
β’ ((if((1
β π¦) β€ (1 / 2), (1
/ 2), (1 β π¦)) β
β β§ (ΞΈβπ₯) β β β§
(((Οβπ₯)
Β· (logβπ₯))
β β β§ 0 < ((Οβπ₯) Β· (logβπ₯)))) β ((if((1 β π¦) β€ (1 / 2), (1 / 2), (1
β π¦)) Β·
((Οβπ₯)
Β· (logβπ₯)))
< (ΞΈβπ₯)
β if((1 β π¦)
β€ (1 / 2), (1 / 2), (1 β π¦)) < ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) |
68 | 36, 64, 66, 67 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((if((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)) Β·
((Οβπ₯)
Β· (logβπ₯)))
< (ΞΈβπ₯)
β if((1 β π¦)
β€ (1 / 2), (1 / 2), (1 β π¦)) < ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) |
69 | 63, 68 | bitrd 279 |
. . . . . . . . 9
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((((ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)))β2) Β·
((Οβπ₯)
Β· (logβπ₯)))
< (ΞΈβπ₯)
β if((1 β π¦)
β€ (1 / 2), (1 / 2), (1 β π¦)) < ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) |
70 | | 0red 11165 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (2[,)+β) β 0
β β) |
71 | | 2pos 12263 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 <
2 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (2[,)+β) β 0
< 2) |
73 | 70, 47, 40, 72, 50 | ltletrd 11322 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (2[,)+β) β 0
< π₯) |
74 | 40, 73 | elrpd 12961 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (2[,)+β) β
π₯ β
β+) |
75 | | chtleppi 26574 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β+
β (ΞΈβπ₯)
β€ ((Οβπ₯)
Β· (logβπ₯))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (2[,)+β) β
(ΞΈβπ₯) β€
((Οβπ₯)
Β· (logβπ₯))) |
77 | 53 | rpcnd 12966 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (2[,)+β) β
((Οβπ₯)
Β· (logβπ₯))
β β) |
78 | 77 | mulid1d 11179 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (2[,)+β) β
(((Οβπ₯)
Β· (logβπ₯))
Β· 1) = ((Οβπ₯) Β· (logβπ₯))) |
79 | 76, 78 | breqtrrd 5138 |
. . . . . . . . . . . . . 14
β’ (π₯ β (2[,)+β) β
(ΞΈβπ₯) β€
(((Οβπ₯)
Β· (logβπ₯))
Β· 1)) |
80 | 42, 46, 53 | ledivmuld 13017 |
. . . . . . . . . . . . . 14
β’ (π₯ β (2[,)+β) β
(((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯)))
β€ 1 β (ΞΈβπ₯) β€ (((Οβπ₯) Β· (logβπ₯)) Β·
1))) |
81 | 79, 80 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (π₯ β (2[,)+β) β
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯)))
β€ 1) |
82 | 54, 46, 81 | abssuble0d 15324 |
. . . . . . . . . . . 12
β’ (π₯ β (2[,)+β) β
(absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) = (1 β
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))) |
83 | 82 | breq1d 5120 |
. . . . . . . . . . 11
β’ (π₯ β (2[,)+β) β
((absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦ β (1 β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) < π¦)) |
84 | 83 | adantl 483 |
. . . . . . . . . 10
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦ β (1 β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) < π¦)) |
85 | 2 | a1i 11 |
. . . . . . . . . . 11
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β 1 β β) |
86 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β π¦
β β) |
87 | | ltsub23 11642 |
. . . . . . . . . . 11
β’ ((1
β β β§ ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β β β§ π¦ β β) β ((1 β
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))
< π¦ β (1 β
π¦) <
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))) |
88 | 85, 55, 86, 87 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((1 β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) < π¦ β (1 β π¦) < ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) |
89 | 84, 88 | bitrd 279 |
. . . . . . . . 9
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦ β (1 β π¦) < ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) |
90 | 58, 69, 89 | 3imtr4d 294 |
. . . . . . . 8
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((((ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)))β2) Β·
((Οβπ₯)
Β· (logβπ₯)))
< (ΞΈβπ₯)
β (absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦)) |
91 | 90 | imim2d 57 |
. . . . . . 7
β’ ((π¦ β β+
β§ π₯ β
(2[,)+β)) β ((π§
β€ π₯ β
(((ββif((1 β π¦) β€ (1 / 2), (1 / 2), (1 β π¦)))β2) Β·
((Οβπ₯)
Β· (logβπ₯)))
< (ΞΈβπ₯))
β (π§ β€ π₯ β
(absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦))) |
92 | 91 | ralimdva 3165 |
. . . . . 6
β’ (π¦ β β+
β (βπ₯ β
(2[,)+β)(π§ β€ π₯ β (((ββif((1
β π¦) β€ (1 / 2), (1
/ 2), (1 β π¦)))β2) Β·
((Οβπ₯)
Β· (logβπ₯)))
< (ΞΈβπ₯))
β βπ₯ β
(2[,)+β)(π§ β€ π₯ β
(absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦))) |
93 | 92 | reximdv 3168 |
. . . . 5
β’ (π¦ β β+
β (βπ§ β
β βπ₯ β
(2[,)+β)(π§ β€ π₯ β (((ββif((1
β π¦) β€ (1 / 2), (1
/ 2), (1 β π¦)))β2) Β·
((Οβπ₯)
Β· (logβπ₯)))
< (ΞΈβπ₯))
β βπ§ β
β βπ₯ β
(2[,)+β)(π§ β€ π₯ β
(absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦))) |
94 | 32, 93 | mpd 15 |
. . . 4
β’ (π¦ β β+
β βπ§ β
β βπ₯ β
(2[,)+β)(π§ β€ π₯ β
(absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦)) |
95 | 94 | rgen 3067 |
. . 3
β’
βπ¦ β
β+ βπ§ β β βπ₯ β (2[,)+β)(π§ β€ π₯ β (absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦) |
96 | 54 | recnd 11190 |
. . . . . 6
β’ (π₯ β (2[,)+β) β
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯)))
β β) |
97 | 96 | adantl 483 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β β) |
98 | 97 | ralrimiva 3144 |
. . . 4
β’ (β€
β βπ₯ β
(2[,)+β)((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β β) |
99 | 40 | ssriv 3953 |
. . . . 5
β’
(2[,)+β) β β |
100 | 99 | a1i 11 |
. . . 4
β’ (β€
β (2[,)+β) β β) |
101 | | 1cnd 11157 |
. . . 4
β’ (β€
β 1 β β) |
102 | 98, 100, 101 | rlim2 15385 |
. . 3
β’ (β€
β ((π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) βπ 1 β
βπ¦ β
β+ βπ§ β β βπ₯ β (2[,)+β)(π§ β€ π₯ β (absβ(((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 1)) < π¦))) |
103 | 95, 102 | mpbiri 258 |
. 2
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) βπ
1) |
104 | 103 | mptru 1549 |
1
β’ (π₯ β (2[,)+β) β¦
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))
βπ 1 |