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 \in ℤ \land M \in ℕ_{0}) \to (M + 1 \in bits (2 \cdot N) \leftrightarrow M \in bits (N))$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2	1	a1i	$⊢ N \in ℤ \to 2 \in ℤ$
3		id	$⊢ N \in ℤ \to N \in ℤ$
4	2 3	zmulcld	$⊢ N \in ℤ \to 2 \cdot N \in ℤ$
5		bitsp1	$⊢ (2 \cdot N \in ℤ \land M \in ℕ_{0}) \to (M + 1 \in bits (2 \cdot N) \leftrightarrow M \in bits (⌊\frac{2 \cdot N}{2}⌋))$
6	4 5	sylan	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (M + 1 \in bits (2 \cdot N) \leftrightarrow M \in bits (⌊\frac{2 \cdot N}{2}⌋))$
7		zcn	$⊢ N \in ℤ \to N \in ℂ$
8		2cnd	$⊢ N \in ℤ \to 2 \in ℂ$
9		2ne0	$⊢ 2 \neq 0$
10	9	a1i	$⊢ N \in ℤ \to 2 \neq 0$
11	7 8 10	divcan3d	$⊢ N \in ℤ \to \frac{2 \cdot N}{2} = N$
12	11	fveq2d	$⊢ N \in ℤ \to ⌊\frac{2 \cdot N}{2}⌋ = ⌊N⌋$
13		flid	$⊢ N \in ℤ \to ⌊N⌋ = N$
14	12 13	eqtrd	$⊢ N \in ℤ \to ⌊\frac{2 \cdot N}{2}⌋ = N$
15	14	adantr	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to ⌊\frac{2 \cdot N}{2}⌋ = N$
16	15	fveq2d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to bits (⌊\frac{2 \cdot N}{2}⌋) = bits (N)$
17	16	eleq2d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (M \in bits (⌊\frac{2 \cdot N}{2}⌋) \leftrightarrow M \in bits (N))$
18	6 17	bitrd	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (M + 1 \in bits (2 \cdot N) \leftrightarrow M \in bits (N))$

Metamath Proof Explorer