Metamath Proof Explorer

Theorem blennngt2o2

Description: The binary length of an odd integer greater than 1 is the binary length of the half of the integer decreased by 1, increased by 1. (Contributed by AV, 3-Jun-2020)

Ref Expression
Assertion blennngt2o2 
|- ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( #b ` N ) = ( ( #b ` ( ( N - 1 ) / 2 ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 2rp 
 |-  2 e. RR+
2 1ne2 
 |-  1 =/= 2
3 2 necomi 
 |-  2 =/= 1
4 eldifsn 
 |-  ( 2 e. ( RR+ \ { 1 } ) <-> ( 2 e. RR+ /\ 2 =/= 1 ) )
5 1 3 4 mpbir2an 
 |-  2 e. ( RR+ \ { 1 } )
6 uz2m1nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
7 6 nnrpd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. RR+ )
8 7 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N - 1 ) e. RR+ )
9 relogbdivb 
 |-  ( ( 2 e. ( RR+ \ { 1 } ) /\ ( N - 1 ) e. RR+ ) -> ( 2 logb ( ( N - 1 ) / 2 ) ) = ( ( 2 logb ( N - 1 ) ) - 1 ) )
10 5 8 9 sylancr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( 2 logb ( ( N - 1 ) / 2 ) ) = ( ( 2 logb ( N - 1 ) ) - 1 ) )
11 10 fveq2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( 2 logb ( ( N - 1 ) / 2 ) ) ) = ( |_ ` ( ( 2 logb ( N - 1 ) ) - 1 ) ) )
12 11 oveq1d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( |_ ` ( 2 logb ( ( N - 1 ) / 2 ) ) ) + 1 ) = ( ( |_ ` ( ( 2 logb ( N - 1 ) ) - 1 ) ) + 1 ) )
13 1 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. RR+ )
14 3 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 =/= 1 )
15 relogbcl 
 |-  ( ( 2 e. RR+ /\ ( N - 1 ) e. RR+ /\ 2 =/= 1 ) -> ( 2 logb ( N - 1 ) ) e. RR )
16 13 7 14 15 syl3anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 logb ( N - 1 ) ) e. RR )
17 1z 
 |-  1 e. ZZ
18 16 17 jctir 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( 2 logb ( N - 1 ) ) e. RR /\ 1 e. ZZ ) )
19 18 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( 2 logb ( N - 1 ) ) e. RR /\ 1 e. ZZ ) )
20 flsubz 
 |-  ( ( ( 2 logb ( N - 1 ) ) e. RR /\ 1 e. ZZ ) -> ( |_ ` ( ( 2 logb ( N - 1 ) ) - 1 ) ) = ( ( |_ ` ( 2 logb ( N - 1 ) ) ) - 1 ) )
21 19 20 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( ( 2 logb ( N - 1 ) ) - 1 ) ) = ( ( |_ ` ( 2 logb ( N - 1 ) ) ) - 1 ) )
22 21 oveq1d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( |_ ` ( ( 2 logb ( N - 1 ) ) - 1 ) ) + 1 ) = ( ( ( |_ ` ( 2 logb ( N - 1 ) ) ) - 1 ) + 1 ) )
23 16 flcld 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( 2 logb ( N - 1 ) ) ) e. ZZ )
24 23 zcnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( 2 logb ( N - 1 ) ) ) e. CC )
25 npcan1 
 |-  ( ( |_ ` ( 2 logb ( N - 1 ) ) ) e. CC -> ( ( ( |_ ` ( 2 logb ( N - 1 ) ) ) - 1 ) + 1 ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) )
26 24 25 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( |_ ` ( 2 logb ( N - 1 ) ) ) - 1 ) + 1 ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) )
27 26 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( ( |_ ` ( 2 logb ( N - 1 ) ) ) - 1 ) + 1 ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) )
28 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
29 28 peano2nnd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N + 1 ) e. NN )
30 29 nnred 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N + 1 ) e. RR )
31 2re 
 |-  2 e. RR
32 31 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. RR )
33 eluzge2nn0 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
34 nn0p1gt0 
 |-  ( N e. NN0 -> 0 < ( N + 1 ) )
35 33 34 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 < ( N + 1 ) )
36 2pos 
 |-  0 < 2
37 36 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 < 2 )
38 30 32 35 37 divgt0d 
 |-  ( N e. ( ZZ>= ` 2 ) -> 0 < ( ( N + 1 ) / 2 ) )
39 nn0z 
 |-  ( ( ( N + 1 ) / 2 ) e. NN0 -> ( ( N + 1 ) / 2 ) e. ZZ )
40 38 39 anim12ci 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( ( N + 1 ) / 2 ) e. ZZ /\ 0 < ( ( N + 1 ) / 2 ) ) )
41 elnnz 
 |-  ( ( ( N + 1 ) / 2 ) e. NN <-> ( ( ( N + 1 ) / 2 ) e. ZZ /\ 0 < ( ( N + 1 ) / 2 ) ) )
42 40 41 sylibr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N + 1 ) / 2 ) e. NN )
43 nnolog2flm1 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) )
44 42 43 syldan 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( 2 logb N ) ) = ( |_ ` ( 2 logb ( N - 1 ) ) ) )
45 27 44 eqtr4d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( ( |_ ` ( 2 logb ( N - 1 ) ) ) - 1 ) + 1 ) = ( |_ ` ( 2 logb N ) ) )
46 12 22 45 3eqtrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( |_ ` ( 2 logb ( ( N - 1 ) / 2 ) ) ) + 1 ) = ( |_ ` ( 2 logb N ) ) )
47 46 oveq1d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( ( |_ ` ( 2 logb ( ( N - 1 ) / 2 ) ) ) + 1 ) + 1 ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
48 nno 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN )
49 blennn 
 |-  ( ( ( N - 1 ) / 2 ) e. NN -> ( #b ` ( ( N - 1 ) / 2 ) ) = ( ( |_ ` ( 2 logb ( ( N - 1 ) / 2 ) ) ) + 1 ) )
50 49 oveq1d 
 |-  ( ( ( N - 1 ) / 2 ) e. NN -> ( ( #b ` ( ( N - 1 ) / 2 ) ) + 1 ) = ( ( ( |_ ` ( 2 logb ( ( N - 1 ) / 2 ) ) ) + 1 ) + 1 ) )
51 48 50 syl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( #b ` ( ( N - 1 ) / 2 ) ) + 1 ) = ( ( ( |_ ` ( 2 logb ( ( N - 1 ) / 2 ) ) ) + 1 ) + 1 ) )
52 blennn 
 |-  ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
53 28 52 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
54 53 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
55 47 51 54 3eqtr4rd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( #b ` N ) = ( ( #b ` ( ( N - 1 ) / 2 ) ) + 1 ) )