Metamath Proof Explorer

Theorem blennnt2

Description: The binary length of a positive integer, doubled and increased by 1, is the binary length of the integer plus 1. (Contributed by AV, 30-May-2010)

Ref Expression
Assertion blennnt2 
|- ( N e. NN -> ( #b ` ( 2 x. N ) ) = ( ( #b ` N ) + 1 ) )

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 1 a1i 
 |-  ( N e. NN -> 2 e. NN )
3 id 
 |-  ( N e. NN -> N e. NN )
4 2 3 nnmulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. NN )
5 blennn 
 |-  ( ( 2 x. N ) e. NN -> ( #b ` ( 2 x. N ) ) = ( ( |_ ` ( 2 logb ( 2 x. N ) ) ) + 1 ) )
6 4 5 syl 
 |-  ( N e. NN -> ( #b ` ( 2 x. N ) ) = ( ( |_ ` ( 2 logb ( 2 x. N ) ) ) + 1 ) )
7 2cn 
 |-  2 e. CC
8 7 a1i 
 |-  ( N e. NN -> 2 e. CC )
9 nncn 
 |-  ( N e. NN -> N e. CC )
10 8 9 mulcomd 
 |-  ( N e. NN -> ( 2 x. N ) = ( N x. 2 ) )
11 10 oveq2d 
 |-  ( N e. NN -> ( 2 logb ( 2 x. N ) ) = ( 2 logb ( N x. 2 ) ) )
12 2z 
 |-  2 e. ZZ
13 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
14 12 13 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
15 eluz2cnn0n1 
 |-  ( 2 e. ( ZZ>= ` 2 ) -> 2 e. ( CC \ { 0 , 1 } ) )
16 14 15 mp1i 
 |-  ( N e. NN -> 2 e. ( CC \ { 0 , 1 } ) )
17 nnrp 
 |-  ( N e. NN -> N e. RR+ )
18 2rp 
 |-  2 e. RR+
19 18 a1i 
 |-  ( N e. NN -> 2 e. RR+ )
20 relogbmul 
 |-  ( ( 2 e. ( CC \ { 0 , 1 } ) /\ ( N e. RR+ /\ 2 e. RR+ ) ) -> ( 2 logb ( N x. 2 ) ) = ( ( 2 logb N ) + ( 2 logb 2 ) ) )
21 16 17 19 20 syl12anc 
 |-  ( N e. NN -> ( 2 logb ( N x. 2 ) ) = ( ( 2 logb N ) + ( 2 logb 2 ) ) )
22 2ne0 
 |-  2 =/= 0
23 1ne2 
 |-  1 =/= 2
24 23 necomi 
 |-  2 =/= 1
25 7 22 24 3pm3.2i 
 |-  ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 )
26 logbid1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 2 ) = 1 )
27 25 26 mp1i 
 |-  ( N e. NN -> ( 2 logb 2 ) = 1 )
28 27 oveq2d 
 |-  ( N e. NN -> ( ( 2 logb N ) + ( 2 logb 2 ) ) = ( ( 2 logb N ) + 1 ) )
29 11 21 28 3eqtrd 
 |-  ( N e. NN -> ( 2 logb ( 2 x. N ) ) = ( ( 2 logb N ) + 1 ) )
30 29 fveq2d 
 |-  ( N e. NN -> ( |_ ` ( 2 logb ( 2 x. N ) ) ) = ( |_ ` ( ( 2 logb N ) + 1 ) ) )
31 24 a1i 
 |-  ( N e. NN -> 2 =/= 1 )
32 relogbcl 
 |-  ( ( 2 e. RR+ /\ N e. RR+ /\ 2 =/= 1 ) -> ( 2 logb N ) e. RR )
33 19 17 31 32 syl3anc 
 |-  ( N e. NN -> ( 2 logb N ) e. RR )
34 1zzd 
 |-  ( N e. NN -> 1 e. ZZ )
35 fladdz 
 |-  ( ( ( 2 logb N ) e. RR /\ 1 e. ZZ ) -> ( |_ ` ( ( 2 logb N ) + 1 ) ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
36 33 34 35 syl2anc 
 |-  ( N e. NN -> ( |_ ` ( ( 2 logb N ) + 1 ) ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
37 30 36 eqtrd 
 |-  ( N e. NN -> ( |_ ` ( 2 logb ( 2 x. N ) ) ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
38 37 oveq1d 
 |-  ( N e. NN -> ( ( |_ ` ( 2 logb ( 2 x. N ) ) ) + 1 ) = ( ( ( |_ ` ( 2 logb N ) ) + 1 ) + 1 ) )
39 blennn 
 |-  ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
40 39 eqcomd 
 |-  ( N e. NN -> ( ( |_ ` ( 2 logb N ) ) + 1 ) = ( #b ` N ) )
41 40 oveq1d 
 |-  ( N e. NN -> ( ( ( |_ ` ( 2 logb N ) ) + 1 ) + 1 ) = ( ( #b ` N ) + 1 ) )
42 6 38 41 3eqtrd 
 |-  ( N e. NN -> ( #b ` ( 2 x. N ) ) = ( ( #b ` N ) + 1 ) )