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 ( 𝑁 ∈ ℕ → ( #b ‘ ( 2 · 𝑁 ) ) = ( ( #b𝑁 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 2nn 2 ∈ ℕ
2 1 a1i ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
3 id ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
4 2 3 nnmulcld ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℕ )
5 blennn ( ( 2 · 𝑁 ) ∈ ℕ → ( #b ‘ ( 2 · 𝑁 ) ) = ( ( ⌊ ‘ ( 2 logb ( 2 · 𝑁 ) ) ) + 1 ) )
6 4 5 syl ( 𝑁 ∈ ℕ → ( #b ‘ ( 2 · 𝑁 ) ) = ( ( ⌊ ‘ ( 2 logb ( 2 · 𝑁 ) ) ) + 1 ) )
7 2cn 2 ∈ ℂ
8 7 a1i ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
9 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
10 8 9 mulcomd ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) = ( 𝑁 · 2 ) )
11 10 oveq2d ( 𝑁 ∈ ℕ → ( 2 logb ( 2 · 𝑁 ) ) = ( 2 logb ( 𝑁 · 2 ) ) )
12 2z 2 ∈ ℤ
13 uzid ( 2 ∈ ℤ → 2 ∈ ( ℤ ‘ 2 ) )
14 12 13 ax-mp 2 ∈ ( ℤ ‘ 2 )
15 eluz2cnn0n1 ( 2 ∈ ( ℤ ‘ 2 ) → 2 ∈ ( ℂ ∖ { 0 , 1 } ) )
16 14 15 mp1i ( 𝑁 ∈ ℕ → 2 ∈ ( ℂ ∖ { 0 , 1 } ) )
17 nnrp ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
18 2rp 2 ∈ ℝ+
19 18 a1i ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
20 relogbmul ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝑁 ∈ ℝ+ ∧ 2 ∈ ℝ+ ) ) → ( 2 logb ( 𝑁 · 2 ) ) = ( ( 2 logb 𝑁 ) + ( 2 logb 2 ) ) )
21 16 17 19 20 syl12anc ( 𝑁 ∈ ℕ → ( 2 logb ( 𝑁 · 2 ) ) = ( ( 2 logb 𝑁 ) + ( 2 logb 2 ) ) )
22 2ne0 2 ≠ 0
23 1ne2 1 ≠ 2
24 23 necomi 2 ≠ 1
25 7 22 24 3pm3.2i ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 )
26 logbid1 ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 2 ) = 1 )
27 25 26 mp1i ( 𝑁 ∈ ℕ → ( 2 logb 2 ) = 1 )
28 27 oveq2d ( 𝑁 ∈ ℕ → ( ( 2 logb 𝑁 ) + ( 2 logb 2 ) ) = ( ( 2 logb 𝑁 ) + 1 ) )
29 11 21 28 3eqtrd ( 𝑁 ∈ ℕ → ( 2 logb ( 2 · 𝑁 ) ) = ( ( 2 logb 𝑁 ) + 1 ) )
30 29 fveq2d ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb ( 2 · 𝑁 ) ) ) = ( ⌊ ‘ ( ( 2 logb 𝑁 ) + 1 ) ) )
31 24 a1i ( 𝑁 ∈ ℕ → 2 ≠ 1 )
32 relogbcl ( ( 2 ∈ ℝ+𝑁 ∈ ℝ+ ∧ 2 ≠ 1 ) → ( 2 logb 𝑁 ) ∈ ℝ )
33 19 17 31 32 syl3anc ( 𝑁 ∈ ℕ → ( 2 logb 𝑁 ) ∈ ℝ )
34 1zzd ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
35 fladdz ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( ( 2 logb 𝑁 ) + 1 ) ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
36 33 34 35 syl2anc ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( ( 2 logb 𝑁 ) + 1 ) ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
37 30 36 eqtrd ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb ( 2 · 𝑁 ) ) ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
38 37 oveq1d ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb ( 2 · 𝑁 ) ) ) + 1 ) = ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) + 1 ) )
39 blennn ( 𝑁 ∈ ℕ → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
40 39 eqcomd ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) = ( #b𝑁 ) )
41 40 oveq1d ( 𝑁 ∈ ℕ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) + 1 ) = ( ( #b𝑁 ) + 1 ) )
42 6 38 41 3eqtrd ( 𝑁 ∈ ℕ → ( #b ‘ ( 2 · 𝑁 ) ) = ( ( #b𝑁 ) + 1 ) )