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