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 + X 2 log 2 X = 1

Proof

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