Step | Hyp | Ref
| Expression |
1 | | 2rp 12927 |
. . . . 5
โข 2 โ
โ+ |
2 | | 4nn 12243 |
. . . . . . 7
โข 4 โ
โ |
3 | | 4z 12544 |
. . . . . . . . 9
โข 4 โ
โค |
4 | 3 | a1i 11 |
. . . . . . . 8
โข ((๐ โ โ โง 8 โค
๐) โ 4 โ
โค) |
5 | | chebbnd1lem2.1 |
. . . . . . . . 9
โข ๐ = (โโ(๐ / 2)) |
6 | | rehalfcl 12386 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ / 2) โ
โ) |
7 | 6 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ โง 8 โค
๐) โ (๐ / 2) โ
โ) |
8 | 7 | flcld 13710 |
. . . . . . . . 9
โข ((๐ โ โ โง 8 โค
๐) โ
(โโ(๐ / 2))
โ โค) |
9 | 5, 8 | eqeltrid 2842 |
. . . . . . . 8
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ โค) |
10 | | 4t2e8 12328 |
. . . . . . . . . . . 12
โข (4
ยท 2) = 8 |
11 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 8 โค
๐) โ 8 โค ๐) |
12 | 10, 11 | eqbrtrid 5145 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 8 โค
๐) โ (4 ยท 2)
โค ๐) |
13 | | 4re 12244 |
. . . . . . . . . . . . 13
โข 4 โ
โ |
14 | 13 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 8 โค
๐) โ 4 โ
โ) |
15 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ โ) |
16 | | 2re 12234 |
. . . . . . . . . . . . 13
โข 2 โ
โ |
17 | 16 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 8 โค
๐) โ 2 โ
โ) |
18 | | 2pos 12263 |
. . . . . . . . . . . . 13
โข 0 <
2 |
19 | 18 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 8 โค
๐) โ 0 <
2) |
20 | | lemuldiv 12042 |
. . . . . . . . . . . 12
โข ((4
โ โ โง ๐
โ โ โง (2 โ โ โง 0 < 2)) โ ((4 ยท 2)
โค ๐ โ 4 โค (๐ / 2))) |
21 | 14, 15, 17, 19, 20 | syl112anc 1375 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 8 โค
๐) โ ((4 ยท 2)
โค ๐ โ 4 โค (๐ / 2))) |
22 | 12, 21 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โ โ โง 8 โค
๐) โ 4 โค (๐ / 2)) |
23 | | flge 13717 |
. . . . . . . . . . 11
โข (((๐ / 2) โ โ โง 4
โ โค) โ (4 โค (๐ / 2) โ 4 โค (โโ(๐ / 2)))) |
24 | 7, 3, 23 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ โ โ โง 8 โค
๐) โ (4 โค (๐ / 2) โ 4 โค
(โโ(๐ /
2)))) |
25 | 22, 24 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โ โ โง 8 โค
๐) โ 4 โค
(โโ(๐ /
2))) |
26 | 25, 5 | breqtrrdi 5152 |
. . . . . . . 8
โข ((๐ โ โ โง 8 โค
๐) โ 4 โค ๐) |
27 | | eluz2 12776 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ4) โ (4 โ โค โง ๐ โ โค โง 4 โค
๐)) |
28 | 4, 9, 26, 27 | syl3anbrc 1344 |
. . . . . . 7
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ
(โคโฅโ4)) |
29 | | eluznn 12850 |
. . . . . . 7
โข ((4
โ โ โง ๐
โ (โคโฅโ4)) โ ๐ โ โ) |
30 | 2, 28, 29 | sylancr 588 |
. . . . . 6
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ โ) |
31 | 30 | nnrpd 12962 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ
โ+) |
32 | | rpmulcl 12945 |
. . . . 5
โข ((2
โ โ+ โง ๐ โ โ+) โ (2
ยท ๐) โ
โ+) |
33 | 1, 31, 32 | sylancr 588 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ (2 ยท ๐) โ
โ+) |
34 | 33 | relogcld 25994 |
. . 3
โข ((๐ โ โ โง 8 โค
๐) โ (logโ(2
ยท ๐)) โ
โ) |
35 | 34, 33 | rerpdivcld 12995 |
. 2
โข ((๐ โ โ โง 8 โค
๐) โ ((logโ(2
ยท ๐)) / (2 ยท
๐)) โ
โ) |
36 | | 0red 11165 |
. . . . . . 7
โข ((๐ โ โ โง 8 โค
๐) โ 0 โ
โ) |
37 | | 8re 12256 |
. . . . . . . 8
โข 8 โ
โ |
38 | 37 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ โง 8 โค
๐) โ 8 โ
โ) |
39 | | 8pos 12272 |
. . . . . . . 8
โข 0 <
8 |
40 | 39 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ โง 8 โค
๐) โ 0 <
8) |
41 | 36, 38, 15, 40, 11 | ltletrd 11322 |
. . . . . 6
โข ((๐ โ โ โง 8 โค
๐) โ 0 < ๐) |
42 | 15, 41 | elrpd 12961 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ
โ+) |
43 | 42 | rphalfcld 12976 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ (๐ / 2) โ
โ+) |
44 | 43 | relogcld 25994 |
. . 3
โข ((๐ โ โ โง 8 โค
๐) โ (logโ(๐ / 2)) โ
โ) |
45 | 44, 43 | rerpdivcld 12995 |
. 2
โข ((๐ โ โ โง 8 โค
๐) โ
((logโ(๐ / 2)) /
(๐ / 2)) โ
โ) |
46 | 42 | relogcld 25994 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ (logโ๐) โ
โ) |
47 | 46, 42 | rerpdivcld 12995 |
. . 3
โข ((๐ โ โ โง 8 โค
๐) โ ((logโ๐) / ๐) โ โ) |
48 | | remulcl 11143 |
. . 3
โข ((2
โ โ โง ((logโ๐) / ๐) โ โ) โ (2 ยท
((logโ๐) / ๐)) โ
โ) |
49 | 16, 47, 48 | sylancr 588 |
. 2
โข ((๐ โ โ โง 8 โค
๐) โ (2 ยท
((logโ๐) / ๐)) โ
โ) |
50 | 9 | zred 12614 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ โ) |
51 | | peano2re 11335 |
. . . . 5
โข (๐ โ โ โ (๐ + 1) โ
โ) |
52 | 50, 51 | syl 17 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ (๐ + 1) โ
โ) |
53 | | remulcl 11143 |
. . . . 5
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
54 | 16, 50, 53 | sylancr 588 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ (2 ยท ๐) โ
โ) |
55 | | flltp1 13712 |
. . . . . 6
โข ((๐ / 2) โ โ โ
(๐ / 2) <
((โโ(๐ / 2)) +
1)) |
56 | 7, 55 | syl 17 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ (๐ / 2) <
((โโ(๐ / 2)) +
1)) |
57 | 5 | oveq1i 7372 |
. . . . 5
โข (๐ + 1) = ((โโ(๐ / 2)) + 1) |
58 | 56, 57 | breqtrrdi 5152 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ (๐ / 2) < (๐ + 1)) |
59 | | 1red 11163 |
. . . . . 6
โข ((๐ โ โ โง 8 โค
๐) โ 1 โ
โ) |
60 | 30 | nnge1d 12208 |
. . . . . 6
โข ((๐ โ โ โง 8 โค
๐) โ 1 โค ๐) |
61 | 59, 50, 50, 60 | leadd2dd 11777 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ (๐ + 1) โค (๐ + ๐)) |
62 | 50 | recnd 11190 |
. . . . . 6
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ โ) |
63 | 62 | 2timesd 12403 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ (2 ยท ๐) = (๐ + ๐)) |
64 | 61, 63 | breqtrrd 5138 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ (๐ + 1) โค (2 ยท ๐)) |
65 | 7, 52, 54, 58, 64 | ltletrd 11322 |
. . 3
โข ((๐ โ โ โง 8 โค
๐) โ (๐ / 2) < (2 ยท ๐)) |
66 | | ere 15978 |
. . . . . 6
โข e โ
โ |
67 | 66 | a1i 11 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ e โ
โ) |
68 | | egt2lt3 16095 |
. . . . . . . . 9
โข (2 < e
โง e < 3) |
69 | 68 | simpri 487 |
. . . . . . . 8
โข e <
3 |
70 | | 3lt4 12334 |
. . . . . . . 8
โข 3 <
4 |
71 | | 3re 12240 |
. . . . . . . . 9
โข 3 โ
โ |
72 | 66, 71, 13 | lttri 11288 |
. . . . . . . 8
โข ((e <
3 โง 3 < 4) โ e < 4) |
73 | 69, 70, 72 | mp2an 691 |
. . . . . . 7
โข e <
4 |
74 | 73 | a1i 11 |
. . . . . 6
โข ((๐ โ โ โง 8 โค
๐) โ e <
4) |
75 | 67, 14, 7, 74, 22 | ltletrd 11322 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ e < (๐ / 2)) |
76 | 67, 7, 75 | ltled 11310 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ e โค (๐ / 2)) |
77 | 67, 7, 54, 75, 65 | lttrd 11323 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ e < (2
ยท ๐)) |
78 | 67, 54, 77 | ltled 11310 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ e โค (2
ยท ๐)) |
79 | | logdivlt 25992 |
. . . 4
โข ((((๐ / 2) โ โ โง e
โค (๐ / 2)) โง ((2
ยท ๐) โ โ
โง e โค (2 ยท ๐))) โ ((๐ / 2) < (2 ยท ๐) โ ((logโ(2 ยท ๐)) / (2 ยท ๐)) < ((logโ(๐ / 2)) / (๐ / 2)))) |
80 | 7, 76, 54, 78, 79 | syl22anc 838 |
. . 3
โข ((๐ โ โ โง 8 โค
๐) โ ((๐ / 2) < (2 ยท ๐) โ ((logโ(2 ยท
๐)) / (2 ยท ๐)) < ((logโ(๐ / 2)) / (๐ / 2)))) |
81 | 65, 80 | mpbid 231 |
. 2
โข ((๐ โ โ โง 8 โค
๐) โ ((logโ(2
ยท ๐)) / (2 ยท
๐)) < ((logโ(๐ / 2)) / (๐ / 2))) |
82 | | rphalflt 12951 |
. . . . . 6
โข (๐ โ โ+
โ (๐ / 2) < ๐) |
83 | 42, 82 | syl 17 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ (๐ / 2) < ๐) |
84 | | logltb 25971 |
. . . . . 6
โข (((๐ / 2) โ โ+
โง ๐ โ
โ+) โ ((๐ / 2) < ๐ โ (logโ(๐ / 2)) < (logโ๐))) |
85 | 43, 42, 84 | syl2anc 585 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ ((๐ / 2) < ๐ โ (logโ(๐ / 2)) < (logโ๐))) |
86 | 83, 85 | mpbid 231 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ (logโ(๐ / 2)) < (logโ๐)) |
87 | 44, 46, 43, 86 | ltdiv1dd 13021 |
. . 3
โข ((๐ โ โ โง 8 โค
๐) โ
((logโ(๐ / 2)) /
(๐ / 2)) <
((logโ๐) / (๐ / 2))) |
88 | 46 | recnd 11190 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ (logโ๐) โ
โ) |
89 | 15 | recnd 11190 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ โ) |
90 | 17 | recnd 11190 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ 2 โ
โ) |
91 | 42 | rpne0d 12969 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ ๐ โ 0) |
92 | | 2ne0 12264 |
. . . . . 6
โข 2 โ
0 |
93 | 92 | a1i 11 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ 2 โ
0) |
94 | 88, 89, 90, 91, 93 | divdiv2d 11970 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ ((logโ๐) / (๐ / 2)) = (((logโ๐) ยท 2) / ๐)) |
95 | 88, 90 | mulcomd 11183 |
. . . . 5
โข ((๐ โ โ โง 8 โค
๐) โ ((logโ๐) ยท 2) = (2 ยท
(logโ๐))) |
96 | 95 | oveq1d 7377 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ
(((logโ๐) ยท 2)
/ ๐) = ((2 ยท
(logโ๐)) / ๐)) |
97 | 90, 88, 89, 91 | divassd 11973 |
. . . 4
โข ((๐ โ โ โง 8 โค
๐) โ ((2 ยท
(logโ๐)) / ๐) = (2 ยท
((logโ๐) / ๐))) |
98 | 94, 96, 97 | 3eqtrd 2781 |
. . 3
โข ((๐ โ โ โง 8 โค
๐) โ ((logโ๐) / (๐ / 2)) = (2 ยท ((logโ๐) / ๐))) |
99 | 87, 98 | breqtrd 5136 |
. 2
โข ((๐ โ โ โง 8 โค
๐) โ
((logโ(๐ / 2)) /
(๐ / 2)) < (2 ยท
((logโ๐) / ๐))) |
100 | 35, 45, 49, 81, 99 | lttrd 11323 |
1
โข ((๐ โ โ โง 8 โค
๐) โ ((logโ(2
ยท ๐)) / (2 ยท
๐)) < (2 ยท
((logโ๐) / ๐))) |