Metamath Proof Explorer

Theorem blennn0em1

Description: The binary length of the half of an even positive integer is the binary length of the integer minus 1. (Contributed by AV, 30-May-2010)

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

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( N e. NN -> N e. CC )
2 2cnd 
 |-  ( N e. NN -> 2 e. CC )
3 2ne0 
 |-  2 =/= 0
4 3 a1i 
 |-  ( N e. NN -> 2 =/= 0 )
5 1 2 4 3jca 
 |-  ( N e. NN -> ( N e. CC /\ 2 e. CC /\ 2 =/= 0 ) )
6 5 adantr 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( N e. CC /\ 2 e. CC /\ 2 =/= 0 ) )
7 divcan2 
 |-  ( ( N e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( N / 2 ) ) = N )
8 7 eqcomd 
 |-  ( ( N e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> N = ( 2 x. ( N / 2 ) ) )
9 6 8 syl 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> N = ( 2 x. ( N / 2 ) ) )
10 9 fveq2d 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( #b ` N ) = ( #b ` ( 2 x. ( N / 2 ) ) ) )
11 nn0enne 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )
12 11 biimpa 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( N / 2 ) e. NN )
13 blennnt2 
 |-  ( ( N / 2 ) e. NN -> ( #b ` ( 2 x. ( N / 2 ) ) ) = ( ( #b ` ( N / 2 ) ) + 1 ) )
14 12 13 syl 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( #b ` ( 2 x. ( N / 2 ) ) ) = ( ( #b ` ( N / 2 ) ) + 1 ) )
15 10 14 eqtr2d 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( #b ` ( N / 2 ) ) + 1 ) = ( #b ` N ) )
16 blennnelnn 
 |-  ( N e. NN -> ( #b ` N ) e. NN )
17 16 nncnd 
 |-  ( N e. NN -> ( #b ` N ) e. CC )
18 17 adantr 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( #b ` N ) e. CC )
19 1cnd 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> 1 e. CC )
20 blennn0elnn 
 |-  ( ( N / 2 ) e. NN0 -> ( #b ` ( N / 2 ) ) e. NN )
21 20 nncnd 
 |-  ( ( N / 2 ) e. NN0 -> ( #b ` ( N / 2 ) ) e. CC )
22 21 adantl 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( #b ` ( N / 2 ) ) e. CC )
23 18 19 22 subadd2d 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( ( #b ` N ) - 1 ) = ( #b ` ( N / 2 ) ) <-> ( ( #b ` ( N / 2 ) ) + 1 ) = ( #b ` N ) ) )
24 15 23 mpbird 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( ( #b ` N ) - 1 ) = ( #b ` ( N / 2 ) ) )
25 24 eqcomd 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( #b ` ( N / 2 ) ) = ( ( #b ` N ) - 1 ) )