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 ) )