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	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ ( 2 · 𝑁 ) ) ↔ 𝑀 ∈ ( bits ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2	1	a1i	⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℤ )
3		id	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℤ )
4	2 3	zmulcld	⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℤ )
5		bitsp1	⊢ ( ( ( 2 · 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ ( 2 · 𝑁 ) ) ↔ 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 2 ) ) ) ) )
6	4 5	sylan	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ ( 2 · 𝑁 ) ) ↔ 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 2 ) ) ) ) )
7		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
8		2cnd	⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ )
9		2ne0	⊢ 2 ≠ 0
10	9	a1i	⊢ ( 𝑁 ∈ ℤ → 2 ≠ 0 )
11	7 8 10	divcan3d	⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 𝑁 ) / 2 ) = 𝑁 )
12	11	fveq2d	⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 2 ) ) = ( ⌊ ‘ 𝑁 ) )
13		flid	⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
14	12 13	eqtrd	⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 2 ) ) = 𝑁 )
15	14	adantr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 2 ) ) = 𝑁 )
16	15	fveq2d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( bits ‘ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 2 ) ) ) = ( bits ‘ 𝑁 ) )
17	16	eleq2d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 2 ) ) ) ↔ 𝑀 ∈ ( bits ‘ 𝑁 ) ) )
18	6 17	bitrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ∈ ( bits ‘ ( 2 · 𝑁 ) ) ↔ 𝑀 ∈ ( bits ‘ 𝑁 ) ) )