Step | Hyp | Ref
| Expression |
1 | | 1red 11163 |
. . 3
β’ (β€
β 1 β β) |
2 | | 1red 11163 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β 1 β β) |
3 | | 2re 12234 |
. . . . . . . . . . 11
β’ 2 β
β |
4 | | elicopnf 13369 |
. . . . . . . . . . 11
β’ (2 β
β β (π₯ β
(2[,)+β) β (π₯
β β β§ 2 β€ π₯))) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
(π₯ β β β§ 2
β€ π₯)) |
6 | 5 | simplbi 499 |
. . . . . . . . 9
β’ (π₯ β (2[,)+β) β
π₯ β
β) |
7 | 6 | adantl 483 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β π₯ β β) |
8 | | 0red 11165 |
. . . . . . . . . . . 12
β’ (π₯ β (2[,)+β) β 0
β β) |
9 | 3 | a1i 11 |
. . . . . . . . . . . 12
β’ (π₯ β (2[,)+β) β 2
β β) |
10 | | 2pos 12263 |
. . . . . . . . . . . . 13
β’ 0 <
2 |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
β’ (π₯ β (2[,)+β) β 0
< 2) |
12 | 5 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π₯ β (2[,)+β) β 2
β€ π₯) |
13 | 8, 9, 6, 11, 12 | ltletrd 11322 |
. . . . . . . . . . 11
β’ (π₯ β (2[,)+β) β 0
< π₯) |
14 | 6, 13 | elrpd 12961 |
. . . . . . . . . 10
β’ (π₯ β (2[,)+β) β
π₯ β
β+) |
15 | 14 | adantl 483 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (2[,)+β)) β π₯ β β+) |
16 | 15 | rpge0d 12968 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β 0 β€ π₯) |
17 | 7, 16 | resqrtcld 15309 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β (ββπ₯) β β) |
18 | 15 | relogcld 25994 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β (logβπ₯) β β) |
19 | 17, 18 | remulcld 11192 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((ββπ₯) Β· (logβπ₯)) β β) |
20 | 12 | adantl 483 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β 2 β€ π₯) |
21 | | chtrpcl 26540 |
. . . . . . 7
β’ ((π₯ β β β§ 2 β€
π₯) β
(ΞΈβπ₯) β
β+) |
22 | 7, 20, 21 | syl2anc 585 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β (ΞΈβπ₯) β
β+) |
23 | 19, 22 | rerpdivcld 12995 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)) β β) |
24 | 6 | ssriv 3953 |
. . . . . 6
β’
(2[,)+β) β β |
25 | 1 | recnd 11190 |
. . . . . 6
β’ (β€
β 1 β β) |
26 | | rlimconst 15433 |
. . . . . 6
β’
(((2[,)+β) β β β§ 1 β β) β (π₯ β (2[,)+β) β¦
1) βπ 1) |
27 | 24, 25, 26 | sylancr 588 |
. . . . 5
β’ (β€
β (π₯ β
(2[,)+β) β¦ 1) βπ 1) |
28 | | ovexd 7397 |
. . . . . . . 8
β’ (β€
β (2[,)+β) β V) |
29 | 7, 22 | rerpdivcld 12995 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β (π₯ / (ΞΈβπ₯)) β β) |
30 | | ovexd 7397 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β (((ββπ₯) Β· (logβπ₯)) / π₯) β V) |
31 | | eqidd 2738 |
. . . . . . . 8
β’ (β€
β (π₯ β
(2[,)+β) β¦ (π₯ /
(ΞΈβπ₯))) =
(π₯ β (2[,)+β)
β¦ (π₯ /
(ΞΈβπ₯)))) |
32 | 7 | recnd 11190 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (2[,)+β)) β π₯ β β) |
33 | | cxpsqrt 26074 |
. . . . . . . . . . . 12
β’ (π₯ β β β (π₯βπ(1 /
2)) = (ββπ₯)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (2[,)+β)) β (π₯βπ(1 / 2)) =
(ββπ₯)) |
35 | 34 | oveq2d 7378 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (2[,)+β)) β ((logβπ₯) / (π₯βπ(1 / 2))) =
((logβπ₯) /
(ββπ₯))) |
36 | 18 | recnd 11190 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (2[,)+β)) β (logβπ₯) β β) |
37 | 15 | rpsqrtcld 15303 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (2[,)+β)) β (ββπ₯) β
β+) |
38 | 37 | rpcnne0d 12973 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (2[,)+β)) β ((ββπ₯) β β β§ (ββπ₯) β 0)) |
39 | | divcan5 11864 |
. . . . . . . . . . 11
β’
(((logβπ₯)
β β β§ ((ββπ₯) β β β§ (ββπ₯) β 0) β§
((ββπ₯) β
β β§ (ββπ₯) β 0)) β (((ββπ₯) Β· (logβπ₯)) / ((ββπ₯) Β· (ββπ₯))) = ((logβπ₯) / (ββπ₯))) |
40 | 36, 38, 38, 39 | syl3anc 1372 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (2[,)+β)) β (((ββπ₯) Β· (logβπ₯)) / ((ββπ₯) Β· (ββπ₯))) = ((logβπ₯) / (ββπ₯))) |
41 | | remsqsqrt 15148 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ 0 β€
π₯) β
((ββπ₯) Β·
(ββπ₯)) = π₯) |
42 | 7, 16, 41 | syl2anc 585 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (2[,)+β)) β ((ββπ₯) Β· (ββπ₯)) = π₯) |
43 | 42 | oveq2d 7378 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (2[,)+β)) β (((ββπ₯) Β· (logβπ₯)) / ((ββπ₯) Β· (ββπ₯))) = (((ββπ₯) Β· (logβπ₯)) / π₯)) |
44 | 35, 40, 43 | 3eqtr2d 2783 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (2[,)+β)) β ((logβπ₯) / (π₯βπ(1 / 2))) =
(((ββπ₯)
Β· (logβπ₯)) /
π₯)) |
45 | 44 | mpteq2dva 5210 |
. . . . . . . 8
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((logβπ₯) / (π₯βπ(1 / 2)))) = (π₯ β (2[,)+β) β¦
(((ββπ₯)
Β· (logβπ₯)) /
π₯))) |
46 | 28, 29, 30, 31, 45 | offval2 7642 |
. . . . . . 7
β’ (β€
β ((π₯ β
(2[,)+β) β¦ (π₯ /
(ΞΈβπ₯)))
βf Β· (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1 /
2))))) = (π₯ β
(2[,)+β) β¦ ((π₯
/ (ΞΈβπ₯))
Β· (((ββπ₯) Β· (logβπ₯)) / π₯)))) |
47 | 15 | rpne0d 12969 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (2[,)+β)) β π₯ β 0) |
48 | 22 | rpcnne0d 12973 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) β β β§ (ΞΈβπ₯) β 0)) |
49 | 19 | recnd 11190 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (2[,)+β)) β ((ββπ₯) Β· (logβπ₯)) β β) |
50 | | dmdcan 11872 |
. . . . . . . . 9
β’ (((π₯ β β β§ π₯ β 0) β§
((ΞΈβπ₯) β
β β§ (ΞΈβπ₯) β 0) β§ ((ββπ₯) Β· (logβπ₯)) β β) β
((π₯ / (ΞΈβπ₯)) Β·
(((ββπ₯)
Β· (logβπ₯)) /
π₯)) =
(((ββπ₯)
Β· (logβπ₯)) /
(ΞΈβπ₯))) |
51 | 32, 47, 48, 49, 50 | syl211anc 1377 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β ((π₯ / (ΞΈβπ₯)) Β· (((ββπ₯) Β· (logβπ₯)) / π₯)) = (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯))) |
52 | 51 | mpteq2dva 5210 |
. . . . . . 7
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((π₯
/ (ΞΈβπ₯))
Β· (((ββπ₯) Β· (logβπ₯)) / π₯))) = (π₯ β (2[,)+β) β¦
(((ββπ₯)
Β· (logβπ₯)) /
(ΞΈβπ₯)))) |
53 | 46, 52 | eqtrd 2777 |
. . . . . 6
β’ (β€
β ((π₯ β
(2[,)+β) β¦ (π₯ /
(ΞΈβπ₯)))
βf Β· (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1 /
2))))) = (π₯ β
(2[,)+β) β¦ (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)))) |
54 | | chto1lb 26842 |
. . . . . . 7
β’ (π₯ β (2[,)+β) β¦
(π₯ / (ΞΈβπ₯))) β
π(1) |
55 | 14 | ssriv 3953 |
. . . . . . . . 9
β’
(2[,)+β) β β+ |
56 | 55 | a1i 11 |
. . . . . . . 8
β’ (β€
β (2[,)+β) β β+) |
57 | | 1rp 12926 |
. . . . . . . . . . 11
β’ 1 β
β+ |
58 | | rphalfcl 12949 |
. . . . . . . . . . 11
β’ (1 β
β+ β (1 / 2) β β+) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . 10
β’ (1 / 2)
β β+ |
60 | | cxploglim 26343 |
. . . . . . . . . 10
β’ ((1 / 2)
β β+ β (π₯ β β+ β¦
((logβπ₯) / (π₯βπ(1 /
2)))) βπ 0) |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . 9
β’ (π₯ β β+
β¦ ((logβπ₯) /
(π₯βπ(1 / 2))))
βπ 0 |
62 | 61 | a1i 11 |
. . . . . . . 8
β’ (β€
β (π₯ β
β+ β¦ ((logβπ₯) / (π₯βπ(1 / 2))))
βπ 0) |
63 | 56, 62 | rlimres2 15450 |
. . . . . . 7
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((logβπ₯) / (π₯βπ(1 / 2))))
βπ 0) |
64 | | o1rlimmul 15508 |
. . . . . . 7
β’ (((π₯ β (2[,)+β) β¦
(π₯ / (ΞΈβπ₯))) β π(1) β§
(π₯ β (2[,)+β)
β¦ ((logβπ₯) /
(π₯βπ(1 / 2))))
βπ 0) β ((π₯ β (2[,)+β) β¦ (π₯ / (ΞΈβπ₯))) βf Β·
(π₯ β (2[,)+β)
β¦ ((logβπ₯) /
(π₯βπ(1 / 2)))))
βπ 0) |
65 | 54, 63, 64 | sylancr 588 |
. . . . . 6
β’ (β€
β ((π₯ β
(2[,)+β) β¦ (π₯ /
(ΞΈβπ₯)))
βf Β· (π₯ β (2[,)+β) β¦
((logβπ₯) / (π₯βπ(1 /
2))))) βπ 0) |
66 | 53, 65 | eqbrtrrd 5134 |
. . . . 5
β’ (β€
β (π₯ β
(2[,)+β) β¦ (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯))) βπ
0) |
67 | 2, 23, 27, 66 | rlimadd 15532 |
. . . 4
β’ (β€
β (π₯ β
(2[,)+β) β¦ (1 + (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)))) βπ (1 +
0)) |
68 | | 1p0e1 12284 |
. . . 4
β’ (1 + 0) =
1 |
69 | 67, 68 | breqtrdi 5151 |
. . 3
β’ (β€
β (π₯ β
(2[,)+β) β¦ (1 + (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)))) βπ
1) |
70 | | 1re 11162 |
. . . 4
β’ 1 β
β |
71 | | readdcl 11141 |
. . . 4
β’ ((1
β β β§ (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)) β β) β (1 +
(((ββπ₯)
Β· (logβπ₯)) /
(ΞΈβπ₯))) β
β) |
72 | 70, 23, 71 | sylancr 588 |
. . 3
β’
((β€ β§ π₯
β (2[,)+β)) β (1 + (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯))) β β) |
73 | | chpcl 26489 |
. . . . 5
β’ (π₯ β β β
(Οβπ₯) β
β) |
74 | 7, 73 | syl 17 |
. . . 4
β’
((β€ β§ π₯
β (2[,)+β)) β (Οβπ₯) β β) |
75 | 74, 22 | rerpdivcld 12995 |
. . 3
β’
((β€ β§ π₯
β (2[,)+β)) β ((Οβπ₯) / (ΞΈβπ₯)) β β) |
76 | | chtcl 26474 |
. . . . . . . 8
β’ (π₯ β β β
(ΞΈβπ₯) β
β) |
77 | 7, 76 | syl 17 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β (ΞΈβπ₯) β β) |
78 | 77, 19 | readdcld 11191 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) + ((ββπ₯) Β· (logβπ₯))) β β) |
79 | 3 | a1i 11 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β 2 β β) |
80 | | 1le2 12369 |
. . . . . . . . 9
β’ 1 β€
2 |
81 | 80 | a1i 11 |
. . . . . . . 8
β’
((β€ β§ π₯
β (2[,)+β)) β 1 β€ 2) |
82 | 2, 79, 7, 81, 20 | letrd 11319 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β 1 β€ π₯) |
83 | | chpub 26584 |
. . . . . . 7
β’ ((π₯ β β β§ 1 β€
π₯) β
(Οβπ₯) β€
((ΞΈβπ₯) +
((ββπ₯) Β·
(logβπ₯)))) |
84 | 7, 82, 83 | syl2anc 585 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β (Οβπ₯) β€ ((ΞΈβπ₯) + ((ββπ₯) Β· (logβπ₯)))) |
85 | 74, 78, 22, 84 | lediv1dd 13022 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β ((Οβπ₯) / (ΞΈβπ₯)) β€ (((ΞΈβπ₯) + ((ββπ₯) Β· (logβπ₯))) / (ΞΈβπ₯))) |
86 | 22 | rpcnd 12966 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β (ΞΈβπ₯) β β) |
87 | | divdir 11845 |
. . . . . . 7
β’
(((ΞΈβπ₯)
β β β§ ((ββπ₯) Β· (logβπ₯)) β β β§ ((ΞΈβπ₯) β β β§
(ΞΈβπ₯) β 0))
β (((ΞΈβπ₯)
+ ((ββπ₯)
Β· (logβπ₯))) /
(ΞΈβπ₯)) =
(((ΞΈβπ₯) /
(ΞΈβπ₯)) +
(((ββπ₯)
Β· (logβπ₯)) /
(ΞΈβπ₯)))) |
88 | 86, 49, 48, 87 | syl3anc 1372 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β (((ΞΈβπ₯) + ((ββπ₯) Β· (logβπ₯))) / (ΞΈβπ₯)) = (((ΞΈβπ₯) / (ΞΈβπ₯)) + (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)))) |
89 | | divid 11849 |
. . . . . . . 8
β’
(((ΞΈβπ₯)
β β β§ (ΞΈβπ₯) β 0) β ((ΞΈβπ₯) / (ΞΈβπ₯)) = 1) |
90 | 48, 89 | syl 17 |
. . . . . . 7
β’
((β€ β§ π₯
β (2[,)+β)) β ((ΞΈβπ₯) / (ΞΈβπ₯)) = 1) |
91 | 90 | oveq1d 7377 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β (((ΞΈβπ₯) / (ΞΈβπ₯)) + (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯))) = (1 + (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)))) |
92 | 88, 91 | eqtrd 2777 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β (((ΞΈβπ₯) + ((ββπ₯) Β· (logβπ₯))) / (ΞΈβπ₯)) = (1 + (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)))) |
93 | 85, 92 | breqtrd 5136 |
. . . 4
β’
((β€ β§ π₯
β (2[,)+β)) β ((Οβπ₯) / (ΞΈβπ₯)) β€ (1 + (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)))) |
94 | 93 | adantrr 716 |
. . 3
β’
((β€ β§ (π₯
β (2[,)+β) β§ 1 β€ π₯)) β ((Οβπ₯) / (ΞΈβπ₯)) β€ (1 + (((ββπ₯) Β· (logβπ₯)) / (ΞΈβπ₯)))) |
95 | 86 | mulid2d 11180 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β (1 Β· (ΞΈβπ₯)) = (ΞΈβπ₯)) |
96 | | chtlepsi 26570 |
. . . . . . 7
β’ (π₯ β β β
(ΞΈβπ₯) β€
(Οβπ₯)) |
97 | 7, 96 | syl 17 |
. . . . . 6
β’
((β€ β§ π₯
β (2[,)+β)) β (ΞΈβπ₯) β€ (Οβπ₯)) |
98 | 95, 97 | eqbrtrd 5132 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β (1 Β· (ΞΈβπ₯)) β€ (Οβπ₯)) |
99 | 2, 74, 22 | lemuldivd 13013 |
. . . . 5
β’
((β€ β§ π₯
β (2[,)+β)) β ((1 Β· (ΞΈβπ₯)) β€ (Οβπ₯) β 1 β€ ((Οβπ₯) / (ΞΈβπ₯)))) |
100 | 98, 99 | mpbid 231 |
. . . 4
β’
((β€ β§ π₯
β (2[,)+β)) β 1 β€ ((Οβπ₯) / (ΞΈβπ₯))) |
101 | 100 | adantrr 716 |
. . 3
β’
((β€ β§ (π₯
β (2[,)+β) β§ 1 β€ π₯)) β 1 β€ ((Οβπ₯) / (ΞΈβπ₯))) |
102 | 1, 1, 69, 72, 75, 94, 101 | rlimsqz2 15542 |
. 2
β’ (β€
β (π₯ β
(2[,)+β) β¦ ((Οβπ₯) / (ΞΈβπ₯))) βπ
1) |
103 | 102 | mptru 1549 |
1
β’ (π₯ β (2[,)+β) β¦
((Οβπ₯) /
(ΞΈβπ₯)))
βπ 1 |