Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . 3
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
2 | 1 | pntrmax 27447 |
. 2
โข
โ๐ โ
โ+ โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ |
3 | 1 | pntpbnd 27471 |
. 2
โข
โ๐ โ
โ+ โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) |
4 | | reeanv 3220 |
. . 3
โข
(โ๐ โ
โ+ โ๐ โ โ+ (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐)) โ (โ๐ โ โ+ โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) |
5 | | 2rp 12982 |
. . . . . . . . 9
โข 2 โ
โ+ |
6 | | rpmulcl 13000 |
. . . . . . . . 9
โข ((2
โ โ+ โง ๐ โ โ+) โ (2
ยท ๐) โ
โ+) |
7 | 5, 6 | mpan 687 |
. . . . . . . 8
โข (๐ โ โ+
โ (2 ยท ๐)
โ โ+) |
8 | | 2re 12287 |
. . . . . . . . 9
โข 2 โ
โ |
9 | | 1lt2 12384 |
. . . . . . . . 9
โข 1 <
2 |
10 | | rplogcl 26488 |
. . . . . . . . 9
โข ((2
โ โ โง 1 < 2) โ (logโ2) โ
โ+) |
11 | 8, 9, 10 | mp2an 689 |
. . . . . . . 8
โข
(logโ2) โ โ+ |
12 | | rpaddcl 12999 |
. . . . . . . 8
โข (((2
ยท ๐) โ
โ+ โง (logโ2) โ โ+) โ ((2
ยท ๐) +
(logโ2)) โ โ+) |
13 | 7, 11, 12 | sylancl 585 |
. . . . . . 7
โข (๐ โ โ+
โ ((2 ยท ๐) +
(logโ2)) โ โ+) |
14 | 13 | ad2antlr 724 |
. . . . . 6
โข (((๐ โ โ+
โง ๐ โ
โ+) โง (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) โ ((2 ยท ๐) + (logโ2)) โ
โ+) |
15 | | id 22 |
. . . . . . . 8
โข (๐ โ โ+
โ ๐ โ
โ+) |
16 | | eqid 2726 |
. . . . . . . 8
โข ((1 / 4)
/ (๐ + 3)) = ((1 / 4) /
(๐ + 3)) |
17 | 1, 15, 16 | pntibndlem1 27472 |
. . . . . . 7
โข (๐ โ โ+
โ ((1 / 4) / (๐ + 3))
โ (0(,)1)) |
18 | 17 | ad2antrr 723 |
. . . . . 6
โข (((๐ โ โ+
โง ๐ โ
โ+) โง (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) โ ((1 / 4) / (๐ + 3)) โ (0(,)1)) |
19 | | elioore 13357 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0(,)1) โ ๐ โ
โ) |
20 | | eliooord 13386 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (0(,)1) โ (0 <
๐ โง ๐ < 1)) |
21 | 20 | simpld 494 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0(,)1) โ 0 <
๐) |
22 | 19, 21 | elrpd 13016 |
. . . . . . . . . . . . . 14
โข (๐ โ (0(,)1) โ ๐ โ
โ+) |
23 | 22 | rphalfcld 13031 |
. . . . . . . . . . . . 13
โข (๐ โ (0(,)1) โ (๐ / 2) โ
โ+) |
24 | 23 | rpred 13019 |
. . . . . . . . . . . 12
โข (๐ โ (0(,)1) โ (๐ / 2) โ
โ) |
25 | 23 | rpgt0d 13022 |
. . . . . . . . . . . 12
โข (๐ โ (0(,)1) โ 0 <
(๐ / 2)) |
26 | | 1red 11216 |
. . . . . . . . . . . . 13
โข (๐ โ (0(,)1) โ 1 โ
โ) |
27 | | rphalflt 13006 |
. . . . . . . . . . . . . 14
โข (๐ โ โ+
โ (๐ / 2) < ๐) |
28 | 22, 27 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (0(,)1) โ (๐ / 2) < ๐) |
29 | 20 | simprd 495 |
. . . . . . . . . . . . 13
โข (๐ โ (0(,)1) โ ๐ < 1) |
30 | 24, 19, 26, 28, 29 | lttrd 11376 |
. . . . . . . . . . . 12
โข (๐ โ (0(,)1) โ (๐ / 2) < 1) |
31 | | 0xr 11262 |
. . . . . . . . . . . . 13
โข 0 โ
โ* |
32 | | 1xr 11274 |
. . . . . . . . . . . . 13
โข 1 โ
โ* |
33 | | elioo2 13368 |
. . . . . . . . . . . . 13
โข ((0
โ โ* โง 1 โ โ*) โ ((๐ / 2) โ (0(,)1) โ
((๐ / 2) โ โ
โง 0 < (๐ / 2) โง
(๐ / 2) <
1))) |
34 | 31, 32, 33 | mp2an 689 |
. . . . . . . . . . . 12
โข ((๐ / 2) โ (0(,)1) โ
((๐ / 2) โ โ
โง 0 < (๐ / 2) โง
(๐ / 2) <
1)) |
35 | 24, 25, 30, 34 | syl3anbrc 1340 |
. . . . . . . . . . 11
โข (๐ โ (0(,)1) โ (๐ / 2) โ
(0(,)1)) |
36 | 35 | adantl 481 |
. . . . . . . . . 10
โข ((((๐ โ โ+
โง ๐ โ
โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โ (๐ / 2) โ (0(,)1)) |
37 | | oveq2 7412 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ / 2) โ (๐ / ๐) = (๐ / (๐ / 2))) |
38 | 37 | fveq2d 6888 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ / 2) โ (expโ(๐ / ๐)) = (expโ(๐ / (๐ / 2)))) |
39 | 38 | oveq1d 7419 |
. . . . . . . . . . . . 13
โข (๐ = (๐ / 2) โ ((expโ(๐ / ๐))[,)+โ) = ((expโ(๐ / (๐ / 2)))[,)+โ)) |
40 | | breq2 5145 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ / 2) โ ((absโ((๐
โ๐) / ๐)) โค ๐ โ (absโ((๐
โ๐) / ๐)) โค (๐ / 2))) |
41 | 40 | anbi2d 628 |
. . . . . . . . . . . . . . 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 3336 |
. . . . . . . . . . . 12
โข (๐ = (๐ / 2) โ (โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ โ ((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) |
45 | 44 | rexbidv 3172 |
. . . . . . . . . . 11
โข (๐ = (๐ / 2) โ (โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐) โ โ๐ โ โ+ โ๐ โ ((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) |
46 | 45 | rspcv 3602 |
. . . . . . . . . 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 780 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ ๐ โ โ+) |
49 | | simpllr 773 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) |
50 | | simplr 766 |
. . . . . . . . . . . 12
โข (((๐ โ โ+
โง ๐ โ
โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โ ๐ โ โ+) |
51 | 50 | ad2antrr 723 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ ๐ โ โ+) |
52 | | eqid 2726 |
. . . . . . . . . . 11
โข
(expโ(๐ /
(๐ / 2))) =
(expโ(๐ / (๐ / 2))) |
53 | | eqid 2726 |
. . . . . . . . . . 11
โข ((2
ยท ๐) +
(logโ2)) = ((2 ยท ๐) + (logโ2)) |
54 | | simplr 766 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ ๐ โ (0(,)1)) |
55 | | simprl 768 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ ๐ โ โ+) |
56 | | simprr 770 |
. . . . . . . . . . 11
โข
(((((๐ โ
โ+ โง ๐
โ โ+) โง โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐) โง ๐ โ (0(,)1)) โง (๐ โ โ+ โง
โ๐ โ
((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2)))) โ โ๐ โ ((expโ(๐ / (๐ / 2)))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค (๐ / 2))) |
57 | 1, 48, 16, 49, 51, 52, 53, 54, 55, 56 | pntibndlem3 27475 |
. . . . . . . . . 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 454 |
. . . . . 6
โข (((๐ โ โ+
โง ๐ โ
โ+) โง (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(((2
ยท ๐) +
(logโ2)) / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
62 | | fvoveq1 7427 |
. . . . . . . . . . 11
โข (๐ = ((2 ยท ๐) + (logโ2)) โ
(expโ(๐ / ๐)) = (expโ(((2 ยท
๐) + (logโ2)) / ๐))) |
63 | 62 | oveq1d 7419 |
. . . . . . . . . 10
โข (๐ = ((2 ยท ๐) + (logโ2)) โ
((expโ(๐ / ๐))[,)+โ) =
((expโ(((2 ยท ๐) + (logโ2)) / ๐))[,)+โ)) |
64 | 63 | raleqdv 3319 |
. . . . . . . . 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 7411 |
. . . . . . . . . . . . . . . 16
โข (๐ = ((1 / 4) / (๐ + 3)) โ (๐ ยท ๐) = (((1 / 4) / (๐ + 3)) ยท ๐)) |
68 | 67 | oveq2d 7420 |
. . . . . . . . . . . . . . 15
โข (๐ = ((1 / 4) / (๐ + 3)) โ (1 + (๐ ยท ๐)) = (1 + (((1 / 4) / (๐ + 3)) ยท ๐))) |
69 | 68 | oveq1d 7419 |
. . . . . . . . . . . . . 14
โข (๐ = ((1 / 4) / (๐ + 3)) โ ((1 + (๐ ยท ๐)) ยท ๐ง) = ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง)) |
70 | 69 | breq1d 5151 |
. . . . . . . . . . . . 13
โข (๐ = ((1 / 4) / (๐ + 3)) โ (((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ) โ ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ))) |
71 | 70 | anbi2d 628 |
. . . . . . . . . . . 12
โข (๐ = ((1 / 4) / (๐ + 3)) โ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โ (๐ฆ < ๐ง โง ((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)))) |
72 | 69 | oveq2d 7420 |
. . . . . . . . . . . . 13
โข (๐ = ((1 / 4) / (๐ + 3)) โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง)) = (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))) |
73 | 72 | raleqdv 3319 |
. . . . . . . . . . . 12
โข (๐ = ((1 / 4) / (๐ + 3)) โ (โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ โ โ๐ข โ (๐ง[,]((1 + (((1 / 4) / (๐ + 3)) ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
74 | 71, 73 | anbi12d 630 |
. . . . . . . . . . 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 3214 |
. . . . . . . 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 3619 |
. . . . . 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 1368 |
. . . . 5
โข (((๐ โ โ+
โง ๐ โ
โ+) โง (โ๐ฅ โ โ+
(absโ((๐
โ๐ฅ) / ๐ฅ)) โค ๐ โง โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฃ โ (๐(,)+โ)โ๐ โ โ ((๐ฃ < ๐ โง ๐ โค (๐ ยท ๐ฃ)) โง (absโ((๐
โ๐) / ๐)) โค ๐))) โ โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ฅ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
81 | 80 | ex 412 |
. . . 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 689 |
1
โข
โ๐ โ
โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) |