Step | Hyp | Ref
| Expression |
1 | | 2re 12093 |
. . 3
โข 2 โ
โ |
2 | | 1le2 12228 |
. . 3
โข 1 โค
2 |
3 | | chpdifbnd 26748 |
. . 3
โข ((2
โ โ โง 1 โค 2) โ โ๐ก โ โ+ โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ))))) |
4 | 1, 2, 3 | mp2an 690 |
. 2
โข
โ๐ก โ
โ+ โ๐ฃ โ (1(,)+โ)โ๐ค โ (๐ฃ[,](2 ยท ๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))) |
5 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ๐ก โ โ+) โ ๐ก โ
โ+) |
6 | | ioossre 13186 |
. . . . . . . . . . . . 13
โข (0(,)1)
โ โ |
7 | | pntibndlem3.4 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ธ โ (0(,)1)) |
8 | 6, 7 | sselid 3924 |
. . . . . . . . . . . 12
โข (๐ โ ๐ธ โ โ) |
9 | | eliooord 13184 |
. . . . . . . . . . . . . 14
โข (๐ธ โ (0(,)1) โ (0 <
๐ธ โง ๐ธ < 1)) |
10 | 7, 9 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (0 < ๐ธ โง ๐ธ < 1)) |
11 | 10 | simpld 496 |
. . . . . . . . . . . 12
โข (๐ โ 0 < ๐ธ) |
12 | 8, 11 | elrpd 12815 |
. . . . . . . . . . 11
โข (๐ โ ๐ธ โ
โ+) |
13 | 12 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ก โ โ+) โ ๐ธ โ
โ+) |
14 | | 4nn 12102 |
. . . . . . . . . . 11
โข 4 โ
โ |
15 | | nnrp 12787 |
. . . . . . . . . . 11
โข (4 โ
โ โ 4 โ โ+) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . 10
โข 4 โ
โ+ |
17 | | rpdivcl 12801 |
. . . . . . . . . 10
โข ((๐ธ โ โ+
โง 4 โ โ+) โ (๐ธ / 4) โ
โ+) |
18 | 13, 16, 17 | sylancl 587 |
. . . . . . . . 9
โข ((๐ โง ๐ก โ โ+) โ (๐ธ / 4) โ
โ+) |
19 | 5, 18 | rpdivcld 12835 |
. . . . . . . 8
โข ((๐ โง ๐ก โ โ+) โ (๐ก / (๐ธ / 4)) โ
โ+) |
20 | 19 | rpred 12818 |
. . . . . . 7
โข ((๐ โง ๐ก โ โ+) โ (๐ก / (๐ธ / 4)) โ โ) |
21 | 20 | rpefcld 15859 |
. . . . . 6
โข ((๐ โง ๐ก โ โ+) โ
(expโ(๐ก / (๐ธ / 4))) โ
โ+) |
22 | | pntibndlem3.6 |
. . . . . . 7
โข (๐ โ ๐ โ
โ+) |
23 | 22 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ก โ โ+) โ ๐ โ
โ+) |
24 | 21, 23 | rpaddcld 12833 |
. . . . 5
โข ((๐ โง ๐ก โ โ+) โ
((expโ(๐ก / (๐ธ / 4))) + ๐) โ
โ+) |
25 | 24 | adantrr 715 |
. . . 4
โข ((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โ ((expโ(๐ก / (๐ธ / 4))) + ๐) โ
โ+) |
26 | | breq2 5085 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ฃ < ๐ โ ๐ฃ < ๐)) |
27 | | breq1 5084 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ โค ((๐ / 2) ยท ๐ฃ) โ ๐ โค ((๐ / 2) ยท ๐ฃ))) |
28 | 26, 27 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โ (๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)))) |
29 | | fveq2 6804 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐
โ๐) = (๐
โ๐)) |
30 | | id 22 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ๐ = ๐) |
31 | 29, 30 | oveq12d 7325 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐
โ๐) / ๐) = ((๐
โ๐) / ๐)) |
32 | 31 | fveq2d 6808 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (absโ((๐
โ๐) / ๐)) = (absโ((๐
โ๐) / ๐))) |
33 | 32 | breq1d 5091 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((absโ((๐
โ๐) / ๐)) โค (๐ธ / 2) โ (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))) |
34 | 28, 33 | anbi12d 632 |
. . . . . . . . 9
โข (๐ = ๐ โ (((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)) โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)))) |
35 | 34 | cbvrexvw 3223 |
. . . . . . . 8
โข
(โ๐ โ
โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)) โ โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))) |
36 | | breq1 5084 |
. . . . . . . . . . 11
โข (๐ฃ = ๐ฆ โ (๐ฃ < ๐ โ ๐ฆ < ๐)) |
37 | | oveq2 7315 |
. . . . . . . . . . . 12
โข (๐ฃ = ๐ฆ โ ((๐ / 2) ยท ๐ฃ) = ((๐ / 2) ยท ๐ฆ)) |
38 | 37 | breq2d 5093 |
. . . . . . . . . . 11
โข (๐ฃ = ๐ฆ โ (๐ โค ((๐ / 2) ยท ๐ฃ) โ ๐ โค ((๐ / 2) ยท ๐ฆ))) |
39 | 36, 38 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ฃ = ๐ฆ โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โ (๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)))) |
40 | 39 | anbi1d 631 |
. . . . . . . . 9
โข (๐ฃ = ๐ฆ โ (((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)) โ ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)))) |
41 | 40 | rexbidv 3172 |
. . . . . . . 8
โข (๐ฃ = ๐ฆ โ (โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)) โ โ๐ โ โ ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)))) |
42 | 35, 41 | bitrid 283 |
. . . . . . 7
โข (๐ฃ = ๐ฆ โ (โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)) โ โ๐ โ โ ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)))) |
43 | | oveq1 7314 |
. . . . . . . . . . . . 13
โข (๐ = (๐ / 2) โ (๐ ยท ๐ฃ) = ((๐ / 2) ยท ๐ฃ)) |
44 | 43 | breq2d 5093 |
. . . . . . . . . . . 12
โข (๐ = (๐ / 2) โ (๐ โค (๐ ยท ๐ฃ) โ ๐ โค ((๐ / 2) ยท ๐ฃ))) |
45 | 44 | anbi2d 630 |
. . . . . . . . . . 11
โข (๐ = (๐ / 2) โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โ (๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)))) |
46 | 45 | anbi1d 631 |
. . . . . . . . . 10
โข (๐ = (๐ / 2) โ (((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)) โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)))) |
47 | 46 | rexbidv 3172 |
. . . . . . . . 9
โข (๐ = (๐ / 2) โ (โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)) โ โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)))) |
48 | 47 | ralbidv 3171 |
. . . . . . . 8
โข (๐ = (๐ / 2) โ (โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)) โ โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)))) |
49 | | pntibndlem3.5 |
. . . . . . . . 9
โข (๐ โ โ๐ โ (๐พ[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))) |
50 | 49 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ โ๐ โ (๐พ[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))) |
51 | | pntibndlem3.c |
. . . . . . . . . . . . . . . . 17
โข ๐ถ = ((2 ยท ๐ต) +
(logโ2)) |
52 | | pntibndlem3.3 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ต โ
โ+) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ก โ โ+) โ ๐ต โ
โ+) |
54 | 53 | rpred 12818 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ก โ โ+) โ ๐ต โ
โ) |
55 | | remulcl 11002 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
โ โ โง ๐ต
โ โ) โ (2 ยท ๐ต) โ โ) |
56 | 1, 54, 55 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ก โ โ+) โ (2
ยท ๐ต) โ
โ) |
57 | | 2rp 12781 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ+ |
58 | | relogcl 25776 |
. . . . . . . . . . . . . . . . . . 19
โข (2 โ
โ+ โ (logโ2) โ โ) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
โข
(logโ2) โ โ |
60 | | readdcl 11000 |
. . . . . . . . . . . . . . . . . 18
โข (((2
ยท ๐ต) โ โ
โง (logโ2) โ โ) โ ((2 ยท ๐ต) + (logโ2)) โ
โ) |
61 | 56, 59, 60 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ก โ โ+) โ ((2
ยท ๐ต) +
(logโ2)) โ โ) |
62 | 51, 61 | eqeltrid 2841 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ก โ โ+) โ ๐ถ โ
โ) |
63 | 62, 13 | rerpdivcld 12849 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ก โ โ+) โ (๐ถ / ๐ธ) โ โ) |
64 | 63 | reefcld 15842 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ก โ โ+) โ
(expโ(๐ถ / ๐ธ)) โ
โ) |
65 | | elicopnf 13223 |
. . . . . . . . . . . . . 14
โข
((expโ(๐ถ /
๐ธ)) โ โ โ
(๐ โ
((expโ(๐ถ / ๐ธ))[,)+โ) โ (๐ โ โ โง
(expโ(๐ถ / ๐ธ)) โค ๐))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ก โ โ+) โ (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โ (๐ โ โ โง (expโ(๐ถ / ๐ธ)) โค ๐))) |
67 | 66 | simprbda 500 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ ๐ โ โ) |
68 | 67 | rehalfcld 12266 |
. . . . . . . . . . 11
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ (๐ / 2) โ โ) |
69 | | pntibndlem3.k |
. . . . . . . . . . . 12
โข ๐พ = (expโ(๐ต / (๐ธ / 2))) |
70 | 13 | rphalfcld 12830 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ก โ โ+) โ (๐ธ / 2) โ
โ+) |
71 | 54, 70 | rerpdivcld 12849 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ก โ โ+) โ (๐ต / (๐ธ / 2)) โ โ) |
72 | 71 | reefcld 15842 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ก โ โ+) โ
(expโ(๐ต / (๐ธ / 2))) โ
โ) |
73 | | remulcl 11002 |
. . . . . . . . . . . . . . . 16
โข
(((expโ(๐ต /
(๐ธ / 2))) โ โ
โง 2 โ โ) โ ((expโ(๐ต / (๐ธ / 2))) ยท 2) โ
โ) |
74 | 72, 1, 73 | sylancl 587 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ก โ โ+) โ
((expโ(๐ต / (๐ธ / 2))) ยท 2) โ
โ) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ ((expโ(๐ต / (๐ธ / 2))) ยท 2) โ
โ) |
76 | 64 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ (expโ(๐ถ / ๐ธ)) โ โ) |
77 | 71 | recnd 11049 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ก โ โ+) โ (๐ต / (๐ธ / 2)) โ โ) |
78 | 59 | recni 11035 |
. . . . . . . . . . . . . . . . . 18
โข
(logโ2) โ โ |
79 | | efadd 15848 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ต / (๐ธ / 2)) โ โ โง (logโ2)
โ โ) โ (expโ((๐ต / (๐ธ / 2)) + (logโ2))) =
((expโ(๐ต / (๐ธ / 2))) ยท
(expโ(logโ2)))) |
80 | 77, 78, 79 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ก โ โ+) โ
(expโ((๐ต / (๐ธ / 2)) + (logโ2))) =
((expโ(๐ต / (๐ธ / 2))) ยท
(expโ(logโ2)))) |
81 | | reeflog 25781 |
. . . . . . . . . . . . . . . . . . 19
โข (2 โ
โ+ โ (expโ(logโ2)) = 2) |
82 | 57, 81 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
โข
(expโ(logโ2)) = 2 |
83 | 82 | oveq2i 7318 |
. . . . . . . . . . . . . . . . 17
โข
((expโ(๐ต /
(๐ธ / 2))) ยท
(expโ(logโ2))) = ((expโ(๐ต / (๐ธ / 2))) ยท 2) |
84 | 80, 83 | eqtrdi 2792 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ก โ โ+) โ
(expโ((๐ต / (๐ธ / 2)) + (logโ2))) =
((expโ(๐ต / (๐ธ / 2))) ยท
2)) |
85 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ก โ โ+) โ
(logโ2) โ โ) |
86 | | rerpdivcl 12806 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((logโ2) โ โ โง ๐ธ โ โ+) โ
((logโ2) / ๐ธ) โ
โ) |
87 | 59, 13, 86 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ก โ โ+) โ
((logโ2) / ๐ธ) โ
โ) |
88 | 78 | div1i 11749 |
. . . . . . . . . . . . . . . . . . . 20
โข
((logโ2) / 1) = (logโ2) |
89 | 10 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ธ < 1) |
90 | 89 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ก โ โ+) โ ๐ธ < 1) |
91 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ก โ โ+) โ ๐ธ โ
โ) |
92 | | 1re 11021 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 1 โ
โ |
93 | | ltle 11109 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ธ โ โ โง 1 โ
โ) โ (๐ธ < 1
โ ๐ธ โค
1)) |
94 | 91, 92, 93 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ก โ โ+) โ (๐ธ < 1 โ ๐ธ โค 1)) |
95 | 90, 94 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ก โ โ+) โ ๐ธ โค 1) |
96 | 13 | rpregt0d 12824 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ก โ โ+) โ (๐ธ โ โ โง 0 <
๐ธ)) |
97 | | 1rp 12780 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 1 โ
โ+ |
98 | | rpregt0 12790 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (1 โ
โ+ โ (1 โ โ โง 0 < 1)) |
99 | 97, 98 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ก โ โ+) โ (1 โ
โ โง 0 < 1)) |
100 | | 1lt2 12190 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 1 <
2 |
101 | | rplogcl 25804 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((2
โ โ โง 1 < 2) โ (logโ2) โ
โ+) |
102 | 1, 100, 101 | mp2an 690 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(logโ2) โ โ+ |
103 | | rpregt0 12790 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
((logโ2) โ โ+ โ ((logโ2) โ
โ โง 0 < (logโ2))) |
104 | 102, 103 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ก โ โ+) โ
((logโ2) โ โ โง 0 < (logโ2))) |
105 | | lediv2 11911 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ธ โ โ โง 0 <
๐ธ) โง (1 โ โ
โง 0 < 1) โง ((logโ2) โ โ โง 0 <
(logโ2))) โ (๐ธ
โค 1 โ ((logโ2) / 1) โค ((logโ2) / ๐ธ))) |
106 | 96, 99, 104, 105 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ก โ โ+) โ (๐ธ โค 1 โ ((logโ2) /
1) โค ((logโ2) / ๐ธ))) |
107 | 95, 106 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ก โ โ+) โ
((logโ2) / 1) โค ((logโ2) / ๐ธ)) |
108 | 88, 107 | eqbrtrrid 5117 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ก โ โ+) โ
(logโ2) โค ((logโ2) / ๐ธ)) |
109 | 85, 87, 71, 108 | leadd2dd 11636 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ก โ โ+) โ ((๐ต / (๐ธ / 2)) + (logโ2)) โค ((๐ต / (๐ธ / 2)) + ((logโ2) / ๐ธ))) |
110 | 51 | oveq1i 7317 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ถ / ๐ธ) = (((2 ยท ๐ต) + (logโ2)) / ๐ธ) |
111 | 56 | recnd 11049 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ก โ โ+) โ (2
ยท ๐ต) โ
โ) |
112 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ก โ โ+) โ
(logโ2) โ โ) |
113 | | rpcnne0 12794 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ธ โ โ+
โ (๐ธ โ โ
โง ๐ธ โ
0)) |
114 | 13, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ก โ โ+) โ (๐ธ โ โ โง ๐ธ โ 0)) |
115 | | divdir 11704 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((2
ยท ๐ต) โ โ
โง (logโ2) โ โ โง (๐ธ โ โ โง ๐ธ โ 0)) โ (((2 ยท ๐ต) + (logโ2)) / ๐ธ) = (((2 ยท ๐ต) / ๐ธ) + ((logโ2) / ๐ธ))) |
116 | 111, 112,
114, 115 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ก โ โ+) โ (((2
ยท ๐ต) +
(logโ2)) / ๐ธ) = (((2
ยท ๐ต) / ๐ธ) + ((logโ2) / ๐ธ))) |
117 | 110, 116 | eqtrid 2788 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ก โ โ+) โ (๐ถ / ๐ธ) = (((2 ยท ๐ต) / ๐ธ) + ((logโ2) / ๐ธ))) |
118 | 1 | recni 11035 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 2 โ
โ |
119 | 54 | recnd 11049 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ก โ โ+) โ ๐ต โ
โ) |
120 | | mulcom 11003 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((2
โ โ โง ๐ต
โ โ) โ (2 ยท ๐ต) = (๐ต ยท 2)) |
121 | 118, 119,
120 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ก โ โ+) โ (2
ยท ๐ต) = (๐ต ยท 2)) |
122 | 121 | oveq1d 7322 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ก โ โ+) โ ((2
ยท ๐ต) / ๐ธ) = ((๐ต ยท 2) / ๐ธ)) |
123 | | rpcnne0 12794 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (2 โ
โ+ โ (2 โ โ โง 2 โ 0)) |
124 | 57, 123 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ก โ โ+) โ (2 โ
โ โง 2 โ 0)) |
125 | | divdiv2 11733 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ต โ โ โง (๐ธ โ โ โง ๐ธ โ 0) โง (2 โ โ
โง 2 โ 0)) โ (๐ต
/ (๐ธ / 2)) = ((๐ต ยท 2) / ๐ธ)) |
126 | 119, 114,
124, 125 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ก โ โ+) โ (๐ต / (๐ธ / 2)) = ((๐ต ยท 2) / ๐ธ)) |
127 | 122, 126 | eqtr4d 2779 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ก โ โ+) โ ((2
ยท ๐ต) / ๐ธ) = (๐ต / (๐ธ / 2))) |
128 | 127 | oveq1d 7322 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ก โ โ+) โ (((2
ยท ๐ต) / ๐ธ) + ((logโ2) / ๐ธ)) = ((๐ต / (๐ธ / 2)) + ((logโ2) / ๐ธ))) |
129 | 117, 128 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ก โ โ+) โ (๐ถ / ๐ธ) = ((๐ต / (๐ธ / 2)) + ((logโ2) / ๐ธ))) |
130 | 109, 129 | breqtrrd 5109 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ก โ โ+) โ ((๐ต / (๐ธ / 2)) + (logโ2)) โค (๐ถ / ๐ธ)) |
131 | | readdcl 11000 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ต / (๐ธ / 2)) โ โ โง (logโ2)
โ โ) โ ((๐ต
/ (๐ธ / 2)) + (logโ2))
โ โ) |
132 | 71, 59, 131 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ก โ โ+) โ ((๐ต / (๐ธ / 2)) + (logโ2)) โ
โ) |
133 | | efle 15872 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ต / (๐ธ / 2)) + (logโ2)) โ โ โง
(๐ถ / ๐ธ) โ โ) โ (((๐ต / (๐ธ / 2)) + (logโ2)) โค (๐ถ / ๐ธ) โ (expโ((๐ต / (๐ธ / 2)) + (logโ2))) โค
(expโ(๐ถ / ๐ธ)))) |
134 | 132, 63, 133 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ก โ โ+) โ (((๐ต / (๐ธ / 2)) + (logโ2)) โค (๐ถ / ๐ธ) โ (expโ((๐ต / (๐ธ / 2)) + (logโ2))) โค
(expโ(๐ถ / ๐ธ)))) |
135 | 130, 134 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ก โ โ+) โ
(expโ((๐ต / (๐ธ / 2)) + (logโ2))) โค
(expโ(๐ถ / ๐ธ))) |
136 | 84, 135 | eqbrtrrd 5105 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ก โ โ+) โ
((expโ(๐ต / (๐ธ / 2))) ยท 2) โค
(expโ(๐ถ / ๐ธ))) |
137 | 136 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ ((expโ(๐ต / (๐ธ / 2))) ยท 2) โค (expโ(๐ถ / ๐ธ))) |
138 | 66 | simplbda 501 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ (expโ(๐ถ / ๐ธ)) โค ๐) |
139 | 75, 76, 67, 137, 138 | letrd 11178 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ ((expโ(๐ต / (๐ธ / 2))) ยท 2) โค ๐) |
140 | 72 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ (expโ(๐ต / (๐ธ / 2))) โ โ) |
141 | | rpregt0 12790 |
. . . . . . . . . . . . . . 15
โข (2 โ
โ+ โ (2 โ โ โง 0 < 2)) |
142 | 57, 141 | mp1i 13 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ (2 โ โ
โง 0 < 2)) |
143 | | lemuldiv 11901 |
. . . . . . . . . . . . . 14
โข
(((expโ(๐ต /
(๐ธ / 2))) โ โ
โง ๐ โ โ
โง (2 โ โ โง 0 < 2)) โ (((expโ(๐ต / (๐ธ / 2))) ยท 2) โค ๐ โ (expโ(๐ต / (๐ธ / 2))) โค (๐ / 2))) |
144 | 140, 67, 142, 143 | syl3anc 1371 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ (((expโ(๐ต / (๐ธ / 2))) ยท 2) โค ๐ โ (expโ(๐ต / (๐ธ / 2))) โค (๐ / 2))) |
145 | 139, 144 | mpbid 231 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ (expโ(๐ต / (๐ธ / 2))) โค (๐ / 2)) |
146 | 69, 145 | eqbrtrid 5116 |
. . . . . . . . . . 11
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ ๐พ โค (๐ / 2)) |
147 | 69, 140 | eqeltrid 2841 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ ๐พ โ โ) |
148 | | elicopnf 13223 |
. . . . . . . . . . . 12
โข (๐พ โ โ โ ((๐ / 2) โ (๐พ[,)+โ) โ ((๐ / 2) โ โ โง ๐พ โค (๐ / 2)))) |
149 | 147, 148 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ ((๐ / 2) โ (๐พ[,)+โ) โ ((๐ / 2) โ โ โง ๐พ โค (๐ / 2)))) |
150 | 68, 146, 149 | mpbir2and 711 |
. . . . . . . . . 10
โข (((๐ โง ๐ก โ โ+) โง ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) โ (๐ / 2) โ (๐พ[,)+โ)) |
151 | 150 | adantrr 715 |
. . . . . . . . 9
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ (๐ / 2) โ (๐พ[,)+โ)) |
152 | 151 | adantlrr 719 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ (๐ / 2) โ (๐พ[,)+โ)) |
153 | 48, 50, 152 | rspcdva 3567 |
. . . . . . 7
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))) |
154 | | elioore 13155 |
. . . . . . . . . 10
โข (๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ) โ ๐ฆ โ โ) |
155 | 154 | ad2antll 727 |
. . . . . . . . 9
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ ๐ฆ โ โ) |
156 | 23 | rpred 12818 |
. . . . . . . . . . 11
โข ((๐ โง ๐ก โ โ+) โ ๐ โ
โ) |
157 | 156 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ ๐ โ โ) |
158 | 20 | reefcld 15842 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ก โ โ+) โ
(expโ(๐ก / (๐ธ / 4))) โ
โ) |
159 | 158, 156 | readdcld 11050 |
. . . . . . . . . . 11
โข ((๐ โง ๐ก โ โ+) โ
((expโ(๐ก / (๐ธ / 4))) + ๐) โ โ) |
160 | 159 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ ((expโ(๐ก / (๐ธ / 4))) + ๐) โ โ) |
161 | 156, 21 | ltaddrp2d 12852 |
. . . . . . . . . . 11
โข ((๐ โง ๐ก โ โ+) โ ๐ < ((expโ(๐ก / (๐ธ / 4))) + ๐)) |
162 | 161 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ ๐ < ((expโ(๐ก / (๐ธ / 4))) + ๐)) |
163 | | eliooord 13184 |
. . . . . . . . . . . 12
โข (๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ) โ (((expโ(๐ก / (๐ธ / 4))) + ๐) < ๐ฆ โง ๐ฆ < +โ)) |
164 | 163 | simpld 496 |
. . . . . . . . . . 11
โข (๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ) โ ((expโ(๐ก / (๐ธ / 4))) + ๐) < ๐ฆ) |
165 | 164 | ad2antll 727 |
. . . . . . . . . 10
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ ((expโ(๐ก / (๐ธ / 4))) + ๐) < ๐ฆ) |
166 | 157, 160,
155, 162, 165 | lttrd 11182 |
. . . . . . . . 9
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ ๐ < ๐ฆ) |
167 | 157 | rexrd 11071 |
. . . . . . . . . 10
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ ๐ โ
โ*) |
168 | | elioopnf 13221 |
. . . . . . . . . 10
โข (๐ โ โ*
โ (๐ฆ โ (๐(,)+โ) โ (๐ฆ โ โ โง ๐ < ๐ฆ))) |
169 | 167, 168 | syl 17 |
. . . . . . . . 9
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ (๐ฆ โ (๐(,)+โ) โ (๐ฆ โ โ โง ๐ < ๐ฆ))) |
170 | 155, 166,
169 | mpbir2and 711 |
. . . . . . . 8
โข (((๐ โง ๐ก โ โ+) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ ๐ฆ โ (๐(,)+โ)) |
171 | 170 | adantlrr 719 |
. . . . . . 7
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ ๐ฆ โ (๐(,)+โ)) |
172 | 42, 153, 171 | rspcdva 3567 |
. . . . . 6
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ โ๐ โ โ ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))) |
173 | | pntibnd.r |
. . . . . . . 8
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
174 | | pntibndlem1.1 |
. . . . . . . . 9
โข (๐ โ ๐ด โ
โ+) |
175 | 174 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ ๐ด โ
โ+) |
176 | | pntibndlem1.l |
. . . . . . . 8
โข ๐ฟ = ((1 / 4) / (๐ด + 3)) |
177 | | pntibndlem3.2 |
. . . . . . . . . 10
โข (๐ โ โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ด) |
178 | | fveq2 6804 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ฃ โ (๐
โ๐ฅ) = (๐
โ๐ฃ)) |
179 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ฃ โ ๐ฅ = ๐ฃ) |
180 | 178, 179 | oveq12d 7325 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ฃ โ ((๐
โ๐ฅ) / ๐ฅ) = ((๐
โ๐ฃ) / ๐ฃ)) |
181 | 180 | fveq2d 6808 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ฃ โ (absโ((๐
โ๐ฅ) / ๐ฅ)) = (absโ((๐
โ๐ฃ) / ๐ฃ))) |
182 | 181 | breq1d 5091 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ฃ โ ((absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ด โ (absโ((๐
โ๐ฃ) / ๐ฃ)) โค ๐ด)) |
183 | 182 | cbvralvw 3222 |
. . . . . . . . . 10
โข
(โ๐ฅ โ
โ+ (absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ด โ โ๐ฃ โ โ+
(absโ((๐
โ๐ฃ) / ๐ฃ)) โค ๐ด) |
184 | 177, 183 | sylib 217 |
. . . . . . . . 9
โข (๐ โ โ๐ฃ โ โ+
(absโ((๐
โ๐ฃ) / ๐ฃ)) โค ๐ด) |
185 | 184 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ โ๐ฃ โ โ+
(absโ((๐
โ๐ฃ) / ๐ฃ)) โค ๐ด) |
186 | 52 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ ๐ต โ
โ+) |
187 | 7 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ ๐ธ โ (0(,)1)) |
188 | 22 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ ๐ โ
โ+) |
189 | | simprrl 779 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ ๐ โ โ) |
190 | | simplrl 775 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ ๐ก โ โ+) |
191 | | simplrr 776 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ โ๐ฃ โ (1(,)+โ)โ๐ค โ (๐ฃ[,](2 ยท ๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ))))) |
192 | | eqid 2736 |
. . . . . . . 8
โข
((expโ(๐ก /
(๐ธ / 4))) + ๐) = ((expโ(๐ก / (๐ธ / 4))) + ๐) |
193 | | simprll 777 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)) |
194 | | simprlr 778 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) |
195 | | simprrr 780 |
. . . . . . . 8
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))) |
196 | 173, 175,
176, 185, 186, 69, 51, 187, 188, 189, 190, 191, 192, 193, 194, 195 | pntibndlem2 26784 |
. . . . . . 7
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง ((๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2))))) โ โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
197 | 196 | anassrs 469 |
. . . . . 6
โข ((((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โง (๐ โ โ โง ((๐ฆ < ๐ โง ๐ โค ((๐ / 2) ยท ๐ฆ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ธ / 2)))) โ โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
198 | 172, 197 | rexlimddv 3155 |
. . . . 5
โข (((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โง (๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ) โง ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ))) โ โ๐ง โ โ+
((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
199 | 198 | ralrimivva 3194 |
. . . 4
โข ((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โ โ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)โ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
200 | | oveq1 7314 |
. . . . . . 7
โข (๐ฅ = ((expโ(๐ก / (๐ธ / 4))) + ๐) โ (๐ฅ(,)+โ) = (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)) |
201 | 200 | raleqdv 3360 |
. . . . . 6
โข (๐ฅ = ((expโ(๐ก / (๐ธ / 4))) + ๐) โ (โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
202 | 201 | ralbidv 3171 |
. . . . 5
โข (๐ฅ = ((expโ(๐ก / (๐ธ / 4))) + ๐) โ (โ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)โ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
203 | 202 | rspcev 3566 |
. . . 4
โข
((((expโ(๐ก /
(๐ธ / 4))) + ๐) โ โ+
โง โ๐ โ
((expโ(๐ถ / ๐ธ))[,)+โ)โ๐ฆ โ (((expโ(๐ก / (๐ธ / 4))) + ๐)(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) โ โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
204 | 25, 199, 203 | syl2anc 585 |
. . 3
โข ((๐ โง (๐ก โ โ+ โง
โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))))) โ โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
205 | 204 | rexlimdvaa 3150 |
. 2
โข (๐ โ (โ๐ก โ โ+ โ๐ฃ โ
(1(,)+โ)โ๐ค
โ (๐ฃ[,](2 ยท
๐ฃ))((ฯโ๐ค) โ (ฯโ๐ฃ)) โค ((2 ยท (๐ค โ ๐ฃ)) + (๐ก ยท (๐ฃ / (logโ๐ฃ)))) โ โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
206 | 4, 205 | mpi 20 |
1
โข (๐ โ โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ถ / ๐ธ))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |