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+12
7 5 6 sylan ⊢N∈ℤ∧M∈ℕ0→M+1∈bits⁡2⋅ N+1↔M∈bits⁡2⋅ N+12
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+12=2⋅ N2+12
18 zcn ⊢N∈ℤ→N∈ℂ
19 18 14 16 divcan3d ⊢N∈ℤ→2⋅ N2=N
20 19 oveq1d ⊢N∈ℤ→2⋅ N2+12=N+12
21 17 20 eqtrd ⊢N∈ℤ→2⋅ N+12=N+12
22 21 fveq2d ⊢N∈ℤ→2⋅ N+12=N+12
23 halfge0 ⊢0≤12
24 halflt1 ⊢12<1
25 23 24 pm3.2i ⊢0≤12∧12<1
26 halfre ⊢12∈ℝ
27 flbi2 ⊢N∈ℤ∧12∈ℝ→N+12=N↔0≤12∧12<1
28 26 27 mpan2 ⊢N∈ℤ→N+12=N↔0≤12∧12<1
29 25 28 mpbiri ⊢N∈ℤ→N+12=N
30 22 29 eqtrd ⊢N∈ℤ→2⋅ N+12=N
31 30 adantr ⊢N∈ℤ∧M∈ℕ0→2⋅ N+12=N
32 31 fveq2d ⊢N∈ℤ∧M∈ℕ0→bits⁡2⋅ N+12=bits⁡N
33 32 eleq2d ⊢N∈ℤ∧M∈ℕ0→M∈bits⁡2⋅ N+12↔M∈bits⁡N
34 7 33 bitrd ⊢N∈ℤ∧M∈ℕ0→M+1∈bits⁡2⋅ N+1↔M∈bits⁡N