Metamath Proof Explorer


Theorem blennngt2o2

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

Ref Expression
Assertion blennngt2o2 ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( #b𝑁 ) = ( ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 2rp 2 ∈ ℝ+
2 1ne2 1 ≠ 2
3 2 necomi 2 ≠ 1
4 eldifsn ( 2 ∈ ( ℝ+ ∖ { 1 } ) ↔ ( 2 ∈ ℝ+ ∧ 2 ≠ 1 ) )
5 1 3 4 mpbir2an 2 ∈ ( ℝ+ ∖ { 1 } )
6 uz2m1nn ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ )
7 6 nnrpd ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℝ+ )
8 7 adantr ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 − 1 ) ∈ ℝ+ )
9 relogbdivb ( ( 2 ∈ ( ℝ+ ∖ { 1 } ) ∧ ( 𝑁 − 1 ) ∈ ℝ+ ) → ( 2 logb ( ( 𝑁 − 1 ) / 2 ) ) = ( ( 2 logb ( 𝑁 − 1 ) ) − 1 ) )
10 5 8 9 sylancr ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 2 logb ( ( 𝑁 − 1 ) / 2 ) ) = ( ( 2 logb ( 𝑁 − 1 ) ) − 1 ) )
11 10 fveq2d ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( 2 logb ( ( 𝑁 − 1 ) / 2 ) ) ) = ( ⌊ ‘ ( ( 2 logb ( 𝑁 − 1 ) ) − 1 ) ) )
12 11 oveq1d ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( 2 logb ( ( 𝑁 − 1 ) / 2 ) ) ) + 1 ) = ( ( ⌊ ‘ ( ( 2 logb ( 𝑁 − 1 ) ) − 1 ) ) + 1 ) )
13 1 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → 2 ∈ ℝ+ )
14 3 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → 2 ≠ 1 )
15 relogbcl ( ( 2 ∈ ℝ+ ∧ ( 𝑁 − 1 ) ∈ ℝ+ ∧ 2 ≠ 1 ) → ( 2 logb ( 𝑁 − 1 ) ) ∈ ℝ )
16 13 7 14 15 syl3anc ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 2 logb ( 𝑁 − 1 ) ) ∈ ℝ )
17 1z 1 ∈ ℤ
18 16 17 jctir ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( 2 logb ( 𝑁 − 1 ) ) ∈ ℝ ∧ 1 ∈ ℤ ) )
19 18 adantr ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 2 logb ( 𝑁 − 1 ) ) ∈ ℝ ∧ 1 ∈ ℤ ) )
20 flsubz ( ( ( 2 logb ( 𝑁 − 1 ) ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( ( 2 logb ( 𝑁 − 1 ) ) − 1 ) ) = ( ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) − 1 ) )
21 19 20 syl ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( ( 2 logb ( 𝑁 − 1 ) ) − 1 ) ) = ( ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) − 1 ) )
22 21 oveq1d ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( ( 2 logb ( 𝑁 − 1 ) ) − 1 ) ) + 1 ) = ( ( ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) − 1 ) + 1 ) )
23 16 flcld ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) ∈ ℤ )
24 23 zcnd ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) ∈ ℂ )
25 npcan1 ( ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) ∈ ℂ → ( ( ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) − 1 ) + 1 ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) )
26 24 25 syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( ( ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) − 1 ) + 1 ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) )
27 26 adantr ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) − 1 ) + 1 ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) )
28 eluz2nn ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℕ )
29 28 peano2nnd ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 + 1 ) ∈ ℕ )
30 29 nnred ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 + 1 ) ∈ ℝ )
31 2re 2 ∈ ℝ
32 31 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → 2 ∈ ℝ )
33 eluzge2nn0 ( 𝑁 ∈ ( ℤ ‘ 2 ) → 𝑁 ∈ ℕ0 )
34 nn0p1gt0 ( 𝑁 ∈ ℕ0 → 0 < ( 𝑁 + 1 ) )
35 33 34 syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → 0 < ( 𝑁 + 1 ) )
36 2pos 0 < 2
37 36 a1i ( 𝑁 ∈ ( ℤ ‘ 2 ) → 0 < 2 )
38 30 32 35 37 divgt0d ( 𝑁 ∈ ( ℤ ‘ 2 ) → 0 < ( ( 𝑁 + 1 ) / 2 ) )
39 nn0z ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
40 38 39 anim12ci ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 < ( ( 𝑁 + 1 ) / 2 ) ) )
41 elnnz ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ↔ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 < ( ( 𝑁 + 1 ) / 2 ) ) )
42 40 41 sylibr ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ )
43 nnolog2flm1 ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) )
44 42 43 syldan ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) )
45 27 44 eqtr4d ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) − 1 ) + 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
46 12 22 45 3eqtrd ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( 2 logb ( ( 𝑁 − 1 ) / 2 ) ) ) + 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
47 46 oveq1d ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ( ⌊ ‘ ( 2 logb ( ( 𝑁 − 1 ) / 2 ) ) ) + 1 ) + 1 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
48 nno ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ )
49 blennn ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ → ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) = ( ( ⌊ ‘ ( 2 logb ( ( 𝑁 − 1 ) / 2 ) ) ) + 1 ) )
50 49 oveq1d ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ → ( ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) = ( ( ( ⌊ ‘ ( 2 logb ( ( 𝑁 − 1 ) / 2 ) ) ) + 1 ) + 1 ) )
51 48 50 syl ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) = ( ( ( ⌊ ‘ ( 2 logb ( ( 𝑁 − 1 ) / 2 ) ) ) + 1 ) + 1 ) )
52 blennn ( 𝑁 ∈ ℕ → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
53 28 52 syl ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
54 53 adantr ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
55 47 51 54 3eqtr4rd ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( #b𝑁 ) = ( ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) )