Metamath Proof Explorer

Theorem logbpw2m1

Description: The floor of the binary logarithm of 2 to the power of a positive integer minus 1 is equal to the integer minus 1. (Contributed by AV, 31-May-2020)

Ref Expression
Assertion logbpw2m1 
|- ( I e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) = ( I - 1 ) )

Proof

Step Hyp Ref Expression
1 2rp 
 |-  2 e. RR+
2 1 a1i 
 |-  ( I e. NN -> 2 e. RR+ )
3 2nn0 
 |-  2 e. NN0
4 3 a1i 
 |-  ( I e. NN -> 2 e. NN0 )
5 nnnn0 
 |-  ( I e. NN -> I e. NN0 )
6 4 5 nn0expcld 
 |-  ( I e. NN -> ( 2 ^ I ) e. NN0 )
7 nnge1 
 |-  ( I e. NN -> 1 <_ I )
8 2re 
 |-  2 e. RR
9 8 a1i 
 |-  ( I e. NN -> 2 e. RR )
10 1zzd 
 |-  ( I e. NN -> 1 e. ZZ )
11 nnz 
 |-  ( I e. NN -> I e. ZZ )
12 1lt2 
 |-  1 < 2
13 12 a1i 
 |-  ( I e. NN -> 1 < 2 )
14 9 10 11 13 leexp2d 
 |-  ( I e. NN -> ( 1 <_ I <-> ( 2 ^ 1 ) <_ ( 2 ^ I ) ) )
15 2cn 
 |-  2 e. CC
16 exp1 
 |-  ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
17 15 16 ax-mp 
 |-  ( 2 ^ 1 ) = 2
18 17 a1i 
 |-  ( I e. NN -> ( 2 ^ 1 ) = 2 )
19 18 breq1d 
 |-  ( I e. NN -> ( ( 2 ^ 1 ) <_ ( 2 ^ I ) <-> 2 <_ ( 2 ^ I ) ) )
20 14 19 bitrd 
 |-  ( I e. NN -> ( 1 <_ I <-> 2 <_ ( 2 ^ I ) ) )
21 7 20 mpbid 
 |-  ( I e. NN -> 2 <_ ( 2 ^ I ) )
22 nn0ge2m1nn 
 |-  ( ( ( 2 ^ I ) e. NN0 /\ 2 <_ ( 2 ^ I ) ) -> ( ( 2 ^ I ) - 1 ) e. NN )
23 6 21 22 syl2anc 
 |-  ( I e. NN -> ( ( 2 ^ I ) - 1 ) e. NN )
24 23 nnrpd 
 |-  ( I e. NN -> ( ( 2 ^ I ) - 1 ) e. RR+ )
25 1ne2 
 |-  1 =/= 2
26 25 necomi 
 |-  2 =/= 1
27 26 a1i 
 |-  ( I e. NN -> 2 =/= 1 )
28 relogbcl 
 |-  ( ( 2 e. RR+ /\ ( ( 2 ^ I ) - 1 ) e. RR+ /\ 2 =/= 1 ) -> ( 2 logb ( ( 2 ^ I ) - 1 ) ) e. RR )
29 2 24 27 28 syl3anc 
 |-  ( I e. NN -> ( 2 logb ( ( 2 ^ I ) - 1 ) ) e. RR )
30 29 flcld 
 |-  ( I e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) e. ZZ )
31 peano2zm 
 |-  ( I e. ZZ -> ( I - 1 ) e. ZZ )
32 11 31 syl 
 |-  ( I e. NN -> ( I - 1 ) e. ZZ )
33 2z 
 |-  2 e. ZZ
34 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
35 33 34 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
36 nnlogbexp 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( I - 1 ) e. ZZ ) -> ( 2 logb ( 2 ^ ( I - 1 ) ) ) = ( I - 1 ) )
37 35 32 36 sylancr 
 |-  ( I e. NN -> ( 2 logb ( 2 ^ ( I - 1 ) ) ) = ( I - 1 ) )
38 37 fveq2d 
 |-  ( I e. NN -> ( |_ ` ( 2 logb ( 2 ^ ( I - 1 ) ) ) ) = ( |_ ` ( I - 1 ) ) )
39 flid 
 |-  ( ( I - 1 ) e. ZZ -> ( |_ ` ( I - 1 ) ) = ( I - 1 ) )
40 32 39 syl 
 |-  ( I e. NN -> ( |_ ` ( I - 1 ) ) = ( I - 1 ) )
41 38 40 eqtrd 
 |-  ( I e. NN -> ( |_ ` ( 2 logb ( 2 ^ ( I - 1 ) ) ) ) = ( I - 1 ) )
42 2nn 
 |-  2 e. NN
43 42 a1i 
 |-  ( I e. NN -> 2 e. NN )
44 nnm1nn0 
 |-  ( I e. NN -> ( I - 1 ) e. NN0 )
45 43 44 nnexpcld 
 |-  ( I e. NN -> ( 2 ^ ( I - 1 ) ) e. NN )
46 45 nnrpd 
 |-  ( I e. NN -> ( 2 ^ ( I - 1 ) ) e. RR+ )
47 relogbcl 
 |-  ( ( 2 e. RR+ /\ ( 2 ^ ( I - 1 ) ) e. RR+ /\ 2 =/= 1 ) -> ( 2 logb ( 2 ^ ( I - 1 ) ) ) e. RR )
48 2 46 27 47 syl3anc 
 |-  ( I e. NN -> ( 2 logb ( 2 ^ ( I - 1 ) ) ) e. RR )
49 pw2m1lepw2m1 
 |-  ( I e. NN -> ( 2 ^ ( I - 1 ) ) <_ ( ( 2 ^ I ) - 1 ) )
50 35 a1i 
 |-  ( I e. NN -> 2 e. ( ZZ>= ` 2 ) )
51 logbleb 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( 2 ^ ( I - 1 ) ) e. RR+ /\ ( ( 2 ^ I ) - 1 ) e. RR+ ) -> ( ( 2 ^ ( I - 1 ) ) <_ ( ( 2 ^ I ) - 1 ) <-> ( 2 logb ( 2 ^ ( I - 1 ) ) ) <_ ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) )
52 50 46 24 51 syl3anc 
 |-  ( I e. NN -> ( ( 2 ^ ( I - 1 ) ) <_ ( ( 2 ^ I ) - 1 ) <-> ( 2 logb ( 2 ^ ( I - 1 ) ) ) <_ ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) )
53 49 52 mpbid 
 |-  ( I e. NN -> ( 2 logb ( 2 ^ ( I - 1 ) ) ) <_ ( 2 logb ( ( 2 ^ I ) - 1 ) ) )
54 flwordi 
 |-  ( ( ( 2 logb ( 2 ^ ( I - 1 ) ) ) e. RR /\ ( 2 logb ( ( 2 ^ I ) - 1 ) ) e. RR /\ ( 2 logb ( 2 ^ ( I - 1 ) ) ) <_ ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) -> ( |_ ` ( 2 logb ( 2 ^ ( I - 1 ) ) ) ) <_ ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) )
55 48 29 53 54 syl3anc 
 |-  ( I e. NN -> ( |_ ` ( 2 logb ( 2 ^ ( I - 1 ) ) ) ) <_ ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) )
56 41 55 eqbrtrrd 
 |-  ( I e. NN -> ( I - 1 ) <_ ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) )
57 43 5 nnexpcld 
 |-  ( I e. NN -> ( 2 ^ I ) e. NN )
58 57 nnnn0d 
 |-  ( I e. NN -> ( 2 ^ I ) e. NN0 )
59 58 21 22 syl2anc 
 |-  ( I e. NN -> ( ( 2 ^ I ) - 1 ) e. NN )
60 59 nnrpd 
 |-  ( I e. NN -> ( ( 2 ^ I ) - 1 ) e. RR+ )
61 2 60 27 28 syl3anc 
 |-  ( I e. NN -> ( 2 logb ( ( 2 ^ I ) - 1 ) ) e. RR )
62 61 flcld 
 |-  ( I e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) e. ZZ )
63 62 zred 
 |-  ( I e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) e. RR )
64 nnre 
 |-  ( I e. NN -> I e. RR )
65 peano2rem 
 |-  ( I e. RR -> ( I - 1 ) e. RR )
66 64 65 syl 
 |-  ( I e. NN -> ( I - 1 ) e. RR )
67 peano2re 
 |-  ( ( I - 1 ) e. RR -> ( ( I - 1 ) + 1 ) e. RR )
68 66 67 syl 
 |-  ( I e. NN -> ( ( I - 1 ) + 1 ) e. RR )
69 flle 
 |-  ( ( 2 logb ( ( 2 ^ I ) - 1 ) ) e. RR -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) <_ ( 2 logb ( ( 2 ^ I ) - 1 ) ) )
70 29 69 syl 
 |-  ( I e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) <_ ( 2 logb ( ( 2 ^ I ) - 1 ) ) )
71 57 nnrpd 
 |-  ( I e. NN -> ( 2 ^ I ) e. RR+ )
72 relogbcl 
 |-  ( ( 2 e. RR+ /\ ( 2 ^ I ) e. RR+ /\ 2 =/= 1 ) -> ( 2 logb ( 2 ^ I ) ) e. RR )
73 2 71 27 72 syl3anc 
 |-  ( I e. NN -> ( 2 logb ( 2 ^ I ) ) e. RR )
74 57 nnred 
 |-  ( I e. NN -> ( 2 ^ I ) e. RR )
75 74 ltm1d 
 |-  ( I e. NN -> ( ( 2 ^ I ) - 1 ) < ( 2 ^ I ) )
76 logblt 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( ( 2 ^ I ) - 1 ) e. RR+ /\ ( 2 ^ I ) e. RR+ ) -> ( ( ( 2 ^ I ) - 1 ) < ( 2 ^ I ) <-> ( 2 logb ( ( 2 ^ I ) - 1 ) ) < ( 2 logb ( 2 ^ I ) ) ) )
77 50 24 71 76 syl3anc 
 |-  ( I e. NN -> ( ( ( 2 ^ I ) - 1 ) < ( 2 ^ I ) <-> ( 2 logb ( ( 2 ^ I ) - 1 ) ) < ( 2 logb ( 2 ^ I ) ) ) )
78 75 77 mpbid 
 |-  ( I e. NN -> ( 2 logb ( ( 2 ^ I ) - 1 ) ) < ( 2 logb ( 2 ^ I ) ) )
79 64 leidd 
 |-  ( I e. NN -> I <_ I )
80 nnlogbexp 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ I e. ZZ ) -> ( 2 logb ( 2 ^ I ) ) = I )
81 35 11 80 sylancr 
 |-  ( I e. NN -> ( 2 logb ( 2 ^ I ) ) = I )
82 nncn 
 |-  ( I e. NN -> I e. CC )
83 npcan1 
 |-  ( I e. CC -> ( ( I - 1 ) + 1 ) = I )
84 82 83 syl 
 |-  ( I e. NN -> ( ( I - 1 ) + 1 ) = I )
85 79 81 84 3brtr4d 
 |-  ( I e. NN -> ( 2 logb ( 2 ^ I ) ) <_ ( ( I - 1 ) + 1 ) )
86 29 73 68 78 85 ltletrd 
 |-  ( I e. NN -> ( 2 logb ( ( 2 ^ I ) - 1 ) ) < ( ( I - 1 ) + 1 ) )
87 63 29 68 70 86 lelttrd 
 |-  ( I e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) < ( ( I - 1 ) + 1 ) )
88 zgeltp1eq 
 |-  ( ( ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) e. ZZ /\ ( I - 1 ) e. ZZ ) -> ( ( ( I - 1 ) <_ ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) /\ ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) < ( ( I - 1 ) + 1 ) ) -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) = ( I - 1 ) ) )
89 88 imp 
 |-  ( ( ( ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) e. ZZ /\ ( I - 1 ) e. ZZ ) /\ ( ( I - 1 ) <_ ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) /\ ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) < ( ( I - 1 ) + 1 ) ) ) -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) = ( I - 1 ) )
90 30 32 56 87 89 syl22anc 
 |-  ( I e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) = ( I - 1 ) )