Metamath Proof Explorer

Theorem blengt1fldiv2p1

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

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

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
2 nneop 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN \/ ( ( N + 1 ) / 2 ) e. NN ) )
3 1 2 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 2 ) e. NN \/ ( ( N + 1 ) / 2 ) e. NN ) )
4 nnnn0 
 |-  ( ( N / 2 ) e. NN -> ( N / 2 ) e. NN0 )
5 blennn0em1 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN0 ) -> ( #b ` ( N / 2 ) ) = ( ( #b ` N ) - 1 ) )
6 4 5 sylan2 
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN ) -> ( #b ` ( N / 2 ) ) = ( ( #b ` N ) - 1 ) )
7 6 ancoms 
 |-  ( ( ( N / 2 ) e. NN /\ N e. NN ) -> ( #b ` ( N / 2 ) ) = ( ( #b ` N ) - 1 ) )
8 7 oveq1d 
 |-  ( ( ( N / 2 ) e. NN /\ N e. NN ) -> ( ( #b ` ( N / 2 ) ) + 1 ) = ( ( ( #b ` N ) - 1 ) + 1 ) )
9 nnz 
 |-  ( ( N / 2 ) e. NN -> ( N / 2 ) e. ZZ )
10 flid 
 |-  ( ( N / 2 ) e. ZZ -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )
11 9 10 syl 
 |-  ( ( N / 2 ) e. NN -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )
12 11 eqcomd 
 |-  ( ( N / 2 ) e. NN -> ( N / 2 ) = ( |_ ` ( N / 2 ) ) )
13 12 fveq2d 
 |-  ( ( N / 2 ) e. NN -> ( #b ` ( N / 2 ) ) = ( #b ` ( |_ ` ( N / 2 ) ) ) )
14 13 oveq1d 
 |-  ( ( N / 2 ) e. NN -> ( ( #b ` ( N / 2 ) ) + 1 ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) )
15 14 adantr 
 |-  ( ( ( N / 2 ) e. NN /\ N e. NN ) -> ( ( #b ` ( N / 2 ) ) + 1 ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) )
16 blennnelnn 
 |-  ( N e. NN -> ( #b ` N ) e. NN )
17 16 nncnd 
 |-  ( N e. NN -> ( #b ` N ) e. CC )
18 npcan1 
 |-  ( ( #b ` N ) e. CC -> ( ( ( #b ` N ) - 1 ) + 1 ) = ( #b ` N ) )
19 17 18 syl 
 |-  ( N e. NN -> ( ( ( #b ` N ) - 1 ) + 1 ) = ( #b ` N ) )
20 19 adantl 
 |-  ( ( ( N / 2 ) e. NN /\ N e. NN ) -> ( ( ( #b ` N ) - 1 ) + 1 ) = ( #b ` N ) )
21 8 15 20 3eqtr3rd 
 |-  ( ( ( N / 2 ) e. NN /\ N e. NN ) -> ( #b ` N ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) )
22 21 expcom 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN -> ( #b ` N ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
23 22 1 syl11 
 |-  ( ( N / 2 ) e. NN -> ( N e. ( ZZ>= ` 2 ) -> ( #b ` N ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
24 nnnn0 
 |-  ( ( ( N + 1 ) / 2 ) e. NN -> ( ( N + 1 ) / 2 ) e. NN0 )
25 blennngt2o2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( #b ` N ) = ( ( #b ` ( ( N - 1 ) / 2 ) ) + 1 ) )
26 24 25 sylan2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( #b ` N ) = ( ( #b ` ( ( N - 1 ) / 2 ) ) + 1 ) )
27 26 ancoms 
 |-  ( ( ( ( N + 1 ) / 2 ) e. NN /\ N e. ( ZZ>= ` 2 ) ) -> ( #b ` N ) = ( ( #b ` ( ( N - 1 ) / 2 ) ) + 1 ) )
28 eluzge2nn0 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
29 nn0ofldiv2 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )
30 28 24 29 syl2anr 
 |-  ( ( ( ( N + 1 ) / 2 ) e. NN /\ N e. ( ZZ>= ` 2 ) ) -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )
31 30 eqcomd 
 |-  ( ( ( ( N + 1 ) / 2 ) e. NN /\ N e. ( ZZ>= ` 2 ) ) -> ( ( N - 1 ) / 2 ) = ( |_ ` ( N / 2 ) ) )
32 31 fveq2d 
 |-  ( ( ( ( N + 1 ) / 2 ) e. NN /\ N e. ( ZZ>= ` 2 ) ) -> ( #b ` ( ( N - 1 ) / 2 ) ) = ( #b ` ( |_ ` ( N / 2 ) ) ) )
33 32 oveq1d 
 |-  ( ( ( ( N + 1 ) / 2 ) e. NN /\ N e. ( ZZ>= ` 2 ) ) -> ( ( #b ` ( ( N - 1 ) / 2 ) ) + 1 ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) )
34 27 33 eqtrd 
 |-  ( ( ( ( N + 1 ) / 2 ) e. NN /\ N e. ( ZZ>= ` 2 ) ) -> ( #b ` N ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) )
35 34 ex 
 |-  ( ( ( N + 1 ) / 2 ) e. NN -> ( N e. ( ZZ>= ` 2 ) -> ( #b ` N ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
36 23 35 jaoi 
 |-  ( ( ( N / 2 ) e. NN \/ ( ( N + 1 ) / 2 ) e. NN ) -> ( N e. ( ZZ>= ` 2 ) -> ( #b ` N ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
37 3 36 mpcom 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( #b ` N ) = ( ( #b ` ( |_ ` ( N / 2 ) ) ) + 1 ) )