Step | Hyp | Ref
| Expression |
1 | | 2z 12542 |
. . . . 5
โข 2 โ
โค |
2 | | uzid 12785 |
. . . . 5
โข (2 โ
โค โ 2 โ (โคโฅโ2)) |
3 | 1, 2 | mp1i 13 |
. . . 4
โข (๐ โ โ+
โ 2 โ (โคโฅโ2)) |
4 | | id 22 |
. . . 4
โข (๐ โ โ+
โ ๐ โ
โ+) |
5 | | eqid 2737 |
. . . 4
โข
(โโ(2 logb ๐)) = (โโ(2 logb ๐)) |
6 | 3, 4, 5 | fllogbd 46720 |
. . 3
โข (๐ โ โ+
โ ((2โ(โโ(2 logb ๐))) โค ๐ โง ๐ < (2โ((โโ(2
logb ๐)) +
1)))) |
7 | | 2re 12234 |
. . . . . . . . 9
โข 2 โ
โ |
8 | 7 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ+
โ 2 โ โ) |
9 | | 2ne0 12264 |
. . . . . . . . 9
โข 2 โ
0 |
10 | 9 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ+
โ 2 โ 0) |
11 | | relogbzcl 26140 |
. . . . . . . . . 10
โข ((2
โ (โคโฅโ2) โง ๐ โ โ+) โ (2
logb ๐) โ
โ) |
12 | 3, 4, 11 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ โ+
โ (2 logb ๐) โ โ) |
13 | 12 | flcld 13710 |
. . . . . . . 8
โข (๐ โ โ+
โ (โโ(2 logb ๐)) โ โค) |
14 | 8, 10, 13 | reexpclzd 14159 |
. . . . . . 7
โข (๐ โ โ+
โ (2โ(โโ(2 logb ๐))) โ โ) |
15 | | 2pos 12263 |
. . . . . . . . 9
โข 0 <
2 |
16 | 15 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ+
โ 0 < 2) |
17 | | expgt0 14008 |
. . . . . . . 8
โข ((2
โ โ โง (โโ(2 logb ๐)) โ โค โง 0 < 2) โ 0
< (2โ(โโ(2 logb ๐)))) |
18 | 8, 13, 16, 17 | syl3anc 1372 |
. . . . . . 7
โข (๐ โ โ+
โ 0 < (2โ(โโ(2 logb ๐)))) |
19 | 14, 18 | elrpd 12961 |
. . . . . 6
โข (๐ โ โ+
โ (2โ(โโ(2 logb ๐))) โ
โ+) |
20 | | rpre 12930 |
. . . . . 6
โข (๐ โ โ+
โ ๐ โ
โ) |
21 | | divge1b 46667 |
. . . . . . 7
โข
(((2โ(โโ(2 logb ๐))) โ โ+ โง ๐ โ โ) โ
((2โ(โโ(2 logb ๐))) โค ๐ โ 1 โค (๐ / (2โ(โโ(2 logb
๐)))))) |
22 | 21 | bicomd 222 |
. . . . . 6
โข
(((2โ(โโ(2 logb ๐))) โ โ+ โง ๐ โ โ) โ (1 โค
(๐ /
(2โ(โโ(2 logb ๐)))) โ (2โ(โโ(2
logb ๐))) โค
๐)) |
23 | 19, 20, 22 | syl2anc 585 |
. . . . 5
โข (๐ โ โ+
โ (1 โค (๐ /
(2โ(โโ(2 logb ๐)))) โ (2โ(โโ(2
logb ๐))) โค
๐)) |
24 | 23 | biimprd 248 |
. . . 4
โข (๐ โ โ+
โ ((2โ(โโ(2 logb ๐))) โค ๐ โ 1 โค (๐ / (2โ(โโ(2 logb
๐)))))) |
25 | | 2cnd 12238 |
. . . . . . . . 9
โข (๐ โ โ+
โ 2 โ โ) |
26 | 25, 10, 13 | expp1zd 14067 |
. . . . . . . 8
โข (๐ โ โ+
โ (2โ((โโ(2 logb ๐)) + 1)) = ((2โ(โโ(2
logb ๐)))
ยท 2)) |
27 | 26 | breq2d 5122 |
. . . . . . 7
โข (๐ โ โ+
โ (๐ <
(2โ((โโ(2 logb ๐)) + 1)) โ ๐ < ((2โ(โโ(2
logb ๐)))
ยท 2))) |
28 | | ltdivmul 12037 |
. . . . . . . 8
โข ((๐ โ โ โง 2 โ
โ โง ((2โ(โโ(2 logb ๐))) โ โ โง 0 <
(2โ(โโ(2 logb ๐))))) โ ((๐ / (2โ(โโ(2 logb
๐)))) < 2 โ ๐ < ((2โ(โโ(2
logb ๐)))
ยท 2))) |
29 | 20, 8, 14, 18, 28 | syl112anc 1375 |
. . . . . . 7
โข (๐ โ โ+
โ ((๐ /
(2โ(โโ(2 logb ๐)))) < 2 โ ๐ < ((2โ(โโ(2
logb ๐)))
ยท 2))) |
30 | 27, 29 | bitr4d 282 |
. . . . . 6
โข (๐ โ โ+
โ (๐ <
(2โ((โโ(2 logb ๐)) + 1)) โ (๐ / (2โ(โโ(2 logb
๐)))) <
2)) |
31 | 30 | biimpd 228 |
. . . . 5
โข (๐ โ โ+
โ (๐ <
(2โ((โโ(2 logb ๐)) + 1)) โ (๐ / (2โ(โโ(2 logb
๐)))) <
2)) |
32 | | 1p1e2 12285 |
. . . . . 6
โข (1 + 1) =
2 |
33 | 32 | breq2i 5118 |
. . . . 5
โข ((๐ / (2โ(โโ(2
logb ๐)))) <
(1 + 1) โ (๐ /
(2โ(โโ(2 logb ๐)))) < 2) |
34 | 31, 33 | syl6ibr 252 |
. . . 4
โข (๐ โ โ+
โ (๐ <
(2โ((โโ(2 logb ๐)) + 1)) โ (๐ / (2โ(โโ(2 logb
๐)))) < (1 +
1))) |
35 | 24, 34 | anim12d 610 |
. . 3
โข (๐ โ โ+
โ (((2โ(โโ(2 logb ๐))) โค ๐ โง ๐ < (2โ((โโ(2
logb ๐)) + 1)))
โ (1 โค (๐ /
(2โ(โโ(2 logb ๐)))) โง (๐ / (2โ(โโ(2 logb
๐)))) < (1 +
1)))) |
36 | 6, 35 | mpd 15 |
. 2
โข (๐ โ โ+
โ (1 โค (๐ /
(2โ(โโ(2 logb ๐)))) โง (๐ / (2โ(โโ(2 logb
๐)))) < (1 +
1))) |
37 | 25, 10, 13 | expne0d 14064 |
. . . 4
โข (๐ โ โ+
โ (2โ(โโ(2 logb ๐))) โ 0) |
38 | 20, 14, 37 | redivcld 11990 |
. . 3
โข (๐ โ โ+
โ (๐ /
(2โ(โโ(2 logb ๐)))) โ โ) |
39 | | 1zzd 12541 |
. . 3
โข (๐ โ โ+
โ 1 โ โค) |
40 | | flbi 13728 |
. . 3
โข (((๐ / (2โ(โโ(2
logb ๐))))
โ โ โง 1 โ โค) โ ((โโ(๐ / (2โ(โโ(2
logb ๐))))) = 1
โ (1 โค (๐ /
(2โ(โโ(2 logb ๐)))) โง (๐ / (2โ(โโ(2 logb
๐)))) < (1 +
1)))) |
41 | 38, 39, 40 | syl2anc 585 |
. 2
โข (๐ โ โ+
โ ((โโ(๐ /
(2โ(โโ(2 logb ๐))))) = 1 โ (1 โค (๐ / (2โ(โโ(2 logb
๐)))) โง (๐ / (2โ(โโ(2
logb ๐)))) <
(1 + 1)))) |
42 | 36, 41 | mpbird 257 |
1
โข (๐ โ โ+
โ (โโ(๐ /
(2โ(โโ(2 logb ๐))))) = 1) |