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 imbitrrdi 
 |-  ( 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 )