Metamath Proof Explorer

Theorem nnolog2flm1

Description: The floor of the binary logarithm of an odd integer greater than 1 is the floor of the binary logarithm of the integer decreased by 1. (Contributed by AV, 2-Jun-2020)

Ref Expression
Assertion nnolog2flm1 
|- ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
2 nnpw2blenfzo2 
 |-  ( N e. NN -> ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) \/ N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) ) )
3 1 2 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) \/ N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) ) )
4 1 adantl 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> N e. NN )
5 nneo 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) )
6 5 bicomd 
 |-  ( N e. NN -> ( -. ( ( N + 1 ) / 2 ) e. NN <-> ( N / 2 ) e. NN ) )
7 4 6 syl 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( -. ( ( N + 1 ) / 2 ) e. NN <-> ( N / 2 ) e. NN ) )
8 notnotb 
 |-  ( ( N / 2 ) e. NN <-> -. -. ( N / 2 ) e. NN )
9 7 8 bitrdi 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( -. ( ( N + 1 ) / 2 ) e. NN <-> -. -. ( N / 2 ) e. NN ) )
10 9 con4bid 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( N + 1 ) / 2 ) e. NN <-> -. ( N / 2 ) e. NN ) )
11 simpl 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> N = ( 2 ^ ( ( #b ` N ) - 1 ) ) )
12 11 oveq1d 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( N / 2 ) = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) / 2 ) )
13 blennnelnn 
 |-  ( N e. NN -> ( #b ` N ) e. NN )
14 13 nnnn0d 
 |-  ( N e. NN -> ( #b ` N ) e. NN0 )
15 1 14 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( #b ` N ) e. NN0 )
16 2m1e1 
 |-  ( 2 - 1 ) = 1
17 2cn 
 |-  2 e. CC
18 2ne0 
 |-  2 =/= 0
19 1ne2 
 |-  1 =/= 2
20 19 necomi 
 |-  2 =/= 1
21 logbid1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 2 ) = 1 )
22 17 18 20 21 mp3an 
 |-  ( 2 logb 2 ) = 1
23 eluzle 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
24 2z 
 |-  2 e. ZZ
25 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
26 24 25 mp1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. ( ZZ>= ` 2 ) )
27 2rp 
 |-  2 e. RR+
28 27 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. RR+ )
29 1 nnrpd 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR+ )
30 logbleb 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ 2 e. RR+ /\ N e. RR+ ) -> ( 2 <_ N <-> ( 2 logb 2 ) <_ ( 2 logb N ) ) )
31 26 28 29 30 syl3anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 <_ N <-> ( 2 logb 2 ) <_ ( 2 logb N ) ) )
32 23 31 mpbid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 logb 2 ) <_ ( 2 logb N ) )
33 22 32 eqbrtrrid 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 <_ ( 2 logb N ) )
34 20 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 =/= 1 )
35 relogbcl 
 |-  ( ( 2 e. RR+ /\ N e. RR+ /\ 2 =/= 1 ) -> ( 2 logb N ) e. RR )
36 28 29 34 35 syl3anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 logb N ) e. RR )
37 1zzd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. ZZ )
38 flge 
 |-  ( ( ( 2 logb N ) e. RR /\ 1 e. ZZ ) -> ( 1 <_ ( 2 logb N ) <-> 1 <_ ( |_ ` ( 2 logb N ) ) ) )
39 36 37 38 syl2anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 1 <_ ( 2 logb N ) <-> 1 <_ ( |_ ` ( 2 logb N ) ) ) )
40 33 39 mpbid 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 <_ ( |_ ` ( 2 logb N ) ) )
41 16 40 eqbrtrid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 - 1 ) <_ ( |_ ` ( 2 logb N ) ) )
42 2re 
 |-  2 e. RR
43 42 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. RR )
44 1red 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. RR )
45 36 flcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( 2 logb N ) ) e. ZZ )
46 45 zred 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( 2 logb N ) ) e. RR )
47 43 44 46 lesubaddd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 - 1 ) <_ ( |_ ` ( 2 logb N ) ) <-> 2 <_ ( ( |_ ` ( 2 logb N ) ) + 1 ) ) )
48 41 47 mpbid 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ ( ( |_ ` ( 2 logb N ) ) + 1 ) )
49 blennn 
 |-  ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
50 1 49 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
51 48 50 breqtrrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ ( #b ` N ) )
52 nn0ge2m1nn 
 |-  ( ( ( #b ` N ) e. NN0 /\ 2 <_ ( #b ` N ) ) -> ( ( #b ` N ) - 1 ) e. NN )
53 15 51 52 syl2anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( #b ` N ) - 1 ) e. NN )
54 53 adantl 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( #b ` N ) - 1 ) e. NN )
55 nnpw2even 
 |-  ( ( ( #b ` N ) - 1 ) e. NN -> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) / 2 ) e. NN )
56 54 55 syl 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) / 2 ) e. NN )
57 12 56 eqeltrd 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( N / 2 ) e. NN )
58 57 pm2.24d 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( -. ( N / 2 ) e. NN -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) ) )
59 10 58 sylbid 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( N + 1 ) / 2 ) e. NN -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) ) )
60 59 ex 
 |-  ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) -> ( N e. ( ZZ>= ` 2 ) -> ( ( ( N + 1 ) / 2 ) e. NN -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) ) ) )
61 1 13 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( #b ` N ) e. NN )
62 nnm1nn0 
 |-  ( ( #b ` N ) e. NN -> ( ( #b ` N ) - 1 ) e. NN0 )
63 61 62 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( #b ` N ) - 1 ) e. NN0 )
64 63 ad2antlr 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( ( #b ` N ) - 1 ) e. NN0 )
65 1 ad2antlr 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> N e. NN )
66 nnpw2blenfzo 
 |-  ( N e. NN -> N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( #b ` N ) ) ) )
67 65 66 syl 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( #b ` N ) ) ) )
68 61 nncnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( #b ` N ) e. CC )
69 68 ad2antlr 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( #b ` N ) e. CC )
70 npcan1 
 |-  ( ( #b ` N ) e. CC -> ( ( ( #b ` N ) - 1 ) + 1 ) = ( #b ` N ) )
71 69 70 syl 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( ( ( #b ` N ) - 1 ) + 1 ) = ( #b ` N ) )
72 71 oveq2d 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) = ( 2 ^ ( #b ` N ) ) )
73 72 oveq2d 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( #b ` N ) ) ) )
74 67 73 eleqtrrd 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) )
75 fllog2 
 |-  ( ( ( ( #b ` N ) - 1 ) e. NN0 /\ N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) ) -> ( |_ ` ( 2 logb N ) ) = ( ( #b ` N ) - 1 ) )
76 64 74 75 syl2anc 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( |_ ` ( 2 logb N ) ) = ( ( #b ` N ) - 1 ) )
77 61 ad2antlr 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( #b ` N ) e. NN )
78 77 62 syl 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( ( #b ` N ) - 1 ) e. NN0 )
79 elfzo2 
 |-  ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) <-> ( N e. ( ZZ>= ` ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ) /\ ( 2 ^ ( #b ` N ) ) e. ZZ /\ N < ( 2 ^ ( #b ` N ) ) ) )
80 eluz2 
 |-  ( N e. ( ZZ>= ` ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ) <-> ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) )
81 80 3anbi1i 
 |-  ( ( N e. ( ZZ>= ` ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ) /\ ( 2 ^ ( #b ` N ) ) e. ZZ /\ N < ( 2 ^ ( #b ` N ) ) ) <-> ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ ( 2 ^ ( #b ` N ) ) e. ZZ /\ N < ( 2 ^ ( #b ` N ) ) ) )
82 79 81 bitri 
 |-  ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) <-> ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ ( 2 ^ ( #b ` N ) ) e. ZZ /\ N < ( 2 ^ ( #b ` N ) ) ) )
83 2nn 
 |-  2 e. NN
84 83 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. NN )
85 84 63 jca 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 e. NN /\ ( ( #b ` N ) - 1 ) e. NN0 ) )
86 85 adantl 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 e. NN /\ ( ( #b ` N ) - 1 ) e. NN0 ) )
87 nnexpcl 
 |-  ( ( 2 e. NN /\ ( ( #b ` N ) - 1 ) e. NN0 ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. NN )
88 86 87 syl 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. NN )
89 88 nnzd 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. ZZ )
90 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
91 90 3ad2ant2 
 |-  ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) -> ( N - 1 ) e. ZZ )
92 91 adantr 
 |-  ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) -> ( N - 1 ) e. ZZ )
93 92 adantr 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( N - 1 ) e. ZZ )
94 84 63 nnexpcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. NN )
95 94 nnred 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. RR )
96 1 nnred 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
97 leaddsub 
 |-  ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N <-> ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ ( N - 1 ) ) )
98 95 44 96 97 syl3anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N <-> ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ ( N - 1 ) ) )
99 98 biimpcd 
 |-  ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N -> ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ ( N - 1 ) ) )
100 99 3ad2ant3 
 |-  ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) -> ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ ( N - 1 ) ) )
101 100 adantr 
 |-  ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) -> ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ ( N - 1 ) ) )
102 101 imp 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ ( N - 1 ) )
103 eluz2 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( 2 ^ ( ( #b ` N ) - 1 ) ) ) <-> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) e. ZZ /\ ( N - 1 ) e. ZZ /\ ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ ( N - 1 ) ) )
104 89 93 102 103 syl3anbrc 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( N - 1 ) e. ( ZZ>= ` ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
105 70 eleq1d 
 |-  ( ( #b ` N ) e. CC -> ( ( ( ( #b ` N ) - 1 ) + 1 ) e. NN0 <-> ( #b ` N ) e. NN0 ) )
106 68 105 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( ( #b ` N ) - 1 ) + 1 ) e. NN0 <-> ( #b ` N ) e. NN0 ) )
107 15 106 mpbird 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( #b ` N ) - 1 ) + 1 ) e. NN0 )
108 84 107 jca 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 e. NN /\ ( ( ( #b ` N ) - 1 ) + 1 ) e. NN0 ) )
109 108 adantl 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 e. NN /\ ( ( ( #b ` N ) - 1 ) + 1 ) e. NN0 ) )
110 nnexpcl 
 |-  ( ( 2 e. NN /\ ( ( ( #b ` N ) - 1 ) + 1 ) e. NN0 ) -> ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) e. NN )
111 109 110 syl 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) e. NN )
112 111 nnzd 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) e. ZZ )
113 ltle 
 |-  ( ( N e. RR /\ ( 2 ^ ( #b ` N ) ) e. RR ) -> ( N < ( 2 ^ ( #b ` N ) ) -> N <_ ( 2 ^ ( #b ` N ) ) ) )
114 nnre 
 |-  ( N e. NN -> N e. RR )
115 42 a1i 
 |-  ( N e. NN -> 2 e. RR )
116 115 14 reexpcld 
 |-  ( N e. NN -> ( 2 ^ ( #b ` N ) ) e. RR )
117 114 116 jca 
 |-  ( N e. NN -> ( N e. RR /\ ( 2 ^ ( #b ` N ) ) e. RR ) )
118 1 117 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N e. RR /\ ( 2 ^ ( #b ` N ) ) e. RR ) )
119 113 118 syl11 
 |-  ( N < ( 2 ^ ( #b ` N ) ) -> ( N e. ( ZZ>= ` 2 ) -> N <_ ( 2 ^ ( #b ` N ) ) ) )
120 119 adantl 
 |-  ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) -> ( N e. ( ZZ>= ` 2 ) -> N <_ ( 2 ^ ( #b ` N ) ) ) )
121 120 imp 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> N <_ ( 2 ^ ( #b ` N ) ) )
122 simpll2 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> N e. ZZ )
123 84 15 nnexpcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( #b ` N ) ) e. NN )
124 123 nnzd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( #b ` N ) ) e. ZZ )
125 124 adantl 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 ^ ( #b ` N ) ) e. ZZ )
126 zlem1lt 
 |-  ( ( N e. ZZ /\ ( 2 ^ ( #b ` N ) ) e. ZZ ) -> ( N <_ ( 2 ^ ( #b ` N ) ) <-> ( N - 1 ) < ( 2 ^ ( #b ` N ) ) ) )
127 122 125 126 syl2anc 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( N <_ ( 2 ^ ( #b ` N ) ) <-> ( N - 1 ) < ( 2 ^ ( #b ` N ) ) ) )
128 121 127 mpbid 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( N - 1 ) < ( 2 ^ ( #b ` N ) ) )
129 68 70 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( #b ` N ) - 1 ) + 1 ) = ( #b ` N ) )
130 129 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) = ( 2 ^ ( #b ` N ) ) )
131 130 adantl 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) = ( 2 ^ ( #b ` N ) ) )
132 128 131 breqtrrd 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( N - 1 ) < ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) )
133 104 112 132 3jca 
 |-  ( ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( N - 1 ) e. ( ZZ>= ` ( 2 ^ ( ( #b ` N ) - 1 ) ) ) /\ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) e. ZZ /\ ( N - 1 ) < ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) )
134 133 ex 
 |-  ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ N < ( 2 ^ ( #b ` N ) ) ) -> ( N e. ( ZZ>= ` 2 ) -> ( ( N - 1 ) e. ( ZZ>= ` ( 2 ^ ( ( #b ` N ) - 1 ) ) ) /\ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) e. ZZ /\ ( N - 1 ) < ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) ) )
135 134 3adant2 
 |-  ( ( ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) e. ZZ /\ N e. ZZ /\ ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) <_ N ) /\ ( 2 ^ ( #b ` N ) ) e. ZZ /\ N < ( 2 ^ ( #b ` N ) ) ) -> ( N e. ( ZZ>= ` 2 ) -> ( ( N - 1 ) e. ( ZZ>= ` ( 2 ^ ( ( #b ` N ) - 1 ) ) ) /\ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) e. ZZ /\ ( N - 1 ) < ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) ) )
136 82 135 sylbi 
 |-  ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) -> ( N e. ( ZZ>= ` 2 ) -> ( ( N - 1 ) e. ( ZZ>= ` ( 2 ^ ( ( #b ` N ) - 1 ) ) ) /\ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) e. ZZ /\ ( N - 1 ) < ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) ) )
137 136 imp 
 |-  ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( N - 1 ) e. ( ZZ>= ` ( 2 ^ ( ( #b ` N ) - 1 ) ) ) /\ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) e. ZZ /\ ( N - 1 ) < ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) )
138 elfzo2 
 |-  ( ( N - 1 ) e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) <-> ( ( N - 1 ) e. ( ZZ>= ` ( 2 ^ ( ( #b ` N ) - 1 ) ) ) /\ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) e. ZZ /\ ( N - 1 ) < ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) )
139 137 138 sylibr 
 |-  ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) -> ( N - 1 ) e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) )
140 139 adantr 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( N - 1 ) e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) )
141 fllog2 
 |-  ( ( ( ( #b ` N ) - 1 ) e. NN0 /\ ( N - 1 ) e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( ( ( #b ` N ) - 1 ) + 1 ) ) ) ) -> ( |_ ` ( 2 logb ( N - 1 ) ) ) = ( ( #b ` N ) - 1 ) )
142 78 140 141 syl2anc 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( |_ ` ( 2 logb ( N - 1 ) ) ) = ( ( #b ` N ) - 1 ) )
143 76 142 eqtr4d 
 |-  ( ( ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) /\ N e. ( ZZ>= ` 2 ) ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) )
144 143 exp31 
 |-  ( N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) -> ( N e. ( ZZ>= ` 2 ) -> ( ( ( N + 1 ) / 2 ) e. NN -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) ) ) )
145 60 144 jaoi 
 |-  ( ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) \/ N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) ) -> ( N e. ( ZZ>= ` 2 ) -> ( ( ( N + 1 ) / 2 ) e. NN -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) ) ) )
146 3 145 mpcom 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( N + 1 ) / 2 ) e. NN -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) ) )
147 146 imp 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) )