Step | Hyp | Ref
| Expression |
1 | | rpssre 12929 |
. . . 4
β’
β+ β β |
2 | 1 | a1i 11 |
. . 3
β’ (β€
β β+ β β) |
3 | | rpre 12930 |
. . . . . . 7
β’ (π₯ β β+
β π₯ β
β) |
4 | | chtcl 26474 |
. . . . . . 7
β’ (π₯ β β β
(ΞΈβπ₯) β
β) |
5 | 3, 4 | syl 17 |
. . . . . 6
β’ (π₯ β β+
β (ΞΈβπ₯)
β β) |
6 | | rerpdivcl 12952 |
. . . . . 6
β’
(((ΞΈβπ₯)
β β β§ π₯
β β+) β ((ΞΈβπ₯) / π₯) β β) |
7 | 5, 6 | mpancom 687 |
. . . . 5
β’ (π₯ β β+
β ((ΞΈβπ₯) /
π₯) β
β) |
8 | 7 | recnd 11190 |
. . . 4
β’ (π₯ β β+
β ((ΞΈβπ₯) /
π₯) β
β) |
9 | 8 | adantl 483 |
. . 3
β’
((β€ β§ π₯
β β+) β ((ΞΈβπ₯) / π₯) β β) |
10 | | 3re 12240 |
. . . 4
β’ 3 β
β |
11 | 10 | a1i 11 |
. . 3
β’ (β€
β 3 β β) |
12 | | 2rp 12927 |
. . . . . 6
β’ 2 β
β+ |
13 | | relogcl 25947 |
. . . . . 6
β’ (2 β
β+ β (logβ2) β β) |
14 | 12, 13 | ax-mp 5 |
. . . . 5
β’
(logβ2) β β |
15 | | 2re 12234 |
. . . . 5
β’ 2 β
β |
16 | 14, 15 | remulcli 11178 |
. . . 4
β’
((logβ2) Β· 2) β β |
17 | 16 | a1i 11 |
. . 3
β’ (β€
β ((logβ2) Β· 2) β β) |
18 | | chtge0 26477 |
. . . . . . . . 9
β’ (π₯ β β β 0 β€
(ΞΈβπ₯)) |
19 | 3, 18 | syl 17 |
. . . . . . . 8
β’ (π₯ β β+
β 0 β€ (ΞΈβπ₯)) |
20 | | rpregt0 12936 |
. . . . . . . 8
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
21 | | divge0 12031 |
. . . . . . . 8
β’
((((ΞΈβπ₯)
β β β§ 0 β€ (ΞΈβπ₯)) β§ (π₯ β β β§ 0 < π₯)) β 0 β€
((ΞΈβπ₯) / π₯)) |
22 | 5, 19, 20, 21 | syl21anc 837 |
. . . . . . 7
β’ (π₯ β β+
β 0 β€ ((ΞΈβπ₯) / π₯)) |
23 | 7, 22 | absidd 15314 |
. . . . . 6
β’ (π₯ β β+
β (absβ((ΞΈβπ₯) / π₯)) = ((ΞΈβπ₯) / π₯)) |
24 | 23 | adantr 482 |
. . . . 5
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(absβ((ΞΈβπ₯) / π₯)) = ((ΞΈβπ₯) / π₯)) |
25 | 7 | adantr 482 |
. . . . . 6
β’ ((π₯ β β+
β§ 3 β€ π₯) β
((ΞΈβπ₯) / π₯) β
β) |
26 | 16 | a1i 11 |
. . . . . 6
β’ ((π₯ β β+
β§ 3 β€ π₯) β
((logβ2) Β· 2) β β) |
27 | 5 | adantr 482 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(ΞΈβπ₯) β
β) |
28 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ 3 β€ π₯) β
π₯ β
β) |
29 | | remulcl 11143 |
. . . . . . . . . . . 12
β’ ((2
β β β§ π₯
β β) β (2 Β· π₯) β β) |
30 | 15, 28, 29 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 3 β€ π₯) β (2
Β· π₯) β
β) |
31 | | resubcl 11472 |
. . . . . . . . . . 11
β’ (((2
Β· π₯) β β
β§ 3 β β) β ((2 Β· π₯) β 3) β β) |
32 | 30, 10, 31 | sylancl 587 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 3 β€ π₯) β ((2
Β· π₯) β 3)
β β) |
33 | | remulcl 11143 |
. . . . . . . . . 10
β’
(((logβ2) β β β§ ((2 Β· π₯) β 3) β β) β
((logβ2) Β· ((2 Β· π₯) β 3)) β
β) |
34 | 14, 32, 33 | sylancr 588 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 3 β€ π₯) β
((logβ2) Β· ((2 Β· π₯) β 3)) β
β) |
35 | | remulcl 11143 |
. . . . . . . . . 10
β’
(((logβ2) β β β§ (2 Β· π₯) β β) β ((logβ2)
Β· (2 Β· π₯))
β β) |
36 | 14, 30, 35 | sylancr 588 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 3 β€ π₯) β
((logβ2) Β· (2 Β· π₯)) β β) |
37 | 15 | a1i 11 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 3 β€ π₯) β 2
β β) |
38 | 10 | a1i 11 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 3 β€ π₯) β 3
β β) |
39 | | 2lt3 12332 |
. . . . . . . . . . . 12
β’ 2 <
3 |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 3 β€ π₯) β 2
< 3) |
41 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 3 β€ π₯) β 3
β€ π₯) |
42 | 37, 38, 28, 40, 41 | ltletrd 11322 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 3 β€ π₯) β 2
< π₯) |
43 | | chtub 26576 |
. . . . . . . . . 10
β’ ((π₯ β β β§ 2 <
π₯) β
(ΞΈβπ₯) <
((logβ2) Β· ((2 Β· π₯) β 3))) |
44 | 28, 42, 43 | syl2anc 585 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(ΞΈβπ₯) <
((logβ2) Β· ((2 Β· π₯) β 3))) |
45 | | 3rp 12928 |
. . . . . . . . . . 11
β’ 3 β
β+ |
46 | | ltsubrp 12958 |
. . . . . . . . . . 11
β’ (((2
Β· π₯) β β
β§ 3 β β+) β ((2 Β· π₯) β 3) < (2 Β· π₯)) |
47 | 30, 45, 46 | sylancl 587 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 3 β€ π₯) β ((2
Β· π₯) β 3) <
(2 Β· π₯)) |
48 | | 1lt2 12331 |
. . . . . . . . . . . . . 14
β’ 1 <
2 |
49 | | rplogcl 25975 |
. . . . . . . . . . . . . 14
β’ ((2
β β β§ 1 < 2) β (logβ2) β
β+) |
50 | 15, 48, 49 | mp2an 691 |
. . . . . . . . . . . . 13
β’
(logβ2) β β+ |
51 | | elrp 12924 |
. . . . . . . . . . . . 13
β’
((logβ2) β β+ β ((logβ2) β
β β§ 0 < (logβ2))) |
52 | 50, 51 | mpbi 229 |
. . . . . . . . . . . 12
β’
((logβ2) β β β§ 0 <
(logβ2)) |
53 | 52 | a1i 11 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 3 β€ π₯) β
((logβ2) β β β§ 0 < (logβ2))) |
54 | | ltmul2 12013 |
. . . . . . . . . . 11
β’ ((((2
Β· π₯) β 3)
β β β§ (2 Β· π₯) β β β§ ((logβ2) β
β β§ 0 < (logβ2))) β (((2 Β· π₯) β 3) < (2 Β· π₯) β ((logβ2) Β·
((2 Β· π₯) β 3))
< ((logβ2) Β· (2 Β· π₯)))) |
55 | 32, 30, 53, 54 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 3 β€ π₯) β (((2
Β· π₯) β 3) <
(2 Β· π₯) β
((logβ2) Β· ((2 Β· π₯) β 3)) < ((logβ2) Β· (2
Β· π₯)))) |
56 | 47, 55 | mpbid 231 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 3 β€ π₯) β
((logβ2) Β· ((2 Β· π₯) β 3)) < ((logβ2) Β· (2
Β· π₯))) |
57 | 27, 34, 36, 44, 56 | lttrd 11323 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(ΞΈβπ₯) <
((logβ2) Β· (2 Β· π₯))) |
58 | 14 | recni 11176 |
. . . . . . . . . 10
β’
(logβ2) β β |
59 | 58 | a1i 11 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(logβ2) β β) |
60 | | 2cnd 12238 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 3 β€ π₯) β 2
β β) |
61 | 3 | recnd 11190 |
. . . . . . . . . 10
β’ (π₯ β β+
β π₯ β
β) |
62 | 61 | adantr 482 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 3 β€ π₯) β
π₯ β
β) |
63 | 59, 60, 62 | mulassd 11185 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(((logβ2) Β· 2) Β· π₯) = ((logβ2) Β· (2 Β· π₯))) |
64 | 57, 63 | breqtrrd 5138 |
. . . . . . 7
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(ΞΈβπ₯) <
(((logβ2) Β· 2) Β· π₯)) |
65 | 20 | adantr 482 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(π₯ β β β§ 0
< π₯)) |
66 | | ltdivmul2 12039 |
. . . . . . . 8
β’
(((ΞΈβπ₯)
β β β§ ((logβ2) Β· 2) β β β§ (π₯ β β β§ 0 <
π₯)) β
(((ΞΈβπ₯) / π₯) < ((logβ2) Β·
2) β (ΞΈβπ₯)
< (((logβ2) Β· 2) Β· π₯))) |
67 | 27, 26, 65, 66 | syl3anc 1372 |
. . . . . . 7
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(((ΞΈβπ₯) / π₯) < ((logβ2) Β·
2) β (ΞΈβπ₯)
< (((logβ2) Β· 2) Β· π₯))) |
68 | 64, 67 | mpbird 257 |
. . . . . 6
β’ ((π₯ β β+
β§ 3 β€ π₯) β
((ΞΈβπ₯) / π₯) < ((logβ2) Β·
2)) |
69 | 25, 26, 68 | ltled 11310 |
. . . . 5
β’ ((π₯ β β+
β§ 3 β€ π₯) β
((ΞΈβπ₯) / π₯) β€ ((logβ2) Β·
2)) |
70 | 24, 69 | eqbrtrd 5132 |
. . . 4
β’ ((π₯ β β+
β§ 3 β€ π₯) β
(absβ((ΞΈβπ₯) / π₯)) β€ ((logβ2) Β·
2)) |
71 | 70 | adantl 483 |
. . 3
β’
((β€ β§ (π₯
β β+ β§ 3 β€ π₯)) β (absβ((ΞΈβπ₯) / π₯)) β€ ((logβ2) Β·
2)) |
72 | 2, 9, 11, 17, 71 | elo1d 15425 |
. 2
β’ (β€
β (π₯ β
β+ β¦ ((ΞΈβπ₯) / π₯)) β π(1)) |
73 | 72 | mptru 1549 |
1
β’ (π₯ β β+
β¦ ((ΞΈβπ₯)
/ π₯)) β
π(1) |