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 ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M + 1 ∈ bits ⁡ 2 ⋅ N + 1 ↔ M ∈ bits ⁡ N

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 1 a1i ⊢ N ∈ ℤ → 2 ∈ ℤ
3 id ⊢ N ∈ ℤ → N ∈ ℤ
4 2 3 zmulcld ⊢ N ∈ ℤ → 2 ⋅ N ∈ ℤ
5 4 peano2zd ⊢ N ∈ ℤ → 2 ⋅ N + 1 ∈ ℤ
6 bitsp1 ⊢ 2 ⋅ N + 1 ∈ ℤ ∧ M ∈ ℕ 0 → M + 1 ∈ bits ⁡ 2 ⋅ N + 1 ↔ M ∈ bits ⁡ 2 ⋅ N + 1 2
7 5 6 sylan ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M + 1 ∈ bits ⁡ 2 ⋅ N + 1 ↔ M ∈ bits ⁡ 2 ⋅ N + 1 2
8 2re ⊢ 2 ∈ ℝ
9 8 a1i ⊢ N ∈ ℤ → 2 ∈ ℝ
10 zre ⊢ N ∈ ℤ → N ∈ ℝ
11 9 10 remulcld ⊢ N ∈ ℤ → 2 ⋅ N ∈ ℝ
12 11 recnd ⊢ N ∈ ℤ → 2 ⋅ N ∈ ℂ
13 1cnd ⊢ N ∈ ℤ → 1 ∈ ℂ
14 2cnd ⊢ N ∈ ℤ → 2 ∈ ℂ
15 2ne0 ⊢ 2 ≠ 0
16 15 a1i ⊢ N ∈ ℤ → 2 ≠ 0
17 12 13 14 16 divdird ⊢ N ∈ ℤ → 2 ⋅ N + 1 2 = 2 ⋅ N 2 + 1 2
18 zcn ⊢ N ∈ ℤ → N ∈ ℂ
19 18 14 16 divcan3d ⊢ N ∈ ℤ → 2 ⋅ N 2 = N
20 19 oveq1d ⊢ N ∈ ℤ → 2 ⋅ N 2 + 1 2 = N + 1 2
21 17 20 eqtrd ⊢ N ∈ ℤ → 2 ⋅ N + 1 2 = N + 1 2
22 21 fveq2d ⊢ N ∈ ℤ → 2 ⋅ N + 1 2 = N + 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 ⊢ N ∈ ℤ ∧ 1 2 ∈ ℝ → N + 1 2 = N ↔ 0 ≤ 1 2 ∧ 1 2 < 1
28 26 27 mpan2 ⊢ N ∈ ℤ → N + 1 2 = N ↔ 0 ≤ 1 2 ∧ 1 2 < 1
29 25 28 mpbiri ⊢ N ∈ ℤ → N + 1 2 = N
30 22 29 eqtrd ⊢ N ∈ ℤ → 2 ⋅ N + 1 2 = N
31 30 adantr ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → 2 ⋅ N + 1 2 = N
32 31 fveq2d ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → bits ⁡ 2 ⋅ N + 1 2 = bits ⁡ N
33 32 eleq2d ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M ∈ bits ⁡ 2 ⋅ N + 1 2 ↔ M ∈ bits ⁡ N
34 7 33 bitrd ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M + 1 ∈ bits ⁡ 2 ⋅ N + 1 ↔ M ∈ bits ⁡ N