Metamath Proof Explorer

Theorem fllog2

Description: The floor of the binary logarithm of 2 to the power of an element of a half-open integer interval bounded by powers of 2 is equal to the integer. (Contributed by AV, 31-May-2020)

Ref Expression
Assertion fllog2 
|- ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( |_ ` ( 2 logb N ) ) = I )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( I e. NN0 -> I e. ZZ )
2 1 adantr 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> I e. ZZ )
3 2rp 
 |-  2 e. RR+
4 elfzoelz 
 |-  ( N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) -> N e. ZZ )
5 4 zred 
 |-  ( N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) -> N e. RR )
6 5 adantl 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> N e. RR )
7 elfzo2 
 |-  ( N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) <-> ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ /\ N < ( 2 ^ ( I + 1 ) ) ) )
8 eluz2 
 |-  ( N e. ( ZZ>= ` ( 2 ^ I ) ) <-> ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ ( 2 ^ I ) <_ N ) )
9 2re 
 |-  2 e. RR
10 2pos 
 |-  0 < 2
11 10 a1i 
 |-  ( I e. NN0 -> 0 < 2 )
12 expgt0 
 |-  ( ( 2 e. RR /\ I e. ZZ /\ 0 < 2 ) -> 0 < ( 2 ^ I ) )
13 9 1 11 12 mp3an2i 
 |-  ( I e. NN0 -> 0 < ( 2 ^ I ) )
14 13 adantl 
 |-  ( ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> 0 < ( 2 ^ I ) )
15 0red 
 |-  ( ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> 0 e. RR )
16 zre 
 |-  ( ( 2 ^ I ) e. ZZ -> ( 2 ^ I ) e. RR )
17 16 adantr 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ ) -> ( 2 ^ I ) e. RR )
18 17 adantr 
 |-  ( ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> ( 2 ^ I ) e. RR )
19 zre 
 |-  ( N e. ZZ -> N e. RR )
20 19 ad2antlr 
 |-  ( ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> N e. RR )
21 ltletr 
 |-  ( ( 0 e. RR /\ ( 2 ^ I ) e. RR /\ N e. RR ) -> ( ( 0 < ( 2 ^ I ) /\ ( 2 ^ I ) <_ N ) -> 0 < N ) )
22 15 18 20 21 syl3anc 
 |-  ( ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> ( ( 0 < ( 2 ^ I ) /\ ( 2 ^ I ) <_ N ) -> 0 < N ) )
23 14 22 mpand 
 |-  ( ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> ( ( 2 ^ I ) <_ N -> 0 < N ) )
24 23 ex 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ ) -> ( I e. NN0 -> ( ( 2 ^ I ) <_ N -> 0 < N ) ) )
25 24 com23 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ ) -> ( ( 2 ^ I ) <_ N -> ( I e. NN0 -> 0 < N ) ) )
26 25 3impia 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ ( 2 ^ I ) <_ N ) -> ( I e. NN0 -> 0 < N ) )
27 8 26 sylbi 
 |-  ( N e. ( ZZ>= ` ( 2 ^ I ) ) -> ( I e. NN0 -> 0 < N ) )
28 27 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ /\ N < ( 2 ^ ( I + 1 ) ) ) -> ( I e. NN0 -> 0 < N ) )
29 7 28 sylbi 
 |-  ( N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) -> ( I e. NN0 -> 0 < N ) )
30 29 impcom 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> 0 < N )
31 6 30 elrpd 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> N e. RR+ )
32 1ne2 
 |-  1 =/= 2
33 32 necomi 
 |-  2 =/= 1
34 33 a1i 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> 2 =/= 1 )
35 relogbcl 
 |-  ( ( 2 e. RR+ /\ N e. RR+ /\ 2 =/= 1 ) -> ( 2 logb N ) e. RR )
36 3 31 34 35 mp3an2i 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( 2 logb N ) e. RR )
37 36 flcld 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( |_ ` ( 2 logb N ) ) e. ZZ )
38 eluzelz 
 |-  ( N e. ( ZZ>= ` ( 2 ^ I ) ) -> N e. ZZ )
39 zltlem1 
 |-  ( ( N e. ZZ /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) -> ( N < ( 2 ^ ( I + 1 ) ) <-> N <_ ( ( 2 ^ ( I + 1 ) ) - 1 ) ) )
40 38 39 sylan 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) -> ( N < ( 2 ^ ( I + 1 ) ) <-> N <_ ( ( 2 ^ ( I + 1 ) ) - 1 ) ) )
41 2z 
 |-  2 e. ZZ
42 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
43 41 42 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
44 eluzelre 
 |-  ( N e. ( ZZ>= ` ( 2 ^ I ) ) -> N e. RR )
45 44 adantr 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ I e. NN0 ) -> N e. RR )
46 9 a1i 
 |-  ( I e. NN0 -> 2 e. RR )
47 46 1 11 3jca 
 |-  ( I e. NN0 -> ( 2 e. RR /\ I e. ZZ /\ 0 < 2 ) )
48 47 3ad2ant3 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ I e. NN0 ) -> ( 2 e. RR /\ I e. ZZ /\ 0 < 2 ) )
49 48 12 syl 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ I e. NN0 ) -> 0 < ( 2 ^ I ) )
50 0red 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ I e. NN0 ) -> 0 e. RR )
51 16 3ad2ant1 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ I e. NN0 ) -> ( 2 ^ I ) e. RR )
52 19 3ad2ant2 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ I e. NN0 ) -> N e. RR )
53 50 51 52 21 syl3anc 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ I e. NN0 ) -> ( ( 0 < ( 2 ^ I ) /\ ( 2 ^ I ) <_ N ) -> 0 < N ) )
54 49 53 mpand 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ I e. NN0 ) -> ( ( 2 ^ I ) <_ N -> 0 < N ) )
55 54 3exp 
 |-  ( ( 2 ^ I ) e. ZZ -> ( N e. ZZ -> ( I e. NN0 -> ( ( 2 ^ I ) <_ N -> 0 < N ) ) ) )
56 55 com34 
 |-  ( ( 2 ^ I ) e. ZZ -> ( N e. ZZ -> ( ( 2 ^ I ) <_ N -> ( I e. NN0 -> 0 < N ) ) ) )
57 56 3imp 
 |-  ( ( ( 2 ^ I ) e. ZZ /\ N e. ZZ /\ ( 2 ^ I ) <_ N ) -> ( I e. NN0 -> 0 < N ) )
58 8 57 sylbi 
 |-  ( N e. ( ZZ>= ` ( 2 ^ I ) ) -> ( I e. NN0 -> 0 < N ) )
59 58 imp 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ I e. NN0 ) -> 0 < N )
60 45 59 elrpd 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ I e. NN0 ) -> N e. RR+ )
61 60 adantlr 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> N e. RR+ )
62 9 a1i 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> 2 e. RR )
63 peano2nn0 
 |-  ( I e. NN0 -> ( I + 1 ) e. NN0 )
64 63 adantl 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( I + 1 ) e. NN0 )
65 62 64 reexpcld 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( 2 ^ ( I + 1 ) ) e. RR )
66 peano2rem 
 |-  ( ( 2 ^ ( I + 1 ) ) e. RR -> ( ( 2 ^ ( I + 1 ) ) - 1 ) e. RR )
67 65 66 syl 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( ( 2 ^ ( I + 1 ) ) - 1 ) e. RR )
68 nn0p1nn 
 |-  ( I e. NN0 -> ( I + 1 ) e. NN )
69 1lt2 
 |-  1 < 2
70 69 a1i 
 |-  ( I e. NN0 -> 1 < 2 )
71 46 68 70 3jca 
 |-  ( I e. NN0 -> ( 2 e. RR /\ ( I + 1 ) e. NN /\ 1 < 2 ) )
72 71 adantl 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( 2 e. RR /\ ( I + 1 ) e. NN /\ 1 < 2 ) )
73 expgt1 
 |-  ( ( 2 e. RR /\ ( I + 1 ) e. NN /\ 1 < 2 ) -> 1 < ( 2 ^ ( I + 1 ) ) )
74 72 73 syl 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> 1 < ( 2 ^ ( I + 1 ) ) )
75 1red 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> 1 e. RR )
76 zre 
 |-  ( ( 2 ^ ( I + 1 ) ) e. ZZ -> ( 2 ^ ( I + 1 ) ) e. RR )
77 76 ad2antlr 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( 2 ^ ( I + 1 ) ) e. RR )
78 75 77 posdifd 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( 1 < ( 2 ^ ( I + 1 ) ) <-> 0 < ( ( 2 ^ ( I + 1 ) ) - 1 ) ) )
79 74 78 mpbid 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> 0 < ( ( 2 ^ ( I + 1 ) ) - 1 ) )
80 67 79 elrpd 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( ( 2 ^ ( I + 1 ) ) - 1 ) e. RR+ )
81 logbleb 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ N e. RR+ /\ ( ( 2 ^ ( I + 1 ) ) - 1 ) e. RR+ ) -> ( N <_ ( ( 2 ^ ( I + 1 ) ) - 1 ) <-> ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) )
82 43 61 80 81 mp3an2i 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( N <_ ( ( 2 ^ ( I + 1 ) ) - 1 ) <-> ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) )
83 44 adantr 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) -> N e. RR )
84 83 adantr 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> N e. RR )
85 59 adantlr 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> 0 < N )
86 84 85 elrpd 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> N e. RR+ )
87 33 a1i 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> 2 =/= 1 )
88 3 86 87 35 mp3an2i 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( 2 logb N ) e. RR )
89 88 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) /\ ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) -> ( 2 logb N ) e. RR )
90 43 a1i 
 |-  ( I e. NN0 -> 2 e. ( ZZ>= ` 2 ) )
91 46 63 reexpcld 
 |-  ( I e. NN0 -> ( 2 ^ ( I + 1 ) ) e. RR )
92 91 66 syl 
 |-  ( I e. NN0 -> ( ( 2 ^ ( I + 1 ) ) - 1 ) e. RR )
93 9 68 70 73 mp3an2i 
 |-  ( I e. NN0 -> 1 < ( 2 ^ ( I + 1 ) ) )
94 1red 
 |-  ( I e. NN0 -> 1 e. RR )
95 94 91 posdifd 
 |-  ( I e. NN0 -> ( 1 < ( 2 ^ ( I + 1 ) ) <-> 0 < ( ( 2 ^ ( I + 1 ) ) - 1 ) ) )
96 93 95 mpbid 
 |-  ( I e. NN0 -> 0 < ( ( 2 ^ ( I + 1 ) ) - 1 ) )
97 92 96 elrpd 
 |-  ( I e. NN0 -> ( ( 2 ^ ( I + 1 ) ) - 1 ) e. RR+ )
98 90 97 jca 
 |-  ( I e. NN0 -> ( 2 e. ( ZZ>= ` 2 ) /\ ( ( 2 ^ ( I + 1 ) ) - 1 ) e. RR+ ) )
99 98 adantl 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( 2 e. ( ZZ>= ` 2 ) /\ ( ( 2 ^ ( I + 1 ) ) - 1 ) e. RR+ ) )
100 relogbzcl 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( ( 2 ^ ( I + 1 ) ) - 1 ) e. RR+ ) -> ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) e. RR )
101 99 100 syl 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) e. RR )
102 101 adantr 
 |-  ( ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) /\ ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) -> ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) e. RR )
103 simpr 
 |-  ( ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) /\ ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) -> ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) )
104 flwordi 
 |-  ( ( ( 2 logb N ) e. RR /\ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) e. RR /\ ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) -> ( |_ ` ( 2 logb N ) ) <_ ( |_ ` ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) )
105 89 102 103 104 syl3anc 
 |-  ( ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) /\ ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) -> ( |_ ` ( 2 logb N ) ) <_ ( |_ ` ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) )
106 105 ex 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) -> ( |_ ` ( 2 logb N ) ) <_ ( |_ ` ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) ) )
107 68 adantl 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( I + 1 ) e. NN )
108 logbpw2m1 
 |-  ( ( I + 1 ) e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) = ( ( I + 1 ) - 1 ) )
109 107 108 syl 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( |_ ` ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) = ( ( I + 1 ) - 1 ) )
110 nn0cn 
 |-  ( I e. NN0 -> I e. CC )
111 pncan1 
 |-  ( I e. CC -> ( ( I + 1 ) - 1 ) = I )
112 110 111 syl 
 |-  ( I e. NN0 -> ( ( I + 1 ) - 1 ) = I )
113 112 adantl 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( ( I + 1 ) - 1 ) = I )
114 109 113 eqtrd 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( |_ ` ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) = I )
115 114 breq2d 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( ( |_ ` ( 2 logb N ) ) <_ ( |_ ` ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) ) <-> ( |_ ` ( 2 logb N ) ) <_ I ) )
116 106 115 sylibd 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( ( 2 logb N ) <_ ( 2 logb ( ( 2 ^ ( I + 1 ) ) - 1 ) ) -> ( |_ ` ( 2 logb N ) ) <_ I ) )
117 82 116 sylbid 
 |-  ( ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) /\ I e. NN0 ) -> ( N <_ ( ( 2 ^ ( I + 1 ) ) - 1 ) -> ( |_ ` ( 2 logb N ) ) <_ I ) )
118 117 ex 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) -> ( I e. NN0 -> ( N <_ ( ( 2 ^ ( I + 1 ) ) - 1 ) -> ( |_ ` ( 2 logb N ) ) <_ I ) ) )
119 118 com23 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) -> ( N <_ ( ( 2 ^ ( I + 1 ) ) - 1 ) -> ( I e. NN0 -> ( |_ ` ( 2 logb N ) ) <_ I ) ) )
120 40 119 sylbid 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ ) -> ( N < ( 2 ^ ( I + 1 ) ) -> ( I e. NN0 -> ( |_ ` ( 2 logb N ) ) <_ I ) ) )
121 120 3impia 
 |-  ( ( N e. ( ZZ>= ` ( 2 ^ I ) ) /\ ( 2 ^ ( I + 1 ) ) e. ZZ /\ N < ( 2 ^ ( I + 1 ) ) ) -> ( I e. NN0 -> ( |_ ` ( 2 logb N ) ) <_ I ) )
122 7 121 sylbi 
 |-  ( N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) -> ( I e. NN0 -> ( |_ ` ( 2 logb N ) ) <_ I ) )
123 122 impcom 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( |_ ` ( 2 logb N ) ) <_ I )
124 nn0re 
 |-  ( I e. NN0 -> I e. RR )
125 nn0ge0 
 |-  ( I e. NN0 -> 0 <_ I )
126 flge0nn0 
 |-  ( ( I e. RR /\ 0 <_ I ) -> ( |_ ` I ) e. NN0 )
127 124 125 126 syl2anc 
 |-  ( I e. NN0 -> ( |_ ` I ) e. NN0 )
128 127 nn0red 
 |-  ( I e. NN0 -> ( |_ ` I ) e. RR )
129 128 adantr 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( |_ ` I ) e. RR )
130 124 adantr 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> I e. RR )
131 flle 
 |-  ( I e. RR -> ( |_ ` I ) <_ I )
132 124 131 syl 
 |-  ( I e. NN0 -> ( |_ ` I ) <_ I )
133 132 adantr 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( |_ ` I ) <_ I )
134 3 a1i 
 |-  ( I e. NN0 -> 2 e. RR+ )
135 134 1 rpexpcld 
 |-  ( I e. NN0 -> ( 2 ^ I ) e. RR+ )
136 33 a1i 
 |-  ( I e. NN0 -> 2 =/= 1 )
137 relogbcl 
 |-  ( ( 2 e. RR+ /\ ( 2 ^ I ) e. RR+ /\ 2 =/= 1 ) -> ( 2 logb ( 2 ^ I ) ) e. RR )
138 3 135 136 137 mp3an2i 
 |-  ( I e. NN0 -> ( 2 logb ( 2 ^ I ) ) e. RR )
139 138 adantr 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( 2 logb ( 2 ^ I ) ) e. RR )
140 nnlogbexp 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ I e. ZZ ) -> ( 2 logb ( 2 ^ I ) ) = I )
141 90 1 140 syl2anc 
 |-  ( I e. NN0 -> ( 2 logb ( 2 ^ I ) ) = I )
142 141 eqcomd 
 |-  ( I e. NN0 -> I = ( 2 logb ( 2 ^ I ) ) )
143 124 142 eqled 
 |-  ( I e. NN0 -> I <_ ( 2 logb ( 2 ^ I ) ) )
144 143 adantr 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> I <_ ( 2 logb ( 2 ^ I ) ) )
145 elfzole1 
 |-  ( N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) -> ( 2 ^ I ) <_ N )
146 145 adantl 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( 2 ^ I ) <_ N )
147 135 adantr 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( 2 ^ I ) e. RR+ )
148 logbleb 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( 2 ^ I ) e. RR+ /\ N e. RR+ ) -> ( ( 2 ^ I ) <_ N <-> ( 2 logb ( 2 ^ I ) ) <_ ( 2 logb N ) ) )
149 43 147 31 148 mp3an2i 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( ( 2 ^ I ) <_ N <-> ( 2 logb ( 2 ^ I ) ) <_ ( 2 logb N ) ) )
150 146 149 mpbid 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( 2 logb ( 2 ^ I ) ) <_ ( 2 logb N ) )
151 130 139 36 144 150 letrd 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> I <_ ( 2 logb N ) )
152 129 130 36 133 151 letrd 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( |_ ` I ) <_ ( 2 logb N ) )
153 flflp1 
 |-  ( ( I e. RR /\ ( 2 logb N ) e. RR ) -> ( ( |_ ` I ) <_ ( 2 logb N ) <-> I < ( ( |_ ` ( 2 logb N ) ) + 1 ) ) )
154 130 36 153 syl2anc 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( ( |_ ` I ) <_ ( 2 logb N ) <-> I < ( ( |_ ` ( 2 logb N ) ) + 1 ) ) )
155 152 154 mpbid 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> I < ( ( |_ ` ( 2 logb N ) ) + 1 ) )
156 zgeltp1eq 
 |-  ( ( I e. ZZ /\ ( |_ ` ( 2 logb N ) ) e. ZZ ) -> ( ( ( |_ ` ( 2 logb N ) ) <_ I /\ I < ( ( |_ ` ( 2 logb N ) ) + 1 ) ) -> I = ( |_ ` ( 2 logb N ) ) ) )
157 156 imp 
 |-  ( ( ( I e. ZZ /\ ( |_ ` ( 2 logb N ) ) e. ZZ ) /\ ( ( |_ ` ( 2 logb N ) ) <_ I /\ I < ( ( |_ ` ( 2 logb N ) ) + 1 ) ) ) -> I = ( |_ ` ( 2 logb N ) ) )
158 2 37 123 155 157 syl22anc 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> I = ( |_ ` ( 2 logb N ) ) )
159 158 eqcomd 
 |-  ( ( I e. NN0 /\ N e. ( ( 2 ^ I ) ..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( |_ ` ( 2 logb N ) ) = I )