Metamath Proof Explorer

Theorem blennn0e2

Description: The binary length of an even positive integer is the binary length of the half of the integer, increased by 1. (Contributed by AV, 29-May-2020)

Ref Expression
Assertion blennn0e2 
|- ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( #b ` N ) = ( ( #b ` ( N / 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 nnrp 
 |-  ( N e. NN -> N e. RR+ )
7 6 adantr 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> N e. RR+ )
8 relogbdivb 
 |-  ( ( 2 e. ( RR+ \ { 1 } ) /\ N e. RR+ ) -> ( 2 logb ( N / 2 ) ) = ( ( 2 logb N ) - 1 ) )
9 5 7 8 sylancr 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( 2 logb ( N / 2 ) ) = ( ( 2 logb N ) - 1 ) )
10 9 fveq2d 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( |_ ` ( 2 logb ( N / 2 ) ) ) = ( |_ ` ( ( 2 logb N ) - 1 ) ) )
11 10 oveq1d 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( |_ ` ( 2 logb ( N / 2 ) ) ) + 1 ) = ( ( |_ ` ( ( 2 logb N ) - 1 ) ) + 1 ) )
12 1 a1i 
 |-  ( N e. NN -> 2 e. RR+ )
13 3 a1i 
 |-  ( N e. NN -> 2 =/= 1 )
14 relogbcl 
 |-  ( ( 2 e. RR+ /\ N e. RR+ /\ 2 =/= 1 ) -> ( 2 logb N ) e. RR )
15 12 6 13 14 syl3anc 
 |-  ( N e. NN -> ( 2 logb N ) e. RR )
16 1zzd 
 |-  ( N e. NN -> 1 e. ZZ )
17 15 16 jca 
 |-  ( N e. NN -> ( ( 2 logb N ) e. RR /\ 1 e. ZZ ) )
18 17 adantr 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( 2 logb N ) e. RR /\ 1 e. ZZ ) )
19 flsubz 
 |-  ( ( ( 2 logb N ) e. RR /\ 1 e. ZZ ) -> ( |_ ` ( ( 2 logb N ) - 1 ) ) = ( ( |_ ` ( 2 logb N ) ) - 1 ) )
20 18 19 syl 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( |_ ` ( ( 2 logb N ) - 1 ) ) = ( ( |_ ` ( 2 logb N ) ) - 1 ) )
21 20 oveq1d 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( |_ ` ( ( 2 logb N ) - 1 ) ) + 1 ) = ( ( ( |_ ` ( 2 logb N ) ) - 1 ) + 1 ) )
22 15 flcld 
 |-  ( N e. NN -> ( |_ ` ( 2 logb N ) ) e. ZZ )
23 22 zcnd 
 |-  ( N e. NN -> ( |_ ` ( 2 logb N ) ) e. CC )
24 npcan1 
 |-  ( ( |_ ` ( 2 logb N ) ) e. CC -> ( ( ( |_ ` ( 2 logb N ) ) - 1 ) + 1 ) = ( |_ ` ( 2 logb N ) ) )
25 23 24 syl 
 |-  ( N e. NN -> ( ( ( |_ ` ( 2 logb N ) ) - 1 ) + 1 ) = ( |_ ` ( 2 logb N ) ) )
26 25 adantr 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( ( |_ ` ( 2 logb N ) ) - 1 ) + 1 ) = ( |_ ` ( 2 logb N ) ) )
27 11 21 26 3eqtrd 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( |_ ` ( 2 logb ( N / 2 ) ) ) + 1 ) = ( |_ ` ( 2 logb N ) ) )
28 27 oveq1d 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( ( |_ ` ( 2 logb ( N / 2 ) ) ) + 1 ) + 1 ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
29 nn0enne 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )
30 29 biimpa 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( N / 2 ) e. NN )
31 blennn 
 |-  ( ( N / 2 ) e. NN -> ( #b ` ( N / 2 ) ) = ( ( |_ ` ( 2 logb ( N / 2 ) ) ) + 1 ) )
32 31 oveq1d 
 |-  ( ( N / 2 ) e. NN -> ( ( #b ` ( N / 2 ) ) + 1 ) = ( ( ( |_ ` ( 2 logb ( N / 2 ) ) ) + 1 ) + 1 ) )
33 30 32 syl 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( #b ` ( N / 2 ) ) + 1 ) = ( ( ( |_ ` ( 2 logb ( N / 2 ) ) ) + 1 ) + 1 ) )
34 blennn 
 |-  ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
35 34 adantr 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
36 28 33 35 3eqtr4rd 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( #b ` N ) = ( ( #b ` ( N / 2 ) ) + 1 ) )