Step | Hyp | Ref
| Expression |
1 | | 1xr 11269 |
. . . . . 6
β’ 1 β
β* |
2 | | 1lt2 12379 |
. . . . . 6
β’ 1 <
2 |
3 | | df-ioo 13324 |
. . . . . . 7
β’ (,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) |
4 | | df-ico 13326 |
. . . . . . 7
β’ [,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ < π¦)}) |
5 | | xrltletr 13132 |
. . . . . . 7
β’ ((1
β β* β§ 2 β β* β§ π€ β β*)
β ((1 < 2 β§ 2 β€ π€) β 1 < π€)) |
6 | 3, 4, 5 | ixxss1 13338 |
. . . . . 6
β’ ((1
β β* β§ 1 < 2) β (2[,)+β) β
(1(,)+β)) |
7 | 1, 2, 6 | mp2an 691 |
. . . . 5
β’
(2[,)+β) β (1(,)+β) |
8 | | resmpt 6035 |
. . . . 5
β’
((2[,)+β) β (1(,)+β) β ((π₯ β (1(,)+β) β¦
((Οβπ₯) /
(π₯ / (logβπ₯)))) βΎ (2[,)+β)) =
(π₯ β (2[,)+β)
β¦ ((Οβπ₯) / (π₯ / (logβπ₯))))) |
9 | 7, 8 | mp1i 13 |
. . . 4
β’ (β€
β ((π₯ β
(1(,)+β) β¦ ((Οβπ₯) / (π₯ / (logβπ₯)))) βΎ (2[,)+β)) = (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(π₯ / (logβπ₯))))) |
10 | 7 | sseli 3977 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
π₯ β
(1(,)+β)) |
11 | | ioossre 13381 |
. . . . . . . . . . 11
β’
(1(,)+β) β β |
12 | 11 | sseli 3977 |
. . . . . . . . . 10
β’ (π₯ β (1(,)+β) β
π₯ β
β) |
13 | 10, 12 | syl 17 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
π₯ β
β) |
14 | | 2re 12282 |
. . . . . . . . . . 11
β’ 2 β
β |
15 | | pnfxr 11264 |
. . . . . . . . . . 11
β’ +β
β β* |
16 | | elico2 13384 |
. . . . . . . . . . 11
β’ ((2
β β β§ +β β β*) β (π₯ β (2[,)+β) β
(π₯ β β β§ 2
β€ π₯ β§ π₯ <
+β))) |
17 | 14, 15, 16 | mp2an 691 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
(π₯ β β β§ 2
β€ π₯ β§ π₯ <
+β)) |
18 | 17 | simp2bi 1147 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β 2
β€ π₯) |
19 | | chtrpcl 26659 |
. . . . . . . . 9
β’ ((π₯ β β β§ 2 β€
π₯) β
(ΞΈβπ₯) β
β+) |
20 | 13, 18, 19 | syl2anc 585 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
(ΞΈβπ₯) β
β+) |
21 | | 0red 11213 |
. . . . . . . . . . 11
β’ (π₯ β (1(,)+β) β 0
β β) |
22 | | 1red 11211 |
. . . . . . . . . . 11
β’ (π₯ β (1(,)+β) β 1
β β) |
23 | | 0lt1 11732 |
. . . . . . . . . . . 12
β’ 0 <
1 |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
β’ (π₯ β (1(,)+β) β 0
< 1) |
25 | | eliooord 13379 |
. . . . . . . . . . . 12
β’ (π₯ β (1(,)+β) β (1
< π₯ β§ π₯ <
+β)) |
26 | 25 | simpld 496 |
. . . . . . . . . . 11
β’ (π₯ β (1(,)+β) β 1
< π₯) |
27 | 21, 22, 12, 24, 26 | lttrd 11371 |
. . . . . . . . . 10
β’ (π₯ β (1(,)+β) β 0
< π₯) |
28 | 12, 27 | elrpd 13009 |
. . . . . . . . 9
β’ (π₯ β (1(,)+β) β
π₯ β
β+) |
29 | 10, 28 | syl 17 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
π₯ β
β+) |
30 | 20, 29 | rpdivcld 13029 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β
((ΞΈβπ₯) / π₯) β
β+) |
31 | 30 | adantl 483 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / π₯) β
β+) |
32 | | ppinncl 26658 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ 2 β€
π₯) β
(Οβπ₯)
β β) |
33 | 13, 18, 32 | syl2anc 585 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
(Οβπ₯)
β β) |
34 | 33 | nnrpd 13010 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
(Οβπ₯)
β β+) |
35 | 12, 26 | rplogcld 26119 |
. . . . . . . . . 10
β’ (π₯ β (1(,)+β) β
(logβπ₯) β
β+) |
36 | 10, 35 | syl 17 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
(logβπ₯) β
β+) |
37 | 34, 36 | rpmulcld 13028 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
((Οβπ₯)
Β· (logβπ₯))
β β+) |
38 | 20, 37 | rpdivcld 13029 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯)))
β β+) |
39 | 38 | adantl 483 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β
β+) |
40 | 29 | ssriv 3985 |
. . . . . . . 8
β’
(2[,)+β) β β+ |
41 | | resmpt 6035 |
. . . . . . . 8
β’
((2[,)+β) β β+ β ((π₯ β β+ β¦
((ΞΈβπ₯) / π₯)) βΎ (2[,)+β)) =
(π₯ β (2[,)+β)
β¦ ((ΞΈβπ₯)
/ π₯))) |
42 | 40, 41 | ax-mp 5 |
. . . . . . 7
β’ ((π₯ β β+
β¦ ((ΞΈβπ₯)
/ π₯)) βΎ
(2[,)+β)) = (π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) |
43 | | pnt2 27096 |
. . . . . . . 8
β’ (π₯ β β+
β¦ ((ΞΈβπ₯)
/ π₯))
βπ 1 |
44 | | rlimres 15498 |
. . . . . . . 8
β’ ((π₯ β β+
β¦ ((ΞΈβπ₯)
/ π₯))
βπ 1 β ((π₯ β β+ β¦
((ΞΈβπ₯) / π₯)) βΎ (2[,)+β))
βπ 1) |
45 | 43, 44 | mp1i 13 |
. . . . . . 7
β’ (β€
β ((π₯ β
β+ β¦ ((ΞΈβπ₯) / π₯)) βΎ (2[,)+β))
βπ 1) |
46 | 42, 45 | eqbrtrrid 5183 |
. . . . . 6
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / π₯)) βπ
1) |
47 | | chtppilim 26958 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β¦
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯))))
βπ 1 |
48 | 47 | a1i 11 |
. . . . . 6
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) βπ
1) |
49 | | ax-1ne0 11175 |
. . . . . . 7
β’ 1 β
0 |
50 | 49 | a1i 11 |
. . . . . 6
β’ (β€
β 1 β 0) |
51 | 38 | rpne0d 13017 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β
((ΞΈβπ₯) /
((Οβπ₯)
Β· (logβπ₯)))
β 0) |
52 | 51 | adantl 483 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))) β 0) |
53 | 31, 39, 46, 48, 50, 52 | rlimdiv 15588 |
. . . . 5
β’ (β€
β (π₯ β
(2[,)+β) β¦ (((ΞΈβπ₯) / π₯) / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) βπ (1 /
1)) |
54 | 13 | recnd 11238 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
π₯ β
β) |
55 | | chtcl 26593 |
. . . . . . . . . . . . 13
β’ (π₯ β β β
(ΞΈβπ₯) β
β) |
56 | 12, 55 | syl 17 |
. . . . . . . . . . . 12
β’ (π₯ β (1(,)+β) β
(ΞΈβπ₯) β
β) |
57 | 56 | recnd 11238 |
. . . . . . . . . . 11
β’ (π₯ β (1(,)+β) β
(ΞΈβπ₯) β
β) |
58 | 10, 57 | syl 17 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
(ΞΈβπ₯) β
β) |
59 | 54, 58 | mulcomd 11231 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
(π₯ Β·
(ΞΈβπ₯)) =
((ΞΈβπ₯) Β·
π₯)) |
60 | 59 | oveq2d 7420 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
(((ΞΈβπ₯)
Β· ((Οβπ₯) Β· (logβπ₯))) / (π₯ Β· (ΞΈβπ₯))) = (((ΞΈβπ₯) Β· ((Οβπ₯) Β· (logβπ₯))) / ((ΞΈβπ₯) Β· π₯))) |
61 | 37 | rpcnd 13014 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
((Οβπ₯)
Β· (logβπ₯))
β β) |
62 | 29 | rpne0d 13017 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
π₯ β 0) |
63 | 20 | rpne0d 13017 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
(ΞΈβπ₯) β
0) |
64 | 61, 54, 58, 62, 63 | divcan5d 12012 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
(((ΞΈβπ₯)
Β· ((Οβπ₯) Β· (logβπ₯))) / ((ΞΈβπ₯) Β· π₯)) = (((Οβπ₯) Β· (logβπ₯)) / π₯)) |
65 | 60, 64 | eqtrd 2773 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β
(((ΞΈβπ₯)
Β· ((Οβπ₯) Β· (logβπ₯))) / (π₯ Β· (ΞΈβπ₯))) = (((Οβπ₯) Β· (logβπ₯)) / π₯)) |
66 | 37 | rpne0d 13017 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
((Οβπ₯)
Β· (logβπ₯))
β 0) |
67 | 58, 54, 58, 61, 62, 66, 63 | divdivdivd 12033 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β
(((ΞΈβπ₯) / π₯) / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) = (((ΞΈβπ₯) Β·
((Οβπ₯)
Β· (logβπ₯))) /
(π₯ Β·
(ΞΈβπ₯)))) |
68 | 33 | nncnd 12224 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
(Οβπ₯)
β β) |
69 | 36 | rpcnd 13014 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
(logβπ₯) β
β) |
70 | 36 | rpne0d 13017 |
. . . . . . . 8
β’ (π₯ β (2[,)+β) β
(logβπ₯) β
0) |
71 | 68, 54, 69, 62, 70 | divdiv2d 12018 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β
((Οβπ₯) /
(π₯ / (logβπ₯))) = (((Οβπ₯) Β· (logβπ₯)) / π₯)) |
72 | 65, 67, 71 | 3eqtr4d 2783 |
. . . . . 6
β’ (π₯ β (2[,)+β) β
(((ΞΈβπ₯) / π₯) / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯)))) = ((Οβπ₯) / (π₯ / (logβπ₯)))) |
73 | 72 | mpteq2ia 5250 |
. . . . 5
β’ (π₯ β (2[,)+β) β¦
(((ΞΈβπ₯) / π₯) / ((ΞΈβπ₯) / ((Οβπ₯) Β· (logβπ₯))))) = (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(π₯ / (logβπ₯)))) |
74 | | 1div1e1 11900 |
. . . . 5
β’ (1 / 1) =
1 |
75 | 53, 73, 74 | 3brtr3g 5180 |
. . . 4
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((Οβπ₯) / (π₯ / (logβπ₯)))) βπ
1) |
76 | 9, 75 | eqbrtrd 5169 |
. . 3
β’ (β€
β ((π₯ β
(1(,)+β) β¦ ((Οβπ₯) / (π₯ / (logβπ₯)))) βΎ (2[,)+β))
βπ 1) |
77 | | ppicl 26615 |
. . . . . . . . . 10
β’ (π₯ β β β
(Οβπ₯)
β β0) |
78 | 12, 77 | syl 17 |
. . . . . . . . 9
β’ (π₯ β (1(,)+β) β
(Οβπ₯)
β β0) |
79 | 78 | nn0red 12529 |
. . . . . . . 8
β’ (π₯ β (1(,)+β) β
(Οβπ₯)
β β) |
80 | 28, 35 | rpdivcld 13029 |
. . . . . . . 8
β’ (π₯ β (1(,)+β) β
(π₯ / (logβπ₯)) β
β+) |
81 | 79, 80 | rerpdivcld 13043 |
. . . . . . 7
β’ (π₯ β (1(,)+β) β
((Οβπ₯) /
(π₯ / (logβπ₯))) β
β) |
82 | 81 | recnd 11238 |
. . . . . 6
β’ (π₯ β (1(,)+β) β
((Οβπ₯) /
(π₯ / (logβπ₯))) β
β) |
83 | 82 | adantl 483 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β ((Οβπ₯) / (π₯ / (logβπ₯))) β β) |
84 | 83 | fmpttd 7110 |
. . . 4
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((Οβπ₯) / (π₯ / (logβπ₯)))):(1(,)+β)βΆβ) |
85 | 11 | a1i 11 |
. . . 4
β’ (β€
β (1(,)+β) β β) |
86 | 14 | a1i 11 |
. . . 4
β’ (β€
β 2 β β) |
87 | 84, 85, 86 | rlimresb 15505 |
. . 3
β’ (β€
β ((π₯ β
(1(,)+β) β¦ ((Οβπ₯) / (π₯ / (logβπ₯)))) βπ 1 β
((π₯ β (1(,)+β)
β¦ ((Οβπ₯) / (π₯ / (logβπ₯)))) βΎ (2[,)+β))
βπ 1)) |
88 | 76, 87 | mpbird 257 |
. 2
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((Οβπ₯) / (π₯ / (logβπ₯)))) βπ
1) |
89 | 88 | mptru 1549 |
1
β’ (π₯ β (1(,)+β) β¦
((Οβπ₯) /
(π₯ / (logβπ₯)))) βπ
1 |