Step |
Hyp |
Ref |
Expression |
1 |
|
2z |
|- 2 e. ZZ |
2 |
|
uzid |
|- ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) ) |
3 |
1 2
|
mp1i |
|- ( X e. RR+ -> 2 e. ( ZZ>= ` 2 ) ) |
4 |
|
id |
|- ( X e. RR+ -> X e. RR+ ) |
5 |
|
eqid |
|- ( |_ ` ( 2 logb X ) ) = ( |_ ` ( 2 logb X ) ) |
6 |
3 4 5
|
fllogbd |
|- ( X e. RR+ -> ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) <_ X /\ X < ( 2 ^ ( ( |_ ` ( 2 logb X ) ) + 1 ) ) ) ) |
7 |
|
2re |
|- 2 e. RR |
8 |
7
|
a1i |
|- ( X e. RR+ -> 2 e. RR ) |
9 |
|
2ne0 |
|- 2 =/= 0 |
10 |
9
|
a1i |
|- ( X e. RR+ -> 2 =/= 0 ) |
11 |
|
relogbzcl |
|- ( ( 2 e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( 2 logb X ) e. RR ) |
12 |
3 4 11
|
syl2anc |
|- ( X e. RR+ -> ( 2 logb X ) e. RR ) |
13 |
12
|
flcld |
|- ( X e. RR+ -> ( |_ ` ( 2 logb X ) ) e. ZZ ) |
14 |
8 10 13
|
reexpclzd |
|- ( X e. RR+ -> ( 2 ^ ( |_ ` ( 2 logb X ) ) ) e. RR ) |
15 |
|
2pos |
|- 0 < 2 |
16 |
15
|
a1i |
|- ( X e. RR+ -> 0 < 2 ) |
17 |
|
expgt0 |
|- ( ( 2 e. RR /\ ( |_ ` ( 2 logb X ) ) e. ZZ /\ 0 < 2 ) -> 0 < ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) |
18 |
8 13 16 17
|
syl3anc |
|- ( X e. RR+ -> 0 < ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) |
19 |
14 18
|
elrpd |
|- ( X e. RR+ -> ( 2 ^ ( |_ ` ( 2 logb X ) ) ) e. RR+ ) |
20 |
|
rpre |
|- ( X e. RR+ -> X e. RR ) |
21 |
|
divge1b |
|- ( ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) e. RR+ /\ X e. RR ) -> ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) <_ X <-> 1 <_ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) ) ) |
22 |
21
|
bicomd |
|- ( ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) e. RR+ /\ X e. RR ) -> ( 1 <_ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) <-> ( 2 ^ ( |_ ` ( 2 logb X ) ) ) <_ X ) ) |
23 |
19 20 22
|
syl2anc |
|- ( X e. RR+ -> ( 1 <_ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) <-> ( 2 ^ ( |_ ` ( 2 logb X ) ) ) <_ X ) ) |
24 |
23
|
biimprd |
|- ( X e. RR+ -> ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) <_ X -> 1 <_ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) ) ) |
25 |
|
2cnd |
|- ( X e. RR+ -> 2 e. CC ) |
26 |
25 10 13
|
expp1zd |
|- ( X e. RR+ -> ( 2 ^ ( ( |_ ` ( 2 logb X ) ) + 1 ) ) = ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) x. 2 ) ) |
27 |
26
|
breq2d |
|- ( X e. RR+ -> ( X < ( 2 ^ ( ( |_ ` ( 2 logb X ) ) + 1 ) ) <-> X < ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) x. 2 ) ) ) |
28 |
|
ltdivmul |
|- ( ( X e. RR /\ 2 e. RR /\ ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) e. RR /\ 0 < ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) ) -> ( ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < 2 <-> X < ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) x. 2 ) ) ) |
29 |
20 8 14 18 28
|
syl112anc |
|- ( X e. RR+ -> ( ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < 2 <-> X < ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) x. 2 ) ) ) |
30 |
27 29
|
bitr4d |
|- ( X e. RR+ -> ( X < ( 2 ^ ( ( |_ ` ( 2 logb X ) ) + 1 ) ) <-> ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < 2 ) ) |
31 |
30
|
biimpd |
|- ( X e. RR+ -> ( X < ( 2 ^ ( ( |_ ` ( 2 logb X ) ) + 1 ) ) -> ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < 2 ) ) |
32 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
33 |
32
|
breq2i |
|- ( ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < ( 1 + 1 ) <-> ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < 2 ) |
34 |
31 33
|
syl6ibr |
|- ( X e. RR+ -> ( X < ( 2 ^ ( ( |_ ` ( 2 logb X ) ) + 1 ) ) -> ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < ( 1 + 1 ) ) ) |
35 |
24 34
|
anim12d |
|- ( X e. RR+ -> ( ( ( 2 ^ ( |_ ` ( 2 logb X ) ) ) <_ X /\ X < ( 2 ^ ( ( |_ ` ( 2 logb X ) ) + 1 ) ) ) -> ( 1 <_ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) /\ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < ( 1 + 1 ) ) ) ) |
36 |
6 35
|
mpd |
|- ( X e. RR+ -> ( 1 <_ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) /\ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < ( 1 + 1 ) ) ) |
37 |
25 10 13
|
expne0d |
|- ( X e. RR+ -> ( 2 ^ ( |_ ` ( 2 logb X ) ) ) =/= 0 ) |
38 |
20 14 37
|
redivcld |
|- ( X e. RR+ -> ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) e. RR ) |
39 |
|
1zzd |
|- ( X e. RR+ -> 1 e. ZZ ) |
40 |
|
flbi |
|- ( ( ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) e. RR /\ 1 e. ZZ ) -> ( ( |_ ` ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) ) = 1 <-> ( 1 <_ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) /\ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < ( 1 + 1 ) ) ) ) |
41 |
38 39 40
|
syl2anc |
|- ( X e. RR+ -> ( ( |_ ` ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) ) = 1 <-> ( 1 <_ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) /\ ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) < ( 1 + 1 ) ) ) ) |
42 |
36 41
|
mpbird |
|- ( X e. RR+ -> ( |_ ` ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) ) = 1 ) |