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