Step | Hyp | Ref
| Expression |
1 | | 2re 12234 |
. . . . 5
โข 2 โ
โ |
2 | | pnfxr 11216 |
. . . . 5
โข +โ
โ โ* |
3 | | icossre 13352 |
. . . . 5
โข ((2
โ โ โง +โ โ โ*) โ (2[,)+โ)
โ โ) |
4 | 1, 2, 3 | mp2an 691 |
. . . 4
โข
(2[,)+โ) โ โ |
5 | 4 | a1i 11 |
. . 3
โข (โค
โ (2[,)+โ) โ โ) |
6 | | elicopnf 13369 |
. . . . . . . . . 10
โข (2 โ
โ โ (๐ฅ โ
(2[,)+โ) โ (๐ฅ
โ โ โง 2 โค ๐ฅ))) |
7 | 1, 6 | ax-mp 5 |
. . . . . . . . 9
โข (๐ฅ โ (2[,)+โ) โ
(๐ฅ โ โ โง 2
โค ๐ฅ)) |
8 | 7 | simplbi 499 |
. . . . . . . 8
โข (๐ฅ โ (2[,)+โ) โ
๐ฅ โ
โ) |
9 | | 0red 11165 |
. . . . . . . . 9
โข (๐ฅ โ (2[,)+โ) โ 0
โ โ) |
10 | | 1re 11162 |
. . . . . . . . . 10
โข 1 โ
โ |
11 | 10 | a1i 11 |
. . . . . . . . 9
โข (๐ฅ โ (2[,)+โ) โ 1
โ โ) |
12 | | 0lt1 11684 |
. . . . . . . . . 10
โข 0 <
1 |
13 | 12 | a1i 11 |
. . . . . . . . 9
โข (๐ฅ โ (2[,)+โ) โ 0
< 1) |
14 | 1 | a1i 11 |
. . . . . . . . . 10
โข (๐ฅ โ (2[,)+โ) โ 2
โ โ) |
15 | | 1lt2 12331 |
. . . . . . . . . . 11
โข 1 <
2 |
16 | 15 | a1i 11 |
. . . . . . . . . 10
โข (๐ฅ โ (2[,)+โ) โ 1
< 2) |
17 | 7 | simprbi 498 |
. . . . . . . . . 10
โข (๐ฅ โ (2[,)+โ) โ 2
โค ๐ฅ) |
18 | 11, 14, 8, 16, 17 | ltletrd 11322 |
. . . . . . . . 9
โข (๐ฅ โ (2[,)+โ) โ 1
< ๐ฅ) |
19 | 9, 11, 8, 13, 18 | lttrd 11323 |
. . . . . . . 8
โข (๐ฅ โ (2[,)+โ) โ 0
< ๐ฅ) |
20 | 8, 19 | elrpd 12961 |
. . . . . . 7
โข (๐ฅ โ (2[,)+โ) โ
๐ฅ โ
โ+) |
21 | 8, 18 | rplogcld 26000 |
. . . . . . 7
โข (๐ฅ โ (2[,)+โ) โ
(logโ๐ฅ) โ
โ+) |
22 | 20, 21 | rpdivcld 12981 |
. . . . . 6
โข (๐ฅ โ (2[,)+โ) โ
(๐ฅ / (logโ๐ฅ)) โ
โ+) |
23 | | ppinncl 26539 |
. . . . . . . 8
โข ((๐ฅ โ โ โง 2 โค
๐ฅ) โ
(ฯโ๐ฅ)
โ โ) |
24 | 7, 23 | sylbi 216 |
. . . . . . 7
โข (๐ฅ โ (2[,)+โ) โ
(ฯโ๐ฅ)
โ โ) |
25 | 24 | nnrpd 12962 |
. . . . . 6
โข (๐ฅ โ (2[,)+โ) โ
(ฯโ๐ฅ)
โ โ+) |
26 | 22, 25 | rpdivcld 12981 |
. . . . 5
โข (๐ฅ โ (2[,)+โ) โ
((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ
โ+) |
27 | 26 | rpcnd 12966 |
. . . 4
โข (๐ฅ โ (2[,)+โ) โ
((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ
โ) |
28 | 27 | adantl 483 |
. . 3
โข
((โค โง ๐ฅ
โ (2[,)+โ)) โ ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ) |
29 | | 8re 12256 |
. . . 4
โข 8 โ
โ |
30 | 29 | a1i 11 |
. . 3
โข (โค
โ 8 โ โ) |
31 | | 2rp 12927 |
. . . . . . . 8
โข 2 โ
โ+ |
32 | | relogcl 25947 |
. . . . . . . 8
โข (2 โ
โ+ โ (logโ2) โ โ) |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
โข
(logโ2) โ โ |
34 | | ere 15978 |
. . . . . . . . 9
โข e โ
โ |
35 | 1, 34 | remulcli 11178 |
. . . . . . . 8
โข (2
ยท e) โ โ |
36 | | 2pos 12263 |
. . . . . . . . . 10
โข 0 <
2 |
37 | | epos 16096 |
. . . . . . . . . 10
โข 0 <
e |
38 | 1, 34, 36, 37 | mulgt0ii 11295 |
. . . . . . . . 9
โข 0 < (2
ยท e) |
39 | 35, 38 | gt0ne0ii 11698 |
. . . . . . . 8
โข (2
ยท e) โ 0 |
40 | 35, 39 | rereccli 11927 |
. . . . . . 7
โข (1 / (2
ยท e)) โ โ |
41 | 33, 40 | resubcli 11470 |
. . . . . 6
โข
((logโ2) โ (1 / (2 ยท e))) โ
โ |
42 | | 2t1e2 12323 |
. . . . . . . . . 10
โข (2
ยท 1) = 2 |
43 | | egt2lt3 16095 |
. . . . . . . . . . . . 13
โข (2 < e
โง e < 3) |
44 | 43 | simpli 485 |
. . . . . . . . . . . 12
โข 2 <
e |
45 | 10, 1, 34 | lttri 11288 |
. . . . . . . . . . . 12
โข ((1 <
2 โง 2 < e) โ 1 < e) |
46 | 15, 44, 45 | mp2an 691 |
. . . . . . . . . . 11
โข 1 <
e |
47 | 10, 34, 1 | ltmul2i 12083 |
. . . . . . . . . . . 12
โข (0 < 2
โ (1 < e โ (2 ยท 1) < (2 ยท e))) |
48 | 36, 47 | ax-mp 5 |
. . . . . . . . . . 11
โข (1 < e
โ (2 ยท 1) < (2 ยท e)) |
49 | 46, 48 | mpbi 229 |
. . . . . . . . . 10
โข (2
ยท 1) < (2 ยท e) |
50 | 42, 49 | eqbrtrri 5133 |
. . . . . . . . 9
โข 2 < (2
ยท e) |
51 | 1, 35, 36, 38 | ltrecii 12078 |
. . . . . . . . 9
โข (2 <
(2 ยท e) โ (1 / (2 ยท e)) < (1 / 2)) |
52 | 50, 51 | mpbi 229 |
. . . . . . . 8
โข (1 / (2
ยท e)) < (1 / 2) |
53 | 43 | simpri 487 |
. . . . . . . . . . . 12
โข e <
3 |
54 | | 3lt4 12334 |
. . . . . . . . . . . 12
โข 3 <
4 |
55 | | 3re 12240 |
. . . . . . . . . . . . 13
โข 3 โ
โ |
56 | | 4re 12244 |
. . . . . . . . . . . . 13
โข 4 โ
โ |
57 | 34, 55, 56 | lttri 11288 |
. . . . . . . . . . . 12
โข ((e <
3 โง 3 < 4) โ e < 4) |
58 | 53, 54, 57 | mp2an 691 |
. . . . . . . . . . 11
โข e <
4 |
59 | | epr 16097 |
. . . . . . . . . . . 12
โข e โ
โ+ |
60 | | 4pos 12267 |
. . . . . . . . . . . . 13
โข 0 <
4 |
61 | 56, 60 | elrpii 12925 |
. . . . . . . . . . . 12
โข 4 โ
โ+ |
62 | | logltb 25971 |
. . . . . . . . . . . 12
โข ((e
โ โ+ โง 4 โ โ+) โ (e < 4
โ (logโe) < (logโ4))) |
63 | 59, 61, 62 | mp2an 691 |
. . . . . . . . . . 11
โข (e < 4
โ (logโe) < (logโ4)) |
64 | 58, 63 | mpbi 229 |
. . . . . . . . . 10
โข
(logโe) < (logโ4) |
65 | | loge 25958 |
. . . . . . . . . 10
โข
(logโe) = 1 |
66 | | sq2 14108 |
. . . . . . . . . . . 12
โข
(2โ2) = 4 |
67 | 66 | fveq2i 6850 |
. . . . . . . . . . 11
โข
(logโ(2โ2)) = (logโ4) |
68 | | 2z 12542 |
. . . . . . . . . . . 12
โข 2 โ
โค |
69 | | relogexp 25967 |
. . . . . . . . . . . 12
โข ((2
โ โ+ โง 2 โ โค) โ
(logโ(2โ2)) = (2 ยท (logโ2))) |
70 | 31, 68, 69 | mp2an 691 |
. . . . . . . . . . 11
โข
(logโ(2โ2)) = (2 ยท (logโ2)) |
71 | 67, 70 | eqtr3i 2767 |
. . . . . . . . . 10
โข
(logโ4) = (2 ยท (logโ2)) |
72 | 64, 65, 71 | 3brtr3i 5139 |
. . . . . . . . 9
โข 1 < (2
ยท (logโ2)) |
73 | 1, 36 | pm3.2i 472 |
. . . . . . . . . 10
โข (2 โ
โ โง 0 < 2) |
74 | | ltdivmul 12037 |
. . . . . . . . . 10
โข ((1
โ โ โง (logโ2) โ โ โง (2 โ โ โง
0 < 2)) โ ((1 / 2) < (logโ2) โ 1 < (2 ยท
(logโ2)))) |
75 | 10, 33, 73, 74 | mp3an 1462 |
. . . . . . . . 9
โข ((1 / 2)
< (logโ2) โ 1 < (2 ยท (logโ2))) |
76 | 72, 75 | mpbir 230 |
. . . . . . . 8
โข (1 / 2)
< (logโ2) |
77 | | halfre 12374 |
. . . . . . . . 9
โข (1 / 2)
โ โ |
78 | 40, 77, 33 | lttri 11288 |
. . . . . . . 8
โข (((1 / (2
ยท e)) < (1 / 2) โง (1 / 2) < (logโ2)) โ (1 / (2
ยท e)) < (logโ2)) |
79 | 52, 76, 78 | mp2an 691 |
. . . . . . 7
โข (1 / (2
ยท e)) < (logโ2) |
80 | 40, 33 | posdifi 11712 |
. . . . . . 7
โข ((1 / (2
ยท e)) < (logโ2) โ 0 < ((logโ2) โ (1 / (2
ยท e)))) |
81 | 79, 80 | mpbi 229 |
. . . . . 6
โข 0 <
((logโ2) โ (1 / (2 ยท e))) |
82 | 41, 81 | elrpii 12925 |
. . . . 5
โข
((logโ2) โ (1 / (2 ยท e))) โ
โ+ |
83 | | rerpdivcl 12952 |
. . . . 5
โข ((2
โ โ โง ((logโ2) โ (1 / (2 ยท e))) โ
โ+) โ (2 / ((logโ2) โ (1 / (2 ยท e))))
โ โ) |
84 | 1, 82, 83 | mp2an 691 |
. . . 4
โข (2 /
((logโ2) โ (1 / (2 ยท e)))) โ โ |
85 | 84 | a1i 11 |
. . 3
โข (โค
โ (2 / ((logโ2) โ (1 / (2 ยท e)))) โ
โ) |
86 | | rpre 12930 |
. . . . . . . 8
โข (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ+ โ ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ) |
87 | | rpge0 12935 |
. . . . . . . 8
โข (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ+ โ 0 โค
((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) |
88 | 86, 87 | absidd 15314 |
. . . . . . 7
โข (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ+ โ
(absโ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ))) =
((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) |
89 | 26, 88 | syl 17 |
. . . . . 6
โข (๐ฅ โ (2[,)+โ) โ
(absโ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ))) =
((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) |
90 | 89 | adantr 482 |
. . . . 5
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ
(absโ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ))) =
((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) |
91 | | eqid 2737 |
. . . . . . . . . 10
โข
(โโ(๐ฅ /
2)) = (โโ(๐ฅ /
2)) |
92 | 91 | chebbnd1lem3 26835 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง 8 โค
๐ฅ) โ (((logโ2)
โ (1 / (2 ยท e))) / 2) < ((ฯโ๐ฅ) ยท ((logโ๐ฅ) / ๐ฅ))) |
93 | 8, 92 | sylan 581 |
. . . . . . . 8
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ
(((logโ2) โ (1 / (2 ยท e))) / 2) <
((ฯโ๐ฅ)
ยท ((logโ๐ฅ) /
๐ฅ))) |
94 | 1 | recni 11176 |
. . . . . . . . . 10
โข 2 โ
โ |
95 | | 2ne0 12264 |
. . . . . . . . . 10
โข 2 โ
0 |
96 | 41 | recni 11176 |
. . . . . . . . . 10
โข
((logโ2) โ (1 / (2 ยท e))) โ
โ |
97 | 41, 81 | gt0ne0ii 11698 |
. . . . . . . . . 10
โข
((logโ2) โ (1 / (2 ยท e))) โ 0 |
98 | | recdiv 11868 |
. . . . . . . . . 10
โข (((2
โ โ โง 2 โ 0) โง (((logโ2) โ (1 / (2 ยท
e))) โ โ โง ((logโ2) โ (1 / (2 ยท e))) โ 0))
โ (1 / (2 / ((logโ2) โ (1 / (2 ยท e))))) =
(((logโ2) โ (1 / (2 ยท e))) / 2)) |
99 | 94, 95, 96, 97, 98 | mp4an 692 |
. . . . . . . . 9
โข (1 / (2 /
((logโ2) โ (1 / (2 ยท e))))) = (((logโ2) โ (1 /
(2 ยท e))) / 2) |
100 | 99 | a1i 11 |
. . . . . . . 8
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ (1 / (2 /
((logโ2) โ (1 / (2 ยท e))))) = (((logโ2) โ (1 /
(2 ยท e))) / 2)) |
101 | 22 | rpcnd 12966 |
. . . . . . . . . . 11
โข (๐ฅ โ (2[,)+โ) โ
(๐ฅ / (logโ๐ฅ)) โ
โ) |
102 | 24 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ฅ โ (2[,)+โ) โ
(ฯโ๐ฅ)
โ โ) |
103 | 22 | rpne0d 12969 |
. . . . . . . . . . 11
โข (๐ฅ โ (2[,)+โ) โ
(๐ฅ / (logโ๐ฅ)) โ 0) |
104 | 24 | nnne0d 12210 |
. . . . . . . . . . 11
โข (๐ฅ โ (2[,)+โ) โ
(ฯโ๐ฅ) โ
0) |
105 | 101, 102,
103, 104 | recdivd 11955 |
. . . . . . . . . 10
โข (๐ฅ โ (2[,)+โ) โ (1
/ ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) = ((ฯโ๐ฅ) / (๐ฅ / (logโ๐ฅ)))) |
106 | 102, 101,
103 | divrecd 11941 |
. . . . . . . . . 10
โข (๐ฅ โ (2[,)+โ) โ
((ฯโ๐ฅ) /
(๐ฅ / (logโ๐ฅ))) = ((ฯโ๐ฅ) ยท (1 / (๐ฅ / (logโ๐ฅ))))) |
107 | 20 | rpcnne0d 12973 |
. . . . . . . . . . . 12
โข (๐ฅ โ (2[,)+โ) โ
(๐ฅ โ โ โง
๐ฅ โ 0)) |
108 | 21 | rpcnne0d 12973 |
. . . . . . . . . . . 12
โข (๐ฅ โ (2[,)+โ) โ
((logโ๐ฅ) โ
โ โง (logโ๐ฅ)
โ 0)) |
109 | | recdiv 11868 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ฅ โ 0) โง ((logโ๐ฅ) โ โ โง
(logโ๐ฅ) โ 0))
โ (1 / (๐ฅ /
(logโ๐ฅ))) =
((logโ๐ฅ) / ๐ฅ)) |
110 | 107, 108,
109 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ฅ โ (2[,)+โ) โ (1
/ (๐ฅ / (logโ๐ฅ))) = ((logโ๐ฅ) / ๐ฅ)) |
111 | 110 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ฅ โ (2[,)+โ) โ
((ฯโ๐ฅ)
ยท (1 / (๐ฅ /
(logโ๐ฅ)))) =
((ฯโ๐ฅ)
ยท ((logโ๐ฅ) /
๐ฅ))) |
112 | 105, 106,
111 | 3eqtrd 2781 |
. . . . . . . . 9
โข (๐ฅ โ (2[,)+โ) โ (1
/ ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) = ((ฯโ๐ฅ) ยท ((logโ๐ฅ) / ๐ฅ))) |
113 | 112 | adantr 482 |
. . . . . . . 8
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ (1 / ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) = ((ฯโ๐ฅ) ยท ((logโ๐ฅ) / ๐ฅ))) |
114 | 93, 100, 113 | 3brtr4d 5142 |
. . . . . . 7
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ (1 / (2 /
((logโ2) โ (1 / (2 ยท e))))) < (1 / ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)))) |
115 | 26 | adantr 482 |
. . . . . . . 8
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ
โ+) |
116 | | elrp 12924 |
. . . . . . . . 9
โข (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ+ โ (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ โง 0 < ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)))) |
117 | 1, 41, 36, 81 | divgt0ii 12079 |
. . . . . . . . . 10
โข 0 < (2
/ ((logโ2) โ (1 / (2 ยท e)))) |
118 | | ltrec 12044 |
. . . . . . . . . 10
โข
(((((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ))
โ โ โง 0 < ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) โง ((2 / ((logโ2) โ (1 /
(2 ยท e)))) โ โ โง 0 < (2 / ((logโ2) โ (1 /
(2 ยท e)))))) โ (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) < (2 / ((logโ2) โ (1 / (2
ยท e)))) โ (1 / (2 / ((logโ2) โ (1 / (2 ยท e)))))
< (1 / ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ))))) |
119 | 84, 117, 118 | mpanr12 704 |
. . . . . . . . 9
โข ((((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ โง 0 < ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) โ (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) < (2 / ((logโ2) โ (1 / (2
ยท e)))) โ (1 / (2 / ((logโ2) โ (1 / (2 ยท e)))))
< (1 / ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ))))) |
120 | 116, 119 | sylbi 216 |
. . . . . . . 8
โข (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ+ โ (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) < (2 / ((logโ2) โ (1 / (2
ยท e)))) โ (1 / (2 / ((logโ2) โ (1 / (2 ยท e)))))
< (1 / ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ))))) |
121 | 115, 120 | syl 17 |
. . . . . . 7
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) < (2 / ((logโ2) โ (1 / (2
ยท e)))) โ (1 / (2 / ((logโ2) โ (1 / (2 ยท e)))))
< (1 / ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ))))) |
122 | 114, 121 | mpbird 257 |
. . . . . 6
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) < (2 / ((logโ2) โ (1 / (2
ยท e))))) |
123 | 115 | rpred 12964 |
. . . . . . 7
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ) |
124 | | ltle 11250 |
. . . . . . 7
โข ((((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โ โ โง (2 / ((logโ2)
โ (1 / (2 ยท e)))) โ โ) โ (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) < (2 / ((logโ2) โ (1 / (2
ยท e)))) โ ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ)) โค
(2 / ((logโ2) โ (1 / (2 ยท e)))))) |
125 | 123, 84, 124 | sylancl 587 |
. . . . . 6
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ (((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) < (2 / ((logโ2) โ (1 / (2
ยท e)))) โ ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ)) โค
(2 / ((logโ2) โ (1 / (2 ยท e)))))) |
126 | 122, 125 | mpd 15 |
. . . . 5
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ)) โค (2 / ((logโ2) โ (1 / (2
ยท e))))) |
127 | 90, 126 | eqbrtrd 5132 |
. . . 4
โข ((๐ฅ โ (2[,)+โ) โง 8
โค ๐ฅ) โ
(absโ((๐ฅ /
(logโ๐ฅ)) /
(ฯโ๐ฅ)))
โค (2 / ((logโ2) โ (1 / (2 ยท e))))) |
128 | 127 | adantl 483 |
. . 3
โข
((โค โง (๐ฅ
โ (2[,)+โ) โง 8 โค ๐ฅ)) โ (absโ((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) โค (2 / ((logโ2) โ (1 / (2
ยท e))))) |
129 | 5, 28, 30, 85, 128 | elo1d 15425 |
. 2
โข (โค
โ (๐ฅ โ
(2[,)+โ) โฆ ((๐ฅ
/ (logโ๐ฅ)) /
(ฯโ๐ฅ)))
โ ๐(1)) |
130 | 129 | mptru 1549 |
1
โข (๐ฅ โ (2[,)+โ) โฆ
((๐ฅ / (logโ๐ฅ)) / (ฯโ๐ฅ))) โ
๐(1) |