Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
โข (๐ โ โ+
โฆ ((ฯโ๐)
โ ๐)) = (๐ โ โ+
โฆ ((ฯโ๐)
โ ๐)) |
2 | 1 | pntrmax 27057 |
. 2
โข
โ๐ โ
โ+ โ๐ โ โ+
(absโ(((๐ โ
โ+ โฆ ((ฯโ๐) โ ๐))โ๐) / ๐)) โค ๐ |
3 | 1 | pntibnd 27086 |
. . . 4
โข
โ๐ โ
โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) |
4 | | simpll 766 |
. . . . . . 7
โข (((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โง ((๐ โ โ+ โง ๐ โ (0(,)1)) โง
โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) โ ๐ โ โ+) |
5 | | simplr 768 |
. . . . . . . 8
โข (((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โง ((๐ โ โ+ โง ๐ โ (0(,)1)) โง
โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) โ โ๐ โ โ+
(absโ(((๐ โ
โ+ โฆ ((ฯโ๐) โ ๐))โ๐) / ๐)) โค ๐) |
6 | | fveq2 6889 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ ((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) = ((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ฅ)) |
7 | | id 22 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ ๐ = ๐ฅ) |
8 | 6, 7 | oveq12d 7424 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ (((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐) = (((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ฅ) / ๐ฅ)) |
9 | 8 | fveq2d 6893 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) = (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ฅ) / ๐ฅ))) |
10 | 9 | breq1d 5158 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ ((absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐ โ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ฅ) / ๐ฅ)) โค ๐)) |
11 | 10 | cbvralvw 3235 |
. . . . . . . 8
โข
(โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐ โ โ๐ฅ โ โ+
(absโ(((๐ โ
โ+ โฆ ((ฯโ๐) โ ๐))โ๐ฅ) / ๐ฅ)) โค ๐) |
12 | 5, 11 | sylib 217 |
. . . . . . 7
โข (((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โง ((๐ โ โ+ โง ๐ โ (0(,)1)) โง
โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) โ โ๐ฅ โ โ+
(absโ(((๐ โ
โ+ โฆ ((ฯโ๐) โ ๐))โ๐ฅ) / ๐ฅ)) โค ๐) |
13 | | simprll 778 |
. . . . . . 7
โข (((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โง ((๐ โ โ+ โง ๐ โ (0(,)1)) โง
โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) โ ๐ โ โ+) |
14 | | simprlr 779 |
. . . . . . 7
โข (((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โง ((๐ โ โ+ โง ๐ โ (0(,)1)) โง
โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) โ ๐ โ (0(,)1)) |
15 | | eqid 2733 |
. . . . . . 7
โข (๐ + 1) = (๐ + 1) |
16 | | eqid 2733 |
. . . . . . 7
โข ((1
โ (1 / (๐ + 1)))
ยท ((๐ / (;32 ยท ๐)) / ((๐ + 1)โ2))) = ((1 โ (1 / (๐ + 1))) ยท ((๐ / (;32 ยท ๐)) / ((๐ + 1)โ2))) |
17 | | simprr 772 |
. . . . . . . 8
โข (((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โง ((๐ โ โ+ โง ๐ โ (0(,)1)) โง
โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) โ โ๐ โ (0(,)1)โ๐ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐)) |
18 | | breq2 5152 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = ๐ โ (๐ฆ < ๐ง โ ๐ฆ < ๐)) |
19 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง = ๐ โ ((1 + (๐ ยท ๐)) ยท ๐ง) = ((1 + (๐ ยท ๐)) ยท ๐)) |
20 | 19 | breq1d 5158 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = ๐ โ (((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ) โ ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐ฆ))) |
21 | 18, 20 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
โข (๐ง = ๐ โ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โ (๐ฆ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐ฆ)))) |
22 | | id 22 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง = ๐ โ ๐ง = ๐) |
23 | 22, 19 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = ๐ โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง)) = (๐[,]((1 + (๐ ยท ๐)) ยท ๐))) |
24 | 23 | raleqdv 3326 |
. . . . . . . . . . . . . . . 16
โข (๐ง = ๐ โ (โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐ โ โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐)) |
25 | 21, 24 | anbi12d 632 |
. . . . . . . . . . . . . . 15
โข (๐ง = ๐ โ (((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ ((๐ฆ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) |
26 | 25 | cbvrexvw 3236 |
. . . . . . . . . . . . . 14
โข
(โ๐ง โ
โ+ ((๐ฆ
< ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ โ+ ((๐ฆ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐)) |
27 | | breq1 5151 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ = ๐ โ (๐ฆ < ๐ โ ๐ < ๐)) |
28 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ = ๐ โ (๐ ยท ๐ฆ) = (๐ ยท ๐)) |
29 | 28 | breq2d 5160 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ = ๐ โ (((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐ฆ) โ ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐))) |
30 | 27, 29 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ = ๐ โ ((๐ฆ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐ฆ)) โ (๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)))) |
31 | 30 | anbi1d 631 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = ๐ โ (((๐ฆ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) |
32 | 31 | rexbidv 3179 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ๐ โ (โ๐ โ โ+ ((๐ฆ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) |
33 | 26, 32 | bitrid 283 |
. . . . . . . . . . . . 13
โข (๐ฆ = ๐ โ (โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) |
34 | 33 | cbvralvw 3235 |
. . . . . . . . . . . 12
โข
(โ๐ฆ โ
(๐(,)+โ)โ๐ง โ โ+
((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ (๐(,)+โ)โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐)) |
35 | | oveq1 7413 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (๐(,)+โ) = (๐ฅ(,)+โ)) |
36 | 35 | raleqdv 3326 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ (โ๐ โ (๐(,)+โ)โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ (๐ฅ(,)+โ)โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) |
37 | 34, 36 | bitrid 283 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ (โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ (๐ฅ(,)+โ)โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) |
38 | 37 | ralbidv 3178 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ โ (๐ฅ(,)+โ)โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) |
39 | 38 | cbvrexvw 3236 |
. . . . . . . . 9
โข
(โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ โ (๐ฅ(,)+โ)โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐)) |
40 | 39 | ralbii 3094 |
. . . . . . . 8
โข
(โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ โ (๐ฅ(,)+โ)โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐)) |
41 | 17, 40 | sylib 217 |
. . . . . . 7
โข (((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โง ((๐ โ โ+ โง ๐ โ (0(,)1)) โง
โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ โ (๐ฅ(,)+โ)โ๐ โ โ+ ((๐ < ๐ โง ((1 + (๐ ยท ๐)) ยท ๐) < (๐ ยท ๐)) โง โ๐ข โ (๐[,]((1 + (๐ ยท ๐)) ยท ๐))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐)) |
42 | 1, 4, 12, 13, 14, 15, 16, 41 | pntleml 27104 |
. . . . . 6
โข (((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โง ((๐ โ โ+ โง ๐ โ (0(,)1)) โง
โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐))) โ (๐ฅ โ โ+ โฆ
((ฯโ๐ฅ) / ๐ฅ)) โ๐
1) |
43 | 42 | expr 458 |
. . . . 5
โข (((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โง (๐ โ โ+ โง ๐ โ (0(,)1))) โ
(โ๐ โ
(0(,)1)โ๐ โ
โ+ โ๐ โ ((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ (๐ฅ โ โ+ โฆ
((ฯโ๐ฅ) / ๐ฅ)) โ๐
1)) |
44 | 43 | rexlimdvva 3212 |
. . . 4
โข ((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โ (โ๐ โ โ+ โ๐ โ (0(,)1)โ๐ โ (0(,)1)โ๐ โ โ+
โ๐ โ
((expโ(๐ / ๐))[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ ยท ๐)) ยท ๐ง))(absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐ข) / ๐ข)) โค ๐) โ (๐ฅ โ โ+ โฆ
((ฯโ๐ฅ) / ๐ฅ)) โ๐
1)) |
45 | 3, 44 | mpi 20 |
. . 3
โข ((๐ โ โ+
โง โ๐ โ
โ+ (absโ(((๐ โ โ+ โฆ
((ฯโ๐) โ
๐))โ๐) / ๐)) โค ๐) โ (๐ฅ โ โ+ โฆ
((ฯโ๐ฅ) / ๐ฅ)) โ๐
1) |
46 | 45 | rexlimiva 3148 |
. 2
โข
(โ๐ โ
โ+ โ๐ โ โ+
(absโ(((๐ โ
โ+ โฆ ((ฯโ๐) โ ๐))โ๐) / ๐)) โค ๐ โ (๐ฅ โ โ+ โฆ
((ฯโ๐ฅ) / ๐ฅ)) โ๐
1) |
47 | 2, 46 | ax-mp 5 |
1
โข (๐ฅ โ โ+
โฆ ((ฯโ๐ฅ) /
๐ฅ))
โ๐ 1 |