bitsp1

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

		Ref	Expression
	Assertion	bitsp1	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (M + 1 \in bits (N) \leftrightarrow M \in bits (⌊\frac{N}{2}⌋))$

Proof

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2	1	a1i	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2 \in ℕ$
3	2	nncnd	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2 \in ℂ$
4		simpr	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to M \in ℕ_{0}$
5	3 4	expp1d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2^{M + 1} = 2^{M} \cdot 2$
6	2 4	nnexpcld	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2^{M} \in ℕ$
7	6	nncnd	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2^{M} \in ℂ$
8	7 3	mulcomd	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2^{M} \cdot 2 = 2 2^{M}$
9	5 8	eqtrd	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2^{M + 1} = 2 2^{M}$
10	9	oveq2d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to \frac{N}{2^{M + 1}} = \frac{N}{2 2^{M}}$
11		simpl	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \in ℤ$
12	11	zcnd	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \in ℂ$
13	2	nnne0d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2 \neq 0$
14	6	nnne0d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2^{M} \neq 0$
15	12 3 7 13 14	divdiv1d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to \frac{\frac{N}{2}}{2^{M}} = \frac{N}{2 2^{M}}$
16	10 15	eqtr4d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to \frac{N}{2^{M + 1}} = \frac{\frac{N}{2}}{2^{M}}$
17	16	fveq2d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to ⌊\frac{N}{2^{M + 1}}⌋ = ⌊\frac{\frac{N}{2}}{2^{M}}⌋$
18	11	zred	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \in ℝ$
19	18	rehalfcld	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to \frac{N}{2} \in ℝ$
20		fldiv	$⊢ (\frac{N}{2} \in ℝ \land 2^{M} \in ℕ) \to ⌊\frac{⌊\frac{N}{2}⌋}{2^{M}}⌋ = ⌊\frac{\frac{N}{2}}{2^{M}}⌋$
21	19 6 20	syl2anc	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to ⌊\frac{⌊\frac{N}{2}⌋}{2^{M}}⌋ = ⌊\frac{\frac{N}{2}}{2^{M}}⌋$
22	17 21	eqtr4d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to ⌊\frac{N}{2^{M + 1}}⌋ = ⌊\frac{⌊\frac{N}{2}⌋}{2^{M}}⌋$
23	22	breq2d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (2 ∥ ⌊\frac{N}{2^{M + 1}}⌋ \leftrightarrow 2 ∥ ⌊\frac{⌊\frac{N}{2}⌋}{2^{M}}⌋)$
24	23	notbid	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (\neg 2 ∥ ⌊\frac{N}{2^{M + 1}}⌋ \leftrightarrow \neg 2 ∥ ⌊\frac{⌊\frac{N}{2}⌋}{2^{M}}⌋)$
25		peano2nn0	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ_{0}$
26		bitsval2	$⊢ (N \in ℤ \land M + 1 \in ℕ_{0}) \to (M + 1 \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{M + 1}}⌋)$
27	25 26	sylan2	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (M + 1 \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{M + 1}}⌋)$
28	19	flcld	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to ⌊\frac{N}{2}⌋ \in ℤ$
29		bitsval2	$⊢ (⌊\frac{N}{2}⌋ \in ℤ \land M \in ℕ_{0}) \to (M \in bits (⌊\frac{N}{2}⌋) \leftrightarrow \neg 2 ∥ ⌊\frac{⌊\frac{N}{2}⌋}{2^{M}}⌋)$
30	28 29	sylancom	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (M \in bits (⌊\frac{N}{2}⌋) \leftrightarrow \neg 2 ∥ ⌊\frac{⌊\frac{N}{2}⌋}{2^{M}}⌋)$
31	24 27 30	3bitr4d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (M + 1 \in bits (N) \leftrightarrow M \in bits (⌊\frac{N}{2}⌋))$

Metamath Proof Explorer

Theorem bitsp1

Proof