Step | Hyp | Ref
| Expression |
1 | | chpdifbnd.c |
. . 3
โข ๐ถ = ((๐ต ยท (๐ด + 1)) + ((2 ยท ๐ด) ยท (logโ๐ด))) |
2 | | chpdifbnd.b |
. . . . . . 7
โข (๐ โ ๐ต โ
โ+) |
3 | | chpdifbnd.a |
. . . . . . . 8
โข (๐ โ ๐ด โ
โ+) |
4 | | 1rp 13002 |
. . . . . . . 8
โข 1 โ
โ+ |
5 | | rpaddcl 13020 |
. . . . . . . 8
โข ((๐ด โ โ+
โง 1 โ โ+) โ (๐ด + 1) โ
โ+) |
6 | 3, 4, 5 | sylancl 585 |
. . . . . . 7
โข (๐ โ (๐ด + 1) โ
โ+) |
7 | 2, 6 | rpmulcld 13056 |
. . . . . 6
โข (๐ โ (๐ต ยท (๐ด + 1)) โ
โ+) |
8 | 7 | rpred 13040 |
. . . . 5
โข (๐ โ (๐ต ยท (๐ด + 1)) โ โ) |
9 | | 2rp 13003 |
. . . . . . . 8
โข 2 โ
โ+ |
10 | | rpmulcl 13021 |
. . . . . . . 8
โข ((2
โ โ+ โง ๐ด โ โ+) โ (2
ยท ๐ด) โ
โ+) |
11 | 9, 3, 10 | sylancr 586 |
. . . . . . 7
โข (๐ โ (2 ยท ๐ด) โ
โ+) |
12 | 11 | rpred 13040 |
. . . . . 6
โข (๐ โ (2 ยท ๐ด) โ
โ) |
13 | 3 | relogcld 26544 |
. . . . . 6
โข (๐ โ (logโ๐ด) โ
โ) |
14 | 12, 13 | remulcld 11266 |
. . . . 5
โข (๐ โ ((2 ยท ๐ด) ยท (logโ๐ด)) โ
โ) |
15 | 8, 14 | readdcld 11265 |
. . . 4
โข (๐ โ ((๐ต ยท (๐ด + 1)) + ((2 ยท ๐ด) ยท (logโ๐ด))) โ โ) |
16 | 7 | rpgt0d 13043 |
. . . . 5
โข (๐ โ 0 < (๐ต ยท (๐ด + 1))) |
17 | 11 | rprege0d 13047 |
. . . . . 6
โข (๐ โ ((2 ยท ๐ด) โ โ โง 0 โค (2
ยท ๐ด))) |
18 | | log1 26506 |
. . . . . . 7
โข
(logโ1) = 0 |
19 | | chpdifbnd.1 |
. . . . . . . 8
โข (๐ โ 1 โค ๐ด) |
20 | | logleb 26524 |
. . . . . . . . 9
โข ((1
โ โ+ โง ๐ด โ โ+) โ (1 โค
๐ด โ (logโ1) โค
(logโ๐ด))) |
21 | 4, 3, 20 | sylancr 586 |
. . . . . . . 8
โข (๐ โ (1 โค ๐ด โ (logโ1) โค (logโ๐ด))) |
22 | 19, 21 | mpbid 231 |
. . . . . . 7
โข (๐ โ (logโ1) โค
(logโ๐ด)) |
23 | 18, 22 | eqbrtrrid 5178 |
. . . . . 6
โข (๐ โ 0 โค (logโ๐ด)) |
24 | | mulge0 11754 |
. . . . . 6
โข ((((2
ยท ๐ด) โ โ
โง 0 โค (2 ยท ๐ด)) โง ((logโ๐ด) โ โ โง 0 โค
(logโ๐ด))) โ 0
โค ((2 ยท ๐ด)
ยท (logโ๐ด))) |
25 | 17, 13, 23, 24 | syl12anc 836 |
. . . . 5
โข (๐ โ 0 โค ((2 ยท ๐ด) ยท (logโ๐ด))) |
26 | 8, 14, 16, 25 | addgtge0d 11810 |
. . . 4
โข (๐ โ 0 < ((๐ต ยท (๐ด + 1)) + ((2 ยท ๐ด) ยท (logโ๐ด)))) |
27 | 15, 26 | elrpd 13037 |
. . 3
โข (๐ โ ((๐ต ยท (๐ด + 1)) + ((2 ยท ๐ด) ยท (logโ๐ด))) โ
โ+) |
28 | 1, 27 | eqeltrid 2832 |
. 2
โข (๐ โ ๐ถ โ
โ+) |
29 | 3 | adantr 480 |
. . . 4
โข ((๐ โง (๐ฅ โ (1(,)+โ) โง ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ)))) โ ๐ด โ
โ+) |
30 | 19 | adantr 480 |
. . . 4
โข ((๐ โง (๐ฅ โ (1(,)+โ) โง ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ)))) โ 1 โค ๐ด) |
31 | 2 | adantr 480 |
. . . 4
โข ((๐ โง (๐ฅ โ (1(,)+โ) โง ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ)))) โ ๐ต โ
โ+) |
32 | | chpdifbnd.2 |
. . . . 5
โข (๐ โ โ๐ง โ
(1[,)+โ)(absโ(((((ฯโ๐ง) ยท (logโ๐ง)) + ฮฃ๐ โ (1...(โโ๐ง))((ฮโ๐) ยท (ฯโ(๐ง / ๐)))) / ๐ง) โ (2 ยท (logโ๐ง)))) โค ๐ต) |
33 | 32 | adantr 480 |
. . . 4
โข ((๐ โง (๐ฅ โ (1(,)+โ) โง ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ)))) โ โ๐ง โ
(1[,)+โ)(absโ(((((ฯโ๐ง) ยท (logโ๐ง)) + ฮฃ๐ โ (1...(โโ๐ง))((ฮโ๐) ยท (ฯโ(๐ง / ๐)))) / ๐ง) โ (2 ยท (logโ๐ง)))) โค ๐ต) |
34 | | simprl 770 |
. . . 4
โข ((๐ โง (๐ฅ โ (1(,)+โ) โง ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ)))) โ ๐ฅ โ (1(,)+โ)) |
35 | | simprr 772 |
. . . 4
โข ((๐ โง (๐ฅ โ (1(,)+โ) โง ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ)))) โ ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ))) |
36 | 29, 30, 31, 33, 1, 34, 35 | chpdifbndlem1 27473 |
. . 3
โข ((๐ โง (๐ฅ โ (1(,)+โ) โง ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ)))) โ ((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ถ ยท (๐ฅ / (logโ๐ฅ))))) |
37 | 36 | ralrimivva 3195 |
. 2
โข (๐ โ โ๐ฅ โ (1(,)+โ)โ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ))((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ถ ยท (๐ฅ / (logโ๐ฅ))))) |
38 | | oveq1 7421 |
. . . . . 6
โข (๐ = ๐ถ โ (๐ ยท (๐ฅ / (logโ๐ฅ))) = (๐ถ ยท (๐ฅ / (logโ๐ฅ)))) |
39 | 38 | oveq2d 7430 |
. . . . 5
โข (๐ = ๐ถ โ ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ ยท (๐ฅ / (logโ๐ฅ)))) = ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ถ ยท (๐ฅ / (logโ๐ฅ))))) |
40 | 39 | breq2d 5154 |
. . . 4
โข (๐ = ๐ถ โ (((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ ยท (๐ฅ / (logโ๐ฅ)))) โ ((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ถ ยท (๐ฅ / (logโ๐ฅ)))))) |
41 | 40 | 2ralbidv 3213 |
. . 3
โข (๐ = ๐ถ โ (โ๐ฅ โ (1(,)+โ)โ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ))((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ ยท (๐ฅ / (logโ๐ฅ)))) โ โ๐ฅ โ (1(,)+โ)โ๐ฆ โ (๐ฅ[,](๐ด ยท ๐ฅ))((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ถ ยท (๐ฅ / (logโ๐ฅ)))))) |
42 | 41 | rspcev 3607 |
. 2
โข ((๐ถ โ โ+
โง โ๐ฅ โ
(1(,)+โ)โ๐ฆ
โ (๐ฅ[,](๐ด ยท ๐ฅ))((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ถ ยท (๐ฅ / (logโ๐ฅ))))) โ โ๐ โ โ+ โ๐ฅ โ
(1(,)+โ)โ๐ฆ
โ (๐ฅ[,](๐ด ยท ๐ฅ))((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ ยท (๐ฅ / (logโ๐ฅ))))) |
43 | 28, 37, 42 | syl2anc 583 |
1
โข (๐ โ โ๐ โ โ+ โ๐ฅ โ
(1(,)+โ)โ๐ฆ
โ (๐ฅ[,](๐ด ยท ๐ฅ))((ฯโ๐ฆ) โ (ฯโ๐ฅ)) โค ((2 ยท (๐ฆ โ ๐ฅ)) + (๐ ยท (๐ฅ / (logโ๐ฅ))))) |