Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ๐ธ โ (๐ต / ๐) = (๐ต / ๐ธ)) |
2 | 1 | fveq2d 6847 |
. . . . . . . 8
โข (๐ = ๐ธ โ (expโ(๐ต / ๐)) = (expโ(๐ต / ๐ธ))) |
3 | | pntlemp.k |
. . . . . . . 8
โข ๐พ = (expโ(๐ต / ๐ธ)) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . 7
โข (๐ = ๐ธ โ (expโ(๐ต / ๐)) = ๐พ) |
5 | 4 | oveq1d 7373 |
. . . . . 6
โข (๐ = ๐ธ โ ((expโ(๐ต / ๐))[,)+โ) = (๐พ[,)+โ)) |
6 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ = ๐ธ โ (๐ฟ ยท ๐) = (๐ฟ ยท ๐ธ)) |
7 | 6 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ = ๐ธ โ (1 + (๐ฟ ยท ๐)) = (1 + (๐ฟ ยท ๐ธ))) |
8 | 7 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ = ๐ธ โ ((1 + (๐ฟ ยท ๐)) ยท ๐ง) = ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง)) |
9 | 8 | breq1d 5116 |
. . . . . . . . . 10
โข (๐ = ๐ธ โ (((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ) โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ))) |
10 | 9 | anbi2d 630 |
. . . . . . . . 9
โข (๐ = ๐ธ โ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โ (๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)))) |
11 | 8 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ธ โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง)) = (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))) |
12 | | breq2 5110 |
. . . . . . . . . 10
โข (๐ = ๐ธ โ ((absโ((๐
โ๐ข) / ๐ข)) โค ๐ โ (absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
13 | 11, 12 | raleqbidv 3318 |
. . . . . . . . 9
โข (๐ = ๐ธ โ (โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ โ โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
14 | 10, 13 | anbi12d 632 |
. . . . . . . 8
โข (๐ = ๐ธ โ (((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
15 | 14 | rexbidv 3172 |
. . . . . . 7
โข (๐ = ๐ธ โ (โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
16 | 15 | ralbidv 3171 |
. . . . . 6
โข (๐ = ๐ธ โ (โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
17 | 5, 16 | raleqbidv 3318 |
. . . . 5
โข (๐ = ๐ธ โ (โ๐ โ ((expโ(๐ต / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
18 | 17 | rexbidv 3172 |
. . . 4
โข (๐ = ๐ธ โ (โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ต / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ฅ โ โ+ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
19 | | oveq1 7365 |
. . . . . . 7
โข (๐ฅ = ๐ก โ (๐ฅ(,)+โ) = (๐ก(,)+โ)) |
20 | 19 | raleqdv 3312 |
. . . . . 6
โข (๐ฅ = ๐ก โ (โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
21 | 20 | ralbidv 3171 |
. . . . 5
โข (๐ฅ = ๐ก โ (โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
22 | 21 | cbvrexvw 3225 |
. . . 4
โข
(โ๐ฅ โ
โ+ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ก โ โ+ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
23 | 18, 22 | bitrdi 287 |
. . 3
โข (๐ = ๐ธ โ (โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ต / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐) โ โ๐ก โ โ+ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
24 | | pntlemp.K |
. . 3
โข (๐ โ โ๐ โ (0(,)1)โ๐ฅ โ โ+ โ๐ โ ((expโ(๐ต / ๐))[,)+โ)โ๐ฆ โ (๐ฅ(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐)) |
25 | | pntlem3.r |
. . . . . 6
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
26 | | pntlem3.a |
. . . . . 6
โข (๐ โ ๐ด โ
โ+) |
27 | | pntlemp.b |
. . . . . 6
โข (๐ โ ๐ต โ
โ+) |
28 | | pntlemp.l |
. . . . . 6
โข (๐ โ ๐ฟ โ (0(,)1)) |
29 | | pntlemp.d |
. . . . . 6
โข ๐ท = (๐ด + 1) |
30 | | pntlemp.f |
. . . . . 6
โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) |
31 | | pntlemp.u |
. . . . . 6
โข (๐ โ ๐ โ
โ+) |
32 | | pntlemp.u2 |
. . . . . 6
โข (๐ โ ๐ โค ๐ด) |
33 | | pntlemp.e |
. . . . . 6
โข ๐ธ = (๐ / ๐ท) |
34 | 25, 26, 27, 28, 29, 30, 31, 32, 33, 3 | pntlemc 26959 |
. . . . 5
โข (๐ โ (๐ธ โ โ+ โง ๐พ โ โ+
โง (๐ธ โ (0(,)1)
โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+))) |
35 | 34 | simp3d 1145 |
. . . 4
โข (๐ โ (๐ธ โ (0(,)1) โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+)) |
36 | 35 | simp1d 1143 |
. . 3
โข (๐ โ ๐ธ โ (0(,)1)) |
37 | 23, 24, 36 | rspcdva 3581 |
. 2
โข (๐ โ โ๐ก โ โ+ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
38 | | pntlemp.y |
. . . . 5
โข (๐ โ (๐ โ โ+ โง 1 โค
๐)) |
39 | 38 | simpld 496 |
. . . 4
โข (๐ โ ๐ โ
โ+) |
40 | 39 | rpred 12962 |
. . 3
โข (๐ โ ๐ โ โ) |
41 | 38 | simprd 497 |
. . 3
โข (๐ โ 1 โค ๐) |
42 | 25 | pntrlog2bnd 26948 |
. . 3
โข ((๐ โ โ โง 1 โค
๐) โ โ๐ โ โ+
โ๐ง โ
(1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐) |
43 | 40, 41, 42 | syl2anc 585 |
. 2
โข (๐ โ โ๐ โ โ+ โ๐ง โ
(1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐) |
44 | | reeanv 3216 |
. . 3
โข
(โ๐ก โ
โ+ โ๐ โ โ+ (โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐) โ (โ๐ก โ โ+ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ โ โ+ โ๐ง โ
(1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐)) |
45 | 26 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ ๐ด โ
โ+) |
46 | 27 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ ๐ต โ
โ+) |
47 | 28 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ ๐ฟ โ (0(,)1)) |
48 | 31 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ ๐ โ
โ+) |
49 | 32 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ ๐ โค ๐ด) |
50 | 38 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ (๐ โ โ+ โง 1 โค
๐)) |
51 | | simpl 484 |
. . . . . . . . 9
โข ((๐ก โ โ+
โง ๐ โ
โ+) โ ๐ก โ โ+) |
52 | | rpaddcl 12942 |
. . . . . . . . 9
โข ((๐ โ โ+
โง ๐ก โ
โ+) โ (๐ + ๐ก) โ
โ+) |
53 | 39, 51, 52 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ (๐ + ๐ก) โ
โ+) |
54 | | ltaddrp 12957 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ก โ โ+)
โ ๐ < (๐ + ๐ก)) |
55 | 40, 51, 54 | syl2an 597 |
. . . . . . . 8
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ ๐ < (๐ + ๐ก)) |
56 | 53, 55 | jca 513 |
. . . . . . 7
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ ((๐ + ๐ก) โ โ+
โง ๐ < (๐ + ๐ก))) |
57 | 56 | adantrr 716 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ ((๐ + ๐ก) โ โ+ โง ๐ < (๐ + ๐ก))) |
58 | | simprlr 779 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ ๐ โ โ+) |
59 | | eqid 2733 |
. . . . . 6
โข (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + ((((๐ + ๐ก) ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐))))) = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + ((((๐ + ๐ก) ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐))))) |
60 | | pntlemp.U |
. . . . . . 7
โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐
โ๐ง) / ๐ง)) โค ๐) |
61 | 60 | adantr 482 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ โ๐ง โ (๐[,)+โ)(absโ((๐
โ๐ง) / ๐ง)) โค ๐) |
62 | | rpxr 12929 |
. . . . . . . . . 10
โข (๐ก โ โ+
โ ๐ก โ
โ*) |
63 | 62 | ad2antrl 727 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ ๐ก โ
โ*) |
64 | | rpre 12928 |
. . . . . . . . . . 11
โข (๐ก โ โ+
โ ๐ก โ
โ) |
65 | 64 | ad2antrl 727 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ ๐ก โ
โ) |
66 | 53 | rpred 12962 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ (๐ + ๐ก) โ
โ) |
67 | 39 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ ๐ โ
โ+) |
68 | 65, 67 | ltaddrp2d 12996 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ ๐ก < (๐ + ๐ก)) |
69 | 65, 66, 68 | ltled 11308 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ ๐ก โค (๐ + ๐ก)) |
70 | | iooss1 13305 |
. . . . . . . . 9
โข ((๐ก โ โ*
โง ๐ก โค (๐ + ๐ก)) โ ((๐ + ๐ก)(,)+โ) โ (๐ก(,)+โ)) |
71 | 63, 69, 70 | syl2anc 585 |
. . . . . . . 8
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ ((๐ + ๐ก)(,)+โ) โ (๐ก(,)+โ)) |
72 | 71 | adantrr 716 |
. . . . . . 7
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ ((๐ + ๐ก)(,)+โ) โ (๐ก(,)+โ)) |
73 | | simprrl 780 |
. . . . . . 7
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
74 | | ssralv 4011 |
. . . . . . . 8
โข (((๐ + ๐ก)(,)+โ) โ (๐ก(,)+โ) โ (โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ฆ โ ((๐ + ๐ก)(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
75 | 74 | ralimdv 3163 |
. . . . . . 7
โข (((๐ + ๐ก)(,)+โ) โ (๐ก(,)+โ) โ (โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ ((๐ + ๐ก)(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
76 | 72, 73, 75 | sylc 65 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ ((๐ + ๐ก)(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
77 | | simprrr 781 |
. . . . . 6
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐) |
78 | 25, 45, 46, 47, 29, 30, 48, 49, 33, 3, 50, 57, 58, 59, 61, 76, 77 | pntleme 26972 |
. . . . 5
โข ((๐ โง ((๐ก โ โ+ โง ๐ โ โ+)
โง (โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐))) โ โ๐ค โ โ+ โ๐ฃ โ (๐ค[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3)))) |
79 | 78 | expr 458 |
. . . 4
โข ((๐ โง (๐ก โ โ+ โง ๐ โ โ+))
โ ((โ๐ โ
(๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐) โ โ๐ค โ โ+ โ๐ฃ โ (๐ค[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3))))) |
80 | 79 | rexlimdvva 3202 |
. . 3
โข (๐ โ (โ๐ก โ โ+ โ๐ โ โ+
(โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐) โ โ๐ค โ โ+ โ๐ฃ โ (๐ค[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3))))) |
81 | 44, 80 | biimtrrid 242 |
. 2
โข (๐ โ ((โ๐ก โ โ+
โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐ก(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โง โ๐ โ โ+ โ๐ง โ
(1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐) โ โ๐ค โ โ+ โ๐ฃ โ (๐ค[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3))))) |
82 | 37, 43, 81 | mp2and 698 |
1
โข (๐ โ โ๐ค โ โ+ โ๐ฃ โ (๐ค[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3)))) |