Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . 3
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
2 | 1 | pntrmax 26928 |
. 2
โข
โ๐ โ
โ+ โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ |
3 | 1 | pntpbnd 26952 |
. 2
โข
โ๐ โ
โ+ โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) |
4 | | reeanv 3216 |
. . 3
โข
(โ๐ โ
โ+ โ๐ โ โ+ (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐)) โ (โ๐ โ โ+ โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) |
5 | | 2rp 12925 |
. . . . . . . . 9
โข 2 โ
โ+ |
6 | | rpmulcl 12943 |
. . . . . . . . 9
โข ((2
โ โ+ โง ๐ โ โ+) โ (2
ยท ๐) โ
โ+) |
7 | 5, 6 | mpan 689 |
. . . . . . . 8
โข (๐ โ โ+
โ (2 ยท ๐)
โ โ+) |
8 | | 2re 12232 |
. . . . . . . . 9
โข 2 โ
โ |
9 | | 1lt2 12329 |
. . . . . . . . 9
โข 1 <
2 |
10 | | rplogcl 25975 |
. . . . . . . . 9
โข ((2
โ โ โง 1 < 2) โ (logโ2) โ
โ+) |
11 | 8, 9, 10 | mp2an 691 |
. . . . . . . 8
โข
(logโ2) โ โ+ |
12 | | rpaddcl 12942 |
. . . . . . . 8
โข (((2
ยท ๐) โ
โ+ โง (logโ2) โ โ+) โ ((2
ยท ๐) +
(logโ2)) โ โ+) |
13 | 7, 11, 12 | sylancl 587 |
. . . . . . 7
โข (๐ โ โ+
โ ((2 ยท ๐) +
(logโ2)) โ โ+) |
14 | 13 | ad2antlr 726 |
. . . . . 6
โข (((๐ โ โ+
โง ๐ โ
โ+) โง (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) โ ((2 ยท ๐) + (logโ2)) โ
โ+) |
15 | | id 22 |
. . . . . . . 8
โข (๐ โ โ+
โ ๐ โ
โ+) |
16 | | eqid 2733 |
. . . . . . . 8
โข ((1 / 4)
/ (๐ + 3)) = ((1 / 4) /
(๐ + 3)) |
17 | 1, 15, 16 | pntibndlem1 26953 |
. . . . . . 7
โข (๐ โ โ+
โ ((1 / 4) / (๐ + 3))
โ (0(,)1)) |
18 | 17 | ad2antrr 725 |
. . . . . 6
โข (((๐ โ โ+
โง ๐ โ
โ+) โง (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) โ ((1 / 4) / (๐ + 3)) โ (0(,)1)) |
19 | | elioore 13300 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0(,)1) โ ๐ โ
โ) |
20 | | eliooord 13329 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (0(,)1) โ (0 <
๐ โง ๐ < 1)) |
21 | 20 | simpld 496 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0(,)1) โ 0 <
๐) |
22 | 19, 21 | elrpd 12959 |
. . . . . . . . . . . . . 14
โข (๐ โ (0(,)1) โ ๐ โ
โ+) |
23 | 22 | rphalfcld 12974 |
. . . . . . . . . . . . 13
โข (๐ โ (0(,)1) โ (๐ / 2) โ
โ+) |
24 | 23 | rpred 12962 |
. . . . . . . . . . . 12
โข (๐ โ (0(,)1) โ (๐ / 2) โ
โ) |
25 | 23 | rpgt0d 12965 |
. . . . . . . . . . . 12
โข (๐ โ (0(,)1) โ 0 <
(๐ / 2)) |
26 | | 1red 11161 |
. . . . . . . . . . . . 13
โข (๐ โ (0(,)1) โ 1 โ
โ) |
27 | | rphalflt 12949 |
. . . . . . . . . . . . . 14
โข (๐ โ โ+
โ (๐ / 2) < ๐) |
28 | 22, 27 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (0(,)1) โ (๐ / 2) < ๐) |
29 | 20 | simprd 497 |
. . . . . . . . . . . . 13
โข (๐ โ (0(,)1) โ ๐ < 1) |
30 | 24, 19, 26, 28, 29 | lttrd 11321 |
. . . . . . . . . . . 12
โข (๐ โ (0(,)1) โ (๐ / 2) < 1) |
31 | | 0xr 11207 |
. . . . . . . . . . . . 13
โข 0 โ
โ* |
32 | | 1xr 11219 |
. . . . . . . . . . . . 13
โข 1 โ
โ* |
33 | | elioo2 13311 |
. . . . . . . . . . . . 13
โข ((0
โ โ* โง 1 โ โ*) โ ((๐ / 2) โ (0(,)1) โ
((๐ / 2) โ โ
โง 0 < (๐ / 2) โง
(๐ / 2) <
1))) |
34 | 31, 32, 33 | mp2an 691 |
. . . . . . . . . . . 12
โข ((๐ / 2) โ (0(,)1) โ
((๐ / 2) โ โ
โง 0 < (๐ / 2) โง
(๐ / 2) <
1)) |
35 | 24, 25, 30, 34 | syl3anbrc 1344 |
. . . . . . . . . . 11
โข (๐ โ (0(,)1) โ (๐ / 2) โ
(0(,)1)) |
36 | 35 | adantl 483 |
. . . . . . . . . 10
โข ((((๐ โ โ+
โง ๐ โ
โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โ (๐ / 2) โ (0(,)1)) |
37 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ / 2) โ (๐ / ๐) = (๐ / (๐ / 2))) |
38 | 37 | fveq2d 6847 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ / 2) โ (expโ(๐ / ๐)) = (expโ(๐ / (๐ / 2)))) |
39 | 38 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ = (๐ / 2) โ ((expโ(๐ / ๐))[,)+โ) = ((expโ(๐ / (๐ / 2)))[,)+โ)) |
40 | | breq2 5110 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ / 2) โ ((absโ((๐
โ๐) / ๐)) โค ๐ โ (absโ((๐
โ๐) / ๐)) โค (๐ / 2))) |
41 | 40 | anbi2d 630 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ / 2) โ (((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) |
42 | 41 | rexbidv 3172 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ / 2) โ (โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) |
43 | 42 | ralbidv 3171 |
. . . . . . . . . . . . 13
โข (๐ = (๐ / 2) โ (โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) |
44 | 39, 43 | raleqbidv 3318 |
. . . . . . . . . . . 12
โข (๐ = (๐ / 2) โ (โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ โ ((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) |
45 | 44 | rexbidv 3172 |
. . . . . . . . . . 11
โข (๐ = (๐ / 2) โ (โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ โ โ+ โ๐ โ ((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) |
46 | 45 | rspcv 3576 |
. . . . . . . . . 10
โข ((๐ / 2) โ (0(,)1) โ
(โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ โ โ+ โ๐ โ ((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) |
47 | 36, 46 | syl 17 |
. . . . . . . . 9
โข ((((๐ โ โ+
โง ๐ โ
โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โ (โ๐ โ (0(,)1)โ๐ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ โ โ+ โ๐ โ ((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) |
48 | | simp-4l 782 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ ๐ โ โ+) |
49 | | simpllr 775 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) |
50 | | simplr 768 |
. . . . . . . . . . . 12
โข (((๐ โ โ+
โง ๐ โ
โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โ ๐ โ โ+) |
51 | 50 | ad2antrr 725 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ ๐ โ โ+) |
52 | | eqid 2733 |
. . . . . . . . . . 11
โข
(expโ(๐ /
(๐ / 2))) =
(expโ(๐ / (๐ / 2))) |
53 | | eqid 2733 |
. . . . . . . . . . 11
โข ((2
ยท ๐) +
(logโ2)) = ((2 ยท ๐) + (logโ2)) |
54 | | simplr 768 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ ๐ โ (0(,)1)) |
55 | | simprl 770 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ ๐ โ โ+) |
56 | | simprr 772 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ โ๐ โ ((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2))) |
57 | 1, 48, 16, 49, 51, 52, 53, 54, 55, 56 | pntibndlem3 26956 |
. . . . . . . . . 10
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
58 | 57 | rexlimdvaa 3150 |
. . . . . . . . 9
โข ((((๐ โ โ+
โง ๐ โ
โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โ (โ๐ โ โ+
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)) โ โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
59 | 47, 58 | syld 47 |
. . . . . . . 8
โข ((((๐ โ โ+
โง ๐ โ
โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โ (โ๐ โ (0(,)1)โ๐ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
60 | 59 | ralrimdva 3148 |
. . . . . . 7
โข (((๐ โ โ+
โง ๐ โ
โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โ (โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
61 | 60 | impr 456 |
. . . . . 6
โข (((๐ โ โ+
โง ๐ โ
โ+) โง (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
62 | | fvoveq1 7381 |
. . . . . . . . . . 11
โข (๐ = ((2 ยท ๐) + (logโ2)) โ
(expโ(๐ / ๐)) = (expโ(((2 ยท
๐) + (logโ2)) / ๐))) |
63 | 62 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ = ((2 ยท ๐) + (logโ2)) โ
((expโ(๐ / ๐))[,)+โ) =
((expโ(((2 ยท ๐) + (logโ2)) / ๐))[,)+โ)) |
64 | 63 | raleqdv 3312 |
. . . . . . . . 9
โข (๐ = ((2 ยท ๐) + (logโ2)) โ
(โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ ((expโ(((2 ยท ๐) + (logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
65 | 64 | rexbidv 3172 |
. . . . . . . 8
โข (๐ = ((2 ยท ๐) + (logโ2)) โ
(โ๐ฅ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
66 | 65 | ralbidv 3171 |
. . . . . . 7
โข (๐ = ((2 ยท ๐) + (logโ2)) โ
(โ๐ โ
(0(,)1)โ๐ฅ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
67 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
โข (๐ = ((1 / 4) / (๐ + 3)) โ (๐ ยท ๐) = (((1 / 4) / (๐ + 3)) ยท ๐)) |
68 | 67 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
โข (๐ = ((1 / 4) / (๐ + 3)) โ (1 + (๐ ยท ๐)) = (1 + (((1 / 4) / (๐ + 3)) ยท ๐))) |
69 | 68 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ = ((1 / 4) / (๐ + 3)) โ ((1 + (๐ ยท ๐)) ยท ๐ง) = ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง)) |
70 | 69 | breq1d 5116 |
. . . . . . . . . . . . 13
โข (๐ = ((1 / 4) / (๐ + 3)) โ (((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ) โ ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ))) |
71 | 70 | anbi2d 630 |
. . . . . . . . . . . 12
โข (๐ = ((1 / 4) / (๐ + 3)) โ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โ (๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)))) |
72 | 69 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (๐ = ((1 / 4) / (๐ + 3)) โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง)) = (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))) |
73 | 72 | raleqdv 3312 |
. . . . . . . . . . . 12
โข (๐ = ((1 / 4) / (๐ + 3)) โ (โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ โ โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
74 | 71, 73 | anbi12d 632 |
. . . . . . . . . . 11
โข (๐ = ((1 / 4) / (๐ + 3)) โ (((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
75 | 74 | rexbidv 3172 |
. . . . . . . . . 10
โข (๐ = ((1 / 4) / (๐ + 3)) โ (โ๐ง โ โ+
((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
76 | 75 | ralbidv 3171 |
. . . . . . . . 9
โข (๐ = ((1 / 4) / (๐ + 3)) โ (โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
77 | 76 | rexralbidv 3211 |
. . . . . . . 8
โข (๐ = ((1 / 4) / (๐ + 3)) โ (โ๐ฅ โ โ+
โ๐ โ
((expโ(((2 ยท ๐) + (logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
78 | 77 | ralbidv 3171 |
. . . . . . 7
โข (๐ = ((1 / 4) / (๐ + 3)) โ (โ๐ โ (0(,)1)โ๐ฅ โ โ+
โ๐ โ
((expโ(((2 ยท ๐) + (logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
79 | 66, 78 | rspc2ev 3591 |
. . . . . 6
โข ((((2
ยท ๐) +
(logโ2)) โ โ+ โง ((1 / 4) / (๐ + 3)) โ (0(,)1) โง โ๐ โ (0(,)1)โ๐ฅ โ โ+
โ๐ โ
((expโ(((2 ยท ๐) + (logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) โ โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ฅ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
80 | 14, 18, 61, 79 | syl3anc 1372 |
. . . . 5
โข (((๐ โ โ+
โง ๐ โ
โ+) โง (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) โ โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ฅ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
81 | 80 | ex 414 |
. . . 4
โข ((๐ โ โ+
โง ๐ โ
โ+) โ ((โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐)) โ โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ฅ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐))) |
82 | 81 | rexlimivv 3193 |
. . 3
โข
(โ๐ โ
โ+ โ๐ โ โ+ (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐)) โ โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ฅ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
83 | 4, 82 | sylbir 234 |
. 2
โข
((โ๐ โ
โ+ โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐)) โ โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ฅ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
84 | 2, 3, 83 | mp2an 691 |
1
โข
โ๐ โ
โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) |