Metamath Proof Explorer

Theorem bitsp1e

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

Ref Expression
Assertion bitsp1e ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M + 1 ∈ bits ⁡ 2 ⋅ N ↔ 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 bitsp1 ⊢ 2 ⋅ N ∈ ℤ ∧ M ∈ ℕ 0 → M + 1 ∈ bits ⁡ 2 ⋅ N ↔ M ∈ bits ⁡ 2 ⋅ N 2
6 4 5 sylan ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M + 1 ∈ bits ⁡ 2 ⋅ N ↔ M ∈ bits ⁡ 2 ⋅ N 2
7 zcn ⊢ N ∈ ℤ → N ∈ ℂ
8 2cnd ⊢ N ∈ ℤ → 2 ∈ ℂ
9 2ne0 ⊢ 2 ≠ 0
10 9 a1i ⊢ N ∈ ℤ → 2 ≠ 0
11 7 8 10 divcan3d ⊢ N ∈ ℤ → 2 ⋅ N 2 = N
12 11 fveq2d ⊢ N ∈ ℤ → 2 ⋅ N 2 = N
13 flid ⊢ N ∈ ℤ → N = N
14 12 13 eqtrd ⊢ N ∈ ℤ → 2 ⋅ N 2 = N
15 14 adantr ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → 2 ⋅ N 2 = N
16 15 fveq2d ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → bits ⁡ 2 ⋅ N 2 = bits ⁡ N
17 16 eleq2d ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M ∈ bits ⁡ 2 ⋅ N 2 ↔ M ∈ bits ⁡ N
18 6 17 bitrd ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M + 1 ∈ bits ⁡ 2 ⋅ N ↔ M ∈ bits ⁡ N