Metamath Proof Explorer

Theorem bitsp1o

Description: The M + 1 -th bit of 2 N + 1 is the M -th bit of N . (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bitsp1o ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ ( ( 2 · 𝑁 ) + 1 ) ) ↔ 𝑀 ∈ ( bits ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 1 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℤ )
3 id ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℤ )
4 2 3 zmulcld ⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℤ )
5 4 peano2zd ⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ )
6 bitsp1 ⊢ ( ( ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ ( ( 2 · 𝑁 ) + 1 ) ) ↔ 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ) ) ) )
7 5 6 sylan ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ ( ( 2 · 𝑁 ) + 1 ) ) ↔ 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ) ) ) )
8 2re ⊢ 2 ∈ ℝ
9 8 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℝ )
10 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
11 9 10 remulcld ⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℝ )
12 11 recnd ⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℂ )
13 1cnd ⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℂ )
14 2cnd ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ )
15 2ne0 ⊢ 2 ≠ 0
16 15 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ≠ 0 )
17 12 13 14 16 divdird ⊢ ( 𝑁 ∈ ℤ → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) = ( ( ( 2 · 𝑁 ) / 2 ) + ( 1 / 2 ) ) )
18 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
19 18 14 16 divcan3d ⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 𝑁 ) / 2 ) = 𝑁 )
20 19 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( ( 2 · 𝑁 ) / 2 ) + ( 1 / 2 ) ) = ( 𝑁 + ( 1 / 2 ) ) )
21 17 20 eqtrd ⊢ ( 𝑁 ∈ ℤ → ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) = ( 𝑁 + ( 1 / 2 ) ) )
22 21 fveq2d ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ) = ( ⌊ ‘ ( 𝑁 + ( 1 / 2 ) ) ) )
23 halfge0 ⊢ 0 ≤ ( 1 / 2 )
24 halflt1 ⊢ ( 1 / 2 ) < 1
25 23 24 pm3.2i ⊢ ( 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 )
26 halfre ⊢ ( 1 / 2 ) ∈ ℝ
27 flbi2 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 𝑁 + ( 1 / 2 ) ) ) = 𝑁 ↔ ( 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) ) )
28 26 27 mpan2 ⊢ ( 𝑁 ∈ ℤ → ( ( ⌊ ‘ ( 𝑁 + ( 1 / 2 ) ) ) = 𝑁 ↔ ( 0 ≤ ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) ) )
29 25 28 mpbiri ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( 𝑁 + ( 1 / 2 ) ) ) = 𝑁 )
30 22 29 eqtrd ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ) = 𝑁 )
31 30 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ) = 𝑁 )
32 31 fveq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( bits ‘ ( ⌊ ‘ ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ) ) = ( bits ‘ 𝑁 ) )
33 32 eleq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( ( ( 2 · 𝑁 ) + 1 ) / 2 ) ) ) ↔ 𝑀 ∈ ( bits ‘ 𝑁 ) ) )
34 7 33 bitrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ ( ( 2 · 𝑁 ) + 1 ) ) ↔ 𝑀 ∈ ( bits ‘ 𝑁 ) ) )