Metamath Proof Explorer


Theorem fldivexpfllog2

Description: The floor of a positive real number divided by 2 to the power of the floor of the logarithm to base 2 of the number is 1. (Contributed by AV, 26-May-2020)

Ref Expression
Assertion fldivexpfllog2
|- ( X e. RR+ -> ( |_ ` ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) ) = 1 )

Proof

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 )